cprover
Loading...
Searching...
No Matches
qbf_bdd_core.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: CM Wintersteiger
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_SOLVERS_QBF_QBF_BDD_CORE_H
11#define CPROVER_SOLVERS_QBF_QBF_BDD_CORE_H
12
13#include <vector>
14
15
16#include "qdimacs_core.h"
17
18class Cudd; // NOLINT(*)
19class BDD; // NOLINT(*)
20
22{
23protected:
25
26 typedef std::vector<BDD*> model_bddst;
28
29 typedef std::unordered_map<unsigned, exprt> function_cachet;
31
32public:
34 virtual ~qbf_bdd_certificatet(void);
35
36 virtual literalt new_variable(void);
37
38 virtual tvt l_get(literalt a) const;
39 virtual const exprt f_get(literalt l);
40};
41
42
44{
45private:
46 typedef std::vector<BDD*> bdd_variable_mapt;
48
50
51public:
53 virtual ~qbf_bdd_coret();
54
55 virtual literalt new_variable();
56
57 virtual void lcnf(const bvt &bv);
58 virtual literalt lor(literalt a, literalt b);
59 virtual literalt lor(const bvt &bv);
60
61 virtual const std::string solver_text();
62 virtual resultt prop_solve();
63 virtual tvt l_get(literalt a) const;
64
65 virtual bool is_in_core(literalt l) const;
66 virtual modeltypet m_get(literalt a) const;
67
68protected:
69 void compress_certificate(void);
70};
71
72#endif // CPROVER_SOLVERS_QBF_QBF_BDD_CORE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class for all expressions.
Definition expr.h:54
std::vector< BDD * > model_bddst
virtual const exprt f_get(literalt l)
std::unordered_map< unsigned, exprt > function_cachet
model_bddst model_bdds
virtual ~qbf_bdd_certificatet(void)
virtual literalt new_variable(void)
Generate a new variable and return it as a literal.
virtual tvt l_get(literalt a) const
function_cachet function_cache
virtual modeltypet m_get(literalt a) const
virtual tvt l_get(literalt a) const
virtual literalt new_variable()
Generate a new variable and return it as a literal.
virtual const std::string solver_text()
virtual void lcnf(const bvt &bv)
virtual ~qbf_bdd_coret()
virtual bool is_in_core(literalt l) const
virtual literalt lor(literalt a, literalt b)
bdd_variable_mapt bdd_variable_map
virtual resultt prop_solve()
std::vector< BDD * > bdd_variable_mapt
void compress_certificate(void)
Definition threeval.h:20
std::vector< literalt > bvt
Definition literal.h:201
resultt
The result of goto verifying.
Definition properties.h:45