cprover
qbf_squolem.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Squolem Backend
4
5Author: 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{
21protected:
22 Squolem2 squolem;
24
25public:
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:97
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