1 /********************* */
2 /*! \file decision_strategy.h
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Mathias Preiner
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 Base classes for decision strategies used by theory solvers
13 ** for use in the DecisionManager of TheoryEngine.
16 #include "cvc4_private.h"
18 #ifndef CVC4__THEORY__DECISION_STRATEGY__H
19 #define CVC4__THEORY__DECISION_STRATEGY__H
22 #include "context/cdo.h"
23 #include "expr/node.h"
24 #include "theory/valuation.h"
30 * Virtual base class for decision strategies.
32 class DecisionStrategy
36 virtual ~DecisionStrategy() {}
38 * Initalize this strategy, This is called once per satisfiability call by
39 * the DecisionManager, prior to using this strategy.
41 virtual void initialize() = 0;
43 * If this method returns a non-null node n, then n is the required next
44 * decision of this strategy. It must be the case that n is a literal in
45 * the current CNF stream.
47 virtual Node
getNextDecisionRequest() = 0;
48 /** identify this strategy (for debugging) */
49 virtual std::string
identify() const = 0;
53 * Decision strategy finite model finding.
55 * This is a virtual base class for decision strategies that follow the
56 * "finite model finding" pattern for decisions. Such strategies have the
57 * distinguishing feature that they are interested in a stream of literals
58 * L_1, L_2, L_3, ... and so on. At any given time, they request that L_i is
59 * asserted true for a minimal i.
61 * To enforce this strategy, this class maintains a SAT-context dependent
62 * index d_curr_literal, which corresponds to the minimal index of a literal
63 * in the above list that is not asserted false. A call to
64 * getNextDecisionRequest increments this value until we find a literal L_j
65 * that is not assigned false. If L_j is unassigned, we return it as a decision,
66 * otherwise we return no decisions.
68 class DecisionStrategyFmf
: public DecisionStrategy
71 DecisionStrategyFmf(context::Context
* satContext
, Valuation valuation
);
72 virtual ~DecisionStrategyFmf() {}
74 void initialize() override
;
75 /** get next decision request */
76 Node
getNextDecisionRequest() override
;
77 /** Make the n^th literal of this strategy */
78 virtual Node
mkLiteral(unsigned n
) = 0;
80 * This method returns true iff there exists a (minimal) i such that L_i
81 * is a literal allocated by this class, and is asserted true in the current
82 * context. If it returns true, the argument i is set to this i.
84 bool getAssertedLiteralIndex(unsigned& i
) const;
86 * This method returns the literal L_i allocated by this class that
87 * has been asserted true in the current context and is such that i is
88 * minimal. It returns null if no such literals exist.
90 Node
getAssertedLiteral();
91 /** Get the n^th literal of this strategy */
92 Node
getLiteral(unsigned lit
);
96 * The valuation of this class, used for knowing what literals are asserted,
97 * and with what polarity.
99 Valuation d_valuation
;
101 * The (SAT-context-dependent) flag that is true if there exists a literal
102 * of this class that is asserted true in the current context, according to
105 context::CDO
<bool> d_has_curr_literal
;
107 * The (SAT-context-dependent) index of the current literal of this strategy.
108 * This corresponds to the first literal that is not asserted false in the
109 * current context, according to d_valuation.
111 context::CDO
<unsigned> d_curr_literal
;
112 /** the list of literals of this strategy */
113 std::vector
<Node
> d_literals
;
117 * Special case of above where we only wish to allocate a single literal L_1.
119 class DecisionStrategySingleton
: public DecisionStrategyFmf
122 DecisionStrategySingleton(const char* name
,
124 context::Context
* satContext
,
125 Valuation valuation
);
127 * Make the n^th literal of this strategy. This method returns d_literal if
128 * n=0, null otherwise.
130 Node
mkLiteral(unsigned n
) override
;
131 /** Get single literal */
132 Node
getSingleLiteral();
134 std::string
identify() const override
{ return d_name
; }
137 /** the name of this strategy */
139 /** the literal to decide on */
143 } // namespace theory
146 #endif /* CVC4__THEORY__DECISION_STRATEGY__H */