1 /********************* */
2 /*! \file decision_strategy.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Implementation of base classes for decision strategies used by theory
13 ** solvers for use in the DecisionManager of TheoryEngine.
16 #include "theory/decision_strategy.h"
18 #include "theory/rewriter.h"
20 using namespace CVC4::kind
;
25 DecisionStrategyFmf::DecisionStrategyFmf(context::Context
* satContext
,
27 : d_valuation(valuation
),
28 d_has_curr_literal(false, satContext
),
29 d_curr_literal(0, satContext
)
33 void DecisionStrategyFmf::initialize() { d_literals
.clear(); }
35 Node
DecisionStrategyFmf::getNextDecisionRequest()
37 Trace("dec-strategy-debug")
38 << "Get next decision request " << identify() << "..." << std::endl
;
39 if (d_has_curr_literal
.get())
41 Trace("dec-strategy-debug") << "...already has decision" << std::endl
;
45 unsigned curr_lit
= d_curr_literal
.get();
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
57 if (!d_valuation
.hasSatValue(lit
, value
))
59 Trace("dec-strategy-debug") << "...not assigned, return." << std::endl
;
60 // if it has not been decided, return it
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
);
75 Trace("dec-strategy-debug") << "...already assigned true." << std::endl
;
80 Trace("dec-strategy-debug") << "...exhausted literals." << std::endl
;
83 // the current literal has been decided with the right polarity, we are done
84 d_has_curr_literal
= true;
88 bool DecisionStrategyFmf::getAssertedLiteralIndex(unsigned& i
) const
90 if (d_has_curr_literal
.get())
92 i
= d_curr_literal
.get();
98 Node
DecisionStrategyFmf::getAssertedLiteral()
100 if (d_has_curr_literal
.get())
102 Assert(d_curr_literal
.get() < d_literals
.size());
103 return getLiteral(d_curr_literal
.get());
108 Node
DecisionStrategyFmf::getLiteral(unsigned n
)
110 // allocate until the index is valid
111 while (n
>= d_literals
.size())
113 Node lit
= mkLiteral(d_literals
.size());
116 lit
= Rewriter::rewrite(lit
);
118 d_literals
.push_back(lit
);
120 Node ret
= d_literals
[n
];
123 // always ensure it is in the CNF stream
124 ret
= d_valuation
.ensureLiteral(ret
);
129 DecisionStrategySingleton::DecisionStrategySingleton(
132 context::Context
* satContext
,
134 : DecisionStrategyFmf(satContext
, valuation
), d_name(name
), d_literal(lit
)
138 Node
DecisionStrategySingleton::mkLiteral(unsigned n
)
147 Node
DecisionStrategySingleton::getSingleLiteral() { return d_literal
; }
149 } // namespace theory