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
17
class
qbf_qube_coret
:
public
qdimacs_coret
18
{
19
protected
:
20
std::string
qbf_tmp_file
;
21
22
typedef
std::map<unsigned, bool>
assignmentt
;
23
assignmentt
assignment
;
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
qbf_qube_coret::qbf_qube_coret
qbf_qube_coret(message_handlert &message_handler)
Definition:
qbf_qube_core.cpp:18
qbf_qube_coret::qbf_tmp_file
std::string qbf_tmp_file
Definition:
qbf_qube_core.h:20
qbf_qube_coret::solver_text
virtual const std::string solver_text()
Definition:
qbf_qube_core.cpp:29
invariant.h
exprt
Base class for all expressions.
Definition:
expr.h:53
literalt::var_no
var_not var_no() const
Definition:
literal.h:83
qbf_qube_coret::is_in_core
virtual bool is_in_core(literalt l) const
Definition:
qbf_qube_core.cpp:132
qdimacs_core.h
qbf_qube_coret
Definition:
qbf_qube_core.h:18
qbf_qube_coret::assignment
assignmentt assignment
Definition:
qbf_qube_core.h:23
qbf_qube_coret::f_get
virtual const exprt f_get(literalt)
Definition:
qbf_qube_core.h:54
qbf_qube_coret::~qbf_qube_coret
virtual ~qbf_qube_coret()
Definition:
qbf_qube_core.cpp:25
message_handlert
Definition:
message.h:28
tvt::unknown
static tvt unknown()
Definition:
threeval.h:33
qdimacs_coret::modeltypet
modeltypet
Definition:
qdimacs_core.h:30
propt::resultt
resultt
Definition:
prop.h:99
qbf_qube_coret::m_get
virtual modeltypet m_get(literalt a) const
Definition:
qbf_qube_core.cpp:137
qdimacs_coret
Definition:
qdimacs_core.h:20
tvt
Definition:
threeval.h:20
literalt::sign
bool sign() const
Definition:
literal.h:88
qbf_qube_coret::l_get
virtual tvt l_get(literalt a) const
Definition:
qbf_qube_core.h:34
qbf_qube_coret::prop_solve
virtual resultt prop_solve()
Definition:
qbf_qube_core.cpp:34
literalt
Definition:
literal.h:26
qbf_qube_coret::assignmentt
std::map< unsigned, bool > assignmentt
Definition:
qbf_qube_core.h:22
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition:
invariant.h:424
solvers
qbf
qbf_qube_core.h
Generated by
1.8.20