cprover
Loading...
Searching...
No Matches
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
Squolem2 squolem
Definition qbf_squolem.h:22
virtual void set_no_variables(size_t no)
virtual resultt prop_solve()
virtual ~qbf_squolemt()
bool early_decision
Definition qbf_squolem.h:23
virtual const std::string solver_text()
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual tvt l_get(literalt a) const
virtual void lcnf(const bvt &bv)
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
resultt
The result of goto verifying.
Definition properties.h:45