cprover
qbf_qube_core.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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{
19protected:
20 std::string qbf_tmp_file;
21
22 typedef std::map<unsigned, bool> assignmentt;
24
25public:
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:97
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