cprover
qbf_squolem_core.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Squolem Backend (with Proofs)
4 
5 Author: 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 {
21 protected:
22  Squolem2 *squolem;
24 
25 public:
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 
51 private:
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
resultt
Definition: prop.h:97
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)
virtual ~qbf_squolem_coret()
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