cprover
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
49 BDD *matrix;
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
Base class for all expressions.
Definition: expr.h:54
resultt
Definition: prop.h:97
std::vector< BDD * > model_bddst
Definition: qbf_bdd_core.h:26
virtual const exprt f_get(literalt l)
std::unordered_map< unsigned, exprt > function_cachet
Definition: qbf_bdd_core.h:29
model_bddst model_bdds
Definition: qbf_bdd_core.h:27
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
Definition: qbf_bdd_core.h:30
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
Definition: qbf_bdd_core.h:47
virtual resultt prop_solve()
std::vector< BDD * > bdd_variable_mapt
Definition: qbf_bdd_core.h:46
void compress_certificate(void)
Definition: threeval.h:20
std::vector< literalt > bvt
Definition: literal.h:201