1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Kshitij Bansal, Andrew Reynolds, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Old implementation of the decision engine |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC4__DECISION__DECISION_ENGINE_OLD_H |
19 |
|
#define CVC4__DECISION__DECISION_ENGINE_OLD_H |
20 |
|
|
21 |
|
#include "base/output.h" |
22 |
|
#include "context/cdo.h" |
23 |
|
#include "decision/decision_strategy.h" |
24 |
|
#include "expr/node.h" |
25 |
|
#include "prop/cnf_stream.h" |
26 |
|
#include "prop/sat_solver.h" |
27 |
|
#include "prop/sat_solver_types.h" |
28 |
|
#include "util/result.h" |
29 |
|
|
30 |
|
using namespace cvc5::prop; |
31 |
|
using namespace cvc5::decision; |
32 |
|
|
33 |
|
namespace cvc5 { |
34 |
|
|
35 |
|
class DecisionEngineOld |
36 |
|
{ |
37 |
|
public: |
38 |
|
// Necessary functions |
39 |
|
|
40 |
|
/** Constructor */ |
41 |
|
DecisionEngineOld(context::Context* sc, context::UserContext* uc); |
42 |
|
|
43 |
|
/** Destructor, currently does nothing */ |
44 |
9494 |
~DecisionEngineOld() |
45 |
9494 |
{ |
46 |
9494 |
Trace("decision") << "Destroying decision engine" << std::endl; |
47 |
9494 |
} |
48 |
|
|
49 |
9494 |
void setSatSolver(CDCLTSatSolverInterface* ss) |
50 |
|
{ |
51 |
|
// setPropEngine should not be called more than once |
52 |
9494 |
Assert(d_satSolver == NULL); |
53 |
9494 |
Assert(ss != NULL); |
54 |
9494 |
d_satSolver = ss; |
55 |
9494 |
} |
56 |
|
|
57 |
9494 |
void setCnfStream(CnfStream* cs) |
58 |
|
{ |
59 |
|
// setPropEngine should not be called more than once |
60 |
9494 |
Assert(d_cnfStream == NULL); |
61 |
9494 |
Assert(cs != NULL); |
62 |
9494 |
d_cnfStream = cs; |
63 |
9494 |
} |
64 |
|
|
65 |
|
/** |
66 |
|
* This is called by SmtEngine, at shutdown time, just before |
67 |
|
* destruction. It is important because there are destruction |
68 |
|
* ordering issues between some parts of the system. |
69 |
|
*/ |
70 |
|
void shutdown(); |
71 |
|
|
72 |
|
// Interface for External World to use our services |
73 |
|
|
74 |
|
/** Gets the next decision based on strategies that are enabled */ |
75 |
|
SatLiteral getNext(bool& stopSearch); |
76 |
|
|
77 |
|
/** Is the DecisionEngineOld in a state where it has solved everything? */ |
78 |
55380 |
bool isDone() |
79 |
|
{ |
80 |
110760 |
Trace("decision") << "DecisionEngineOld::isDone() returning " |
81 |
110760 |
<< (d_result != SAT_VALUE_UNKNOWN) |
82 |
110760 |
<< (d_result != SAT_VALUE_UNKNOWN ? "true" : "false") |
83 |
55380 |
<< std::endl; |
84 |
55380 |
return (d_result != SAT_VALUE_UNKNOWN); |
85 |
|
} |
86 |
|
|
87 |
|
/** */ |
88 |
|
Result getResult() |
89 |
|
{ |
90 |
|
switch (d_result.get()) |
91 |
|
{ |
92 |
|
case SAT_VALUE_TRUE: return Result(Result::SAT); |
93 |
|
case SAT_VALUE_FALSE: return Result(Result::UNSAT); |
94 |
|
case SAT_VALUE_UNKNOWN: |
95 |
|
return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); |
96 |
|
default: Assert(false) << "d_result is garbage"; |
97 |
|
} |
98 |
|
return Result(); |
99 |
|
} |
100 |
|
|
101 |
|
/** */ |
102 |
41528 |
void setResult(SatValue val) { d_result = val; } |
103 |
|
|
104 |
|
// External World helping us help the Strategies |
105 |
|
|
106 |
|
/** |
107 |
|
* Notify this class that assertion is an (input) assertion, not corresponding |
108 |
|
* to a skolem definition. |
109 |
|
*/ |
110 |
|
void addAssertion(TNode assertion); |
111 |
|
/** |
112 |
|
* Notify this class that lem is the skolem definition for skolem, which is |
113 |
|
* a part of the current assertions. |
114 |
|
*/ |
115 |
|
void addSkolemDefinition(TNode lem, TNode skolem); |
116 |
|
|
117 |
|
// Interface for Strategies to use stuff stored in Decision Engine |
118 |
|
// (which was possibly requested by them on initialization) |
119 |
|
|
120 |
|
// Interface for Strategies to get information about External World |
121 |
|
|
122 |
39080235 |
bool hasSatLiteral(TNode n) { return d_cnfStream->hasLiteral(n); } |
123 |
39659521 |
SatLiteral getSatLiteral(TNode n) { return d_cnfStream->getLiteral(n); } |
124 |
39016778 |
SatValue getSatValue(SatLiteral l) { return d_satSolver->value(l); } |
125 |
39016778 |
SatValue getSatValue(TNode n) { return getSatValue(getSatLiteral(n)); } |
126 |
|
Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } |
127 |
|
|
128 |
|
private: |
129 |
|
// Disable creating decision engine without required parameters |
130 |
|
DecisionEngineOld(); |
131 |
|
|
132 |
|
CnfStream* d_cnfStream; |
133 |
|
CDCLTSatSolverInterface* d_satSolver; |
134 |
|
|
135 |
|
context::Context* d_satContext; |
136 |
|
context::UserContext* d_userContext; |
137 |
|
|
138 |
|
// Does decision engine know the answer? |
139 |
|
context::CDO<SatValue> d_result; |
140 |
|
|
141 |
|
// init/shutdown state |
142 |
|
unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown |
143 |
|
/** The ITE decision strategy we have allocated */ |
144 |
|
std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy; |
145 |
|
|
146 |
|
}; /* DecisionEngineOld class */ |
147 |
|
|
148 |
|
} // namespace cvc5 |
149 |
|
|
150 |
|
#endif /* CVC4__DECISION__DECISION_ENGINE_H */ |