cprover
Loading...
Searching...
No Matches
qbf_squolem_core.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Squolem Backend (with Proofs)
4
5Author: CM Wintersteiger
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H
13#define CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H
14
15#include <quannon/squolem2/squolem2.h>
16
17#include "qdimacs_core.h"
18
20{
21protected:
22 Squolem2 *squolem;
24
25public:
27 virtual ~qbf_squolem_coret();
28
29 virtual const std::string solver_text();
30 virtual resultt prop_solve();
31
32 virtual tvt l_get(literalt a) const;
33 virtual bool is_in_core(literalt l) const;
34
35 void set_debug_filename(const std::string &str);
36
37 virtual void lcnf(const bvt &bv);
38 virtual void add_quantifier(const quantifiert &quantifier);
39 virtual void set_quantifier(const quantifiert::typet type, const literalt l);
40 virtual void set_no_variables(size_t no);
41 virtual size_t no_clauses() const { return squolem->clauses(); }
42
43 virtual modeltypet m_get(literalt a) const;
44
45 virtual void write_qdimacs_cnf(std::ostream &out);
46
47 void reset(void);
48
49 virtual const exprt f_get(literalt l);
50
51private:
52 typedef std::unordered_map<unsigned, exprt> function_cachet;
54
55 const exprt f_get_cnf(WitnessStack *wsp);
56 const exprt f_get_dnf(WitnessStack *wsp);
57
58 void setup(void);
59};
60
61#endif // CPROVER_SOLVERS_QBF_QBF_SQUOLEM_CORE_H
Base class for all expressions.
Definition expr.h:54
virtual const exprt f_get(literalt l)
virtual void lcnf(const bvt &bv)
virtual void add_quantifier(const quantifiert &quantifier)
virtual resultt prop_solve()
void set_debug_filename(const std::string &str)
const exprt f_get_cnf(WitnessStack *wsp)
std::unordered_map< unsigned, exprt > function_cachet
virtual modeltypet m_get(literalt a) const
function_cachet function_cache
virtual void set_quantifier(const quantifiert::typet type, const literalt l)
virtual void write_qdimacs_cnf(std::ostream &out)
virtual bool is_in_core(literalt l) const
const exprt f_get_dnf(WitnessStack *wsp)
virtual const std::string solver_text()
virtual void set_no_variables(size_t no)
virtual size_t no_clauses() const
virtual tvt l_get(literalt a) const
Definition threeval.h:20
std::vector< literalt > bvt
Definition literal.h:201
resultt
The result of goto verifying.
Definition properties.h:45