cprover
Loading...
Searching...
No Matches
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class for all expressions.
Definition expr.h:54
virtual const std::string solver_text()
assignmentt assignment
virtual tvt l_get(literalt a) const
std::map< unsigned, bool > assignmentt
virtual modeltypet m_get(literalt a) const
virtual resultt prop_solve()
virtual const exprt f_get(literalt)
virtual ~qbf_qube_coret()
virtual bool is_in_core(literalt l) const
std::string qbf_tmp_file
Definition threeval.h:20
static tvt unknown()
Definition threeval.h:33
resultt
The result of goto verifying.
Definition properties.h:45
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423