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 
15 #include <util/invariant.h>
16 
18 {
19 protected:
20  std::string qbf_tmp_file;
21 
22  typedef std::map<unsigned, bool> assignmentt;
24 
25 public:
26  explicit qbf_qube_coret(message_handlert &message_handler);
27  virtual ~qbf_qube_coret();
28 
29  virtual const std::string solver_text();
30  virtual resultt prop_solve();
31 
32  virtual bool is_in_core(literalt l) const;
33 
34  virtual tvt l_get(literalt a) const
35  {
36  unsigned v=a.var_no();
37 
38  assignmentt::const_iterator fit=assignment.find(v);
39 
40  if(fit!=assignment.end())
41  return a.sign()?tvt(!fit->second) : tvt(fit->second);
42  else
43  {
44  // throw "Missing toplevel assignment from QuBE";
45  // We assume this is a don't-care and return unknown
46  }
47 
48 
49  return tvt::unknown();
50  }
51 
52  virtual modeltypet m_get(literalt a) const;
53 
54  virtual const exprt f_get(literalt)
55  {
56  INVARIANT(false, "qube does not support full certificates.");
57  }
58 };
59 
60 #endif // CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
Base class for all expressions.
Definition: expr.h:54
bool sign() const
Definition: literal.h:88
var_not var_no() const
Definition: literal.h:83
resultt
Definition: prop.h:99
virtual const std::string solver_text()
qbf_qube_coret(message_handlert &message_handler)
assignmentt assignment
Definition: qbf_qube_core.h:23
virtual tvt l_get(literalt a) const
Definition: qbf_qube_core.h:34
std::map< unsigned, bool > assignmentt
Definition: qbf_qube_core.h:22
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
virtual const exprt f_get(literalt)
Definition: qbf_qube_core.h:54
virtual ~qbf_qube_coret()
virtual bool is_in_core(literalt l) const
std::string qbf_tmp_file
Definition: qbf_qube_core.h:20
Definition: threeval.h:20
static tvt unknown()
Definition: threeval.h:33