1 /********************* */
2 /*! \file decision_strategy.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Implementation of base classes for decision strategies used by theory
13 ** solvers for use in the DecisionManager of TheoryEngine.
14 **/
15
16 #include "theory/decision_strategy.h"
17
18 #include "theory/rewriter.h"
19
20 using namespace CVC4::kind;
21
22 namespace CVC4 {
23 namespace theory {
24
DecisionStrategyFmf(context::Context * satContext,Valuation valuation)25 DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext,
26 Valuation valuation)
27 : d_valuation(valuation),
28 d_has_curr_literal(false, satContext),
29 d_curr_literal(0, satContext)
30 {
31 }
32
initialize()33 void DecisionStrategyFmf::initialize() { d_literals.clear(); }
34
getNextDecisionRequest()35 Node DecisionStrategyFmf::getNextDecisionRequest()
36 {
37 Trace("dec-strategy-debug")
38 << "Get next decision request " << identify() << "..." << std::endl;
39 if (d_has_curr_literal.get())
40 {
41 Trace("dec-strategy-debug") << "...already has decision" << std::endl;
42 return Node::null();
43 }
44 bool success;
45 unsigned curr_lit = d_curr_literal.get();
46 do
47 {
48 success = true;
49 // get the current literal
50 Node lit = getLiteral(curr_lit);
51 Trace("dec-strategy-debug")
52 << "...check literal #" << curr_lit << " : " << lit << std::endl;
53 // if out of literals, we are done in the current SAT context
54 if (!lit.isNull())
55 {
56 bool value;
57 if (!d_valuation.hasSatValue(lit, value))
58 {
59 Trace("dec-strategy-debug") << "...not assigned, return." << std::endl;
60 // if it has not been decided, return it
61 return lit;
62 }
63 else if (!value)
64 {
65 Trace("dec-strategy-debug")
66 << "...assigned false, increment." << std::endl;
67 // asserted false, the current literal is incremented
68 curr_lit = d_curr_literal.get() + 1;
69 d_curr_literal.set(curr_lit);
70 // repeat
71 success = false;
72 }
73 else
74 {
75 Trace("dec-strategy-debug") << "...already assigned true." << std::endl;
76 }
77 }
78 else
79 {
80 Trace("dec-strategy-debug") << "...exhausted literals." << std::endl;
81 }
82 } while (!success);
83 // the current literal has been decided with the right polarity, we are done
84 d_has_curr_literal = true;
85 return Node::null();
86 }
87
getAssertedLiteralIndex(unsigned & i) const88 bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i) const
89 {
90 if (d_has_curr_literal.get())
91 {
92 i = d_curr_literal.get();
93 return true;
94 }
95 return false;
96 }
97
getAssertedLiteral()98 Node DecisionStrategyFmf::getAssertedLiteral()
99 {
100 if (d_has_curr_literal.get())
101 {
102 Assert(d_curr_literal.get() < d_literals.size());
103 return getLiteral(d_curr_literal.get());
104 }
105 return Node::null();
106 }
107
getLiteral(unsigned n)108 Node DecisionStrategyFmf::getLiteral(unsigned n)
109 {
110 // allocate until the index is valid
111 while (n >= d_literals.size())
112 {
113 Node lit = mkLiteral(d_literals.size());
114 if (!lit.isNull())
115 {
116 lit = Rewriter::rewrite(lit);
117 lit = d_valuation.ensureLiteral(lit);
118 }
119 d_literals.push_back(lit);
120 }
121 return d_literals[n];
122 }
123
DecisionStrategySingleton(const char * name,Node lit,context::Context * satContext,Valuation valuation)124 DecisionStrategySingleton::DecisionStrategySingleton(
125 const char* name,
126 Node lit,
127 context::Context* satContext,
128 Valuation valuation)
129 : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit)
130 {
131 }
132
mkLiteral(unsigned n)133 Node DecisionStrategySingleton::mkLiteral(unsigned n)
134 {
135 if (n == 0)
136 {
137 return d_literal;
138 }
139 return Node::null();
140 }
141
getSingleLiteral()142 Node DecisionStrategySingleton::getSingleLiteral() { return d_literal; }
143
144 } // namespace theory
145 } // namespace CVC4
146