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 CVC5__DECISION__DECISION_ENGINE_OLD_H |
19 |
|
#define CVC5__DECISION__DECISION_ENGINE_OLD_H |
20 |
|
|
21 |
|
#include "base/output.h" |
22 |
|
#include "context/cdo.h" |
23 |
|
#include "decision/decision_engine.h" |
24 |
|
#include "decision/decision_strategy.h" |
25 |
|
#include "expr/node.h" |
26 |
|
#include "prop/cnf_stream.h" |
27 |
|
#include "prop/sat_solver.h" |
28 |
|
#include "prop/sat_solver_types.h" |
29 |
|
#include "util/result.h" |
30 |
|
|
31 |
|
using namespace cvc5::prop; |
32 |
|
using namespace cvc5::decision; |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
|
36 |
|
class DecisionEngineOld : public decision::DecisionEngine |
37 |
|
{ |
38 |
|
public: |
39 |
|
// Necessary functions |
40 |
|
|
41 |
|
/** Constructor */ |
42 |
|
DecisionEngineOld(Env& env); |
43 |
|
|
44 |
|
/** Destructor, currently does nothing */ |
45 |
6 |
~DecisionEngineOld() |
46 |
6 |
{ |
47 |
3 |
Trace("decision") << "Destroying decision engine" << std::endl; |
48 |
6 |
} |
49 |
|
|
50 |
|
/** |
51 |
|
* This is called by SolverEngine, at shutdown time, just before |
52 |
|
* destruction. It is important because there are destruction |
53 |
|
* ordering issues between some parts of the system. |
54 |
|
*/ |
55 |
|
void shutdown(); |
56 |
|
|
57 |
|
// Interface for External World to use our services |
58 |
|
|
59 |
|
/** Gets the next decision based on strategies that are enabled */ |
60 |
|
SatLiteral getNextInternal(bool& stopSearch) override; |
61 |
|
|
62 |
|
/** Is the DecisionEngineOld in a state where it has solved everything? */ |
63 |
171 |
bool isDone() override |
64 |
|
{ |
65 |
342 |
Trace("decision") << "DecisionEngineOld::isDone() returning " |
66 |
342 |
<< (d_result != SAT_VALUE_UNKNOWN) |
67 |
342 |
<< (d_result != SAT_VALUE_UNKNOWN ? "true" : "false") |
68 |
171 |
<< std::endl; |
69 |
171 |
return (d_result != SAT_VALUE_UNKNOWN); |
70 |
|
} |
71 |
|
|
72 |
|
/** */ |
73 |
|
Result getResult() |
74 |
|
{ |
75 |
|
switch (d_result.get()) |
76 |
|
{ |
77 |
|
case SAT_VALUE_TRUE: return Result(Result::SAT); |
78 |
|
case SAT_VALUE_FALSE: return Result(Result::UNSAT); |
79 |
|
case SAT_VALUE_UNKNOWN: |
80 |
|
return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); |
81 |
|
default: Assert(false) << "d_result is garbage"; |
82 |
|
} |
83 |
|
return Result(); |
84 |
|
} |
85 |
|
|
86 |
|
/** */ |
87 |
|
void setResult(SatValue val) { d_result = val; } |
88 |
|
|
89 |
|
// External World helping us help the Strategies |
90 |
|
|
91 |
|
/** |
92 |
|
* Notify this class that assertion is an (input) assertion, not corresponding |
93 |
|
* to a skolem definition. |
94 |
|
*/ |
95 |
|
void addAssertion(TNode assertion, bool isLemma) override; |
96 |
|
/** |
97 |
|
* Notify this class that lem is the skolem definition for skolem, which is |
98 |
|
* a part of the current assertions. |
99 |
|
*/ |
100 |
|
void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override; |
101 |
|
|
102 |
|
// Interface for Strategies to use stuff stored in Decision Engine |
103 |
|
// (which was possibly requested by them on initialization) |
104 |
|
|
105 |
|
// Interface for Strategies to get information about External World |
106 |
|
|
107 |
|
bool hasSatLiteral(TNode n) { return d_cnfStream->hasLiteral(n); } |
108 |
|
SatLiteral getSatLiteral(TNode n) { return d_cnfStream->getLiteral(n); } |
109 |
|
SatValue getSatValue(SatLiteral l) { return d_satSolver->value(l); } |
110 |
|
SatValue getSatValue(TNode n) { return getSatValue(getSatLiteral(n)); } |
111 |
|
Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } |
112 |
|
|
113 |
|
private: |
114 |
|
// Disable creating decision engine without required parameters |
115 |
|
DecisionEngineOld(); |
116 |
|
|
117 |
|
// Does decision engine know the answer? |
118 |
|
context::CDO<SatValue> d_result; |
119 |
|
|
120 |
|
// init/shutdown state |
121 |
|
unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown |
122 |
|
/** The ITE decision strategy we have allocated */ |
123 |
|
std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy; |
124 |
|
/** Whether we are using stop only */ |
125 |
|
bool d_decisionStopOnly; |
126 |
|
|
127 |
|
}; /* DecisionEngineOld class */ |
128 |
|
|
129 |
|
} // namespace cvc5 |
130 |
|
|
131 |
|
#endif /* CVC5__DECISION__DECISION_ENGINE_H */ |