cprover
qbf_qube_core.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: CM Wintersteiger
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
11 #define CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
12 
13 #include "qdimacs_core.h"
14 
16 {
17 protected:
18  std::string qbf_tmp_file;
19 
20  typedef std::map<unsigned, bool> assignmentt;
22 
23 public:
25  virtual ~qbf_qube_coret();
26 
27  virtual const std::string solver_text();
28  virtual resultt prop_solve();
29 
30  virtual bool is_in_core(literalt l) const;
31 
32  virtual tvt l_get(literalt a) const
33  {
34  unsigned v=a.var_no();
35 
36  assignmentt::const_iterator fit=assignment.find(v);
37 
38  if(fit!=assignment.end())
39  return a.sign()?tvt(!fit->second) : tvt(fit->second);
40  else
41  {
42  // throw "Missing toplevel assignment from QuBE";
43  // We assume this is a don't-care and return unknown
44  }
45 
46 
47  return tvt::unknown();
48  }
49 
50  virtual modeltypet m_get(literalt a) const;
51 
52  virtual const exprt f_get(literalt)
53  {
54  throw "qube does not support full certificates.";
55  }
56 };
57 
58 #endif // CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
std::string qbf_tmp_file
Definition: qbf_qube_core.h:18
static tvt unknown()
Definition: threeval.h:33
virtual bool is_in_core(literalt l) const
virtual ~qbf_qube_coret()
virtual tvt l_get(literalt a) const
Definition: qbf_qube_core.h:32
Definition: threeval.h:19
var_not var_no() const
Definition: literal.h:82
assignmentt assignment
Definition: qbf_qube_core.h:21
virtual const std::string solver_text()
virtual const exprt f_get(literalt)
Definition: qbf_qube_core.h:52
resultt
Definition: prop.h:96
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
Base class for all expressions.
Definition: expr.h:42
bool sign() const
Definition: literal.h:87
std::map< unsigned, bool > assignmentt
Definition: qbf_qube_core.h:20