cprover
qbf_squolem.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Squolem Backend
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_QBF_QBF_SQUOLEM_H
13 #define CPROVER_SOLVERS_QBF_QBF_SQUOLEM_H
14 
15 #include <quannon/squolem2/squolem2.h>
16 
17 #include "qdimacs_cnf.h"
18 
20 {
21 protected:
22  Squolem2 squolem;
24 
25 public:
26  qbf_squolemt();
27  virtual ~qbf_squolemt();
28 
29  virtual const std::string solver_text();
30  virtual resultt prop_solve();
31  virtual tvt l_get(literalt a) const;
32 
33  virtual void lcnf(const bvt &bv);
34  virtual void add_quantifier(const quantifiert &quantifier);
35  virtual void set_quantifier(const quantifiert::typet type, const literalt l);
36  virtual void set_no_variables(size_t no);
37  virtual size_t no_clauses() const { return squolem.clauses(); }
38 };
39 
40 #endif // CPROVER_SOLVERS_QBF_QBF_SQUOLEM_H
resultt
Definition: prop.h:99
Squolem2 squolem
Definition: qbf_squolem.h:22
virtual void set_no_variables(size_t no)
virtual resultt prop_solve()
Definition: qbf_squolem.cpp:34
virtual ~qbf_squolemt()
Definition: qbf_squolem.cpp:19
bool early_decision
Definition: qbf_squolem.h:23
virtual const std::string solver_text()
Definition: qbf_squolem.cpp:29
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual tvt l_get(literalt a) const
Definition: qbf_squolem.cpp:24
virtual void lcnf(const bvt &bv)
Definition: qbf_squolem.cpp:71
virtual size_t no_clauses() const
Definition: qbf_squolem.h:37
virtual void add_quantifier(const quantifiert &quantifier)
Definition: threeval.h:20
std::vector< literalt > bvt
Definition: literal.h:201