cprover
qbf_bdd_core.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
18 class Cudd; // NOLINT(*)
19 class BDD; // NOLINT(*)
20 
22 {
23 protected:
24  Cudd *bdd_manager;
25 
26  typedef std::vector<BDD*> model_bddst;
28 
29  typedef std::unordered_map<unsigned, exprt> function_cachet;
31 
32 public:
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 {
45 private:
46  typedef std::vector<BDD*> bdd_variable_mapt;
48 
49  BDD *matrix;
50 
51 public:
52  qbf_bdd_coret();
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 
68 protected:
69  void compress_certificate(void);
70 };
71 
72 #endif // CPROVER_SOLVERS_QBF_QBF_BDD_CORE_H
virtual bool is_in_core(literalt l) const
virtual void lcnf(const bvt &bv)
virtual resultt prop_solve()
virtual const std::string solver_text()
virtual literalt new_variable(void)
Generate a new variable and return it as a literal.
virtual tvt l_get(literalt a) const
model_bddst model_bdds
Definition: qbf_bdd_core.h:27
virtual literalt lor(literalt a, literalt b)
virtual tvt l_get(literalt a) const
virtual modeltypet m_get(literalt a) const
std::vector< BDD * > bdd_variable_mapt
Definition: qbf_bdd_core.h:46
bdd_variable_mapt bdd_variable_map
Definition: qbf_bdd_core.h:47
std::unordered_map< unsigned, exprt > function_cachet
Definition: qbf_bdd_core.h:29
Definition: threeval.h:19
function_cachet function_cache
Definition: qbf_bdd_core.h:30
resultt
Definition: prop.h:96
virtual ~qbf_bdd_certificatet(void)
std::vector< BDD * > model_bddst
Definition: qbf_bdd_core.h:26
Base class for all expressions.
Definition: expr.h:42
void compress_certificate(void)
virtual const exprt f_get(literalt l)
virtual literalt new_variable()
Generate a new variable and return it as a literal.
virtual ~qbf_bdd_coret()
std::vector< literalt > bvt
Definition: literal.h:200