1 /*********************                                                        */
2 /*! \file decision_strategy.h
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 Base classes for decision strategies used by theory solvers
13  ** for use in the DecisionManager of TheoryEngine.
14  **/
15 
16 #include "cvc4_private.h"
17 
18 #ifndef __CVC4__THEORY__DECISION_STRATEGY__H
19 #define __CVC4__THEORY__DECISION_STRATEGY__H
20 
21 #include <map>
22 #include "context/cdo.h"
23 #include "expr/node.h"
24 #include "theory/valuation.h"
25 
26 namespace CVC4 {
27 namespace theory {
28 
29 /**
30  * Virtual base class for decision strategies.
31  */
32 class DecisionStrategy
33 {
34  public:
DecisionStrategy()35   DecisionStrategy() {}
~DecisionStrategy()36   virtual ~DecisionStrategy() {}
37   /**
38    * Initalize this strategy, This is called once per satisfiability call by
39    * the DecisionManager, prior to using this strategy.
40    */
41   virtual void initialize() = 0;
42   /**
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.
46    */
47   virtual Node getNextDecisionRequest() = 0;
48   /** identify this strategy (for debugging) */
49   virtual std::string identify() const = 0;
50 };
51 
52 /**
53  * Decision strategy finite model finding.
54  *
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.
60  *
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.
67  */
68 class DecisionStrategyFmf : public DecisionStrategy
69 {
70  public:
71   DecisionStrategyFmf(context::Context* satContext, Valuation valuation);
~DecisionStrategyFmf()72   virtual ~DecisionStrategyFmf() {}
73   /** initialize */
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;
79   /**
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.
83    */
84   bool getAssertedLiteralIndex(unsigned& i) const;
85   /**
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.
89    */
90   Node getAssertedLiteral();
91   /** Get the n^th literal of this strategy */
92   Node getLiteral(unsigned lit);
93 
94  protected:
95   /**
96    * The valuation of this class, used for knowing what literals are asserted,
97    * and with what polarity.
98    */
99   Valuation d_valuation;
100   /**
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
103    * d_valuation.
104    */
105   context::CDO<bool> d_has_curr_literal;
106   /**
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.
110    */
111   context::CDO<unsigned> d_curr_literal;
112   /** the list of literals of this strategy */
113   std::vector<Node> d_literals;
114 };
115 
116 /**
117  * Special case of above where we only wish to allocate a single literal L_1.
118  */
119 class DecisionStrategySingleton : public DecisionStrategyFmf
120 {
121  public:
122   DecisionStrategySingleton(const char* name,
123                             Node lit,
124                             context::Context* satContext,
125                             Valuation valuation);
126   /**
127    * Make the n^th literal of this strategy. This method returns d_literal if
128    * n=0, null otherwise.
129    */
130   Node mkLiteral(unsigned n) override;
131   /** Get single literal */
132   Node getSingleLiteral();
133   /** identify */
identify()134   std::string identify() const override { return d_name; }
135 
136  private:
137   /** the name of this strategy */
138   std::string d_name;
139   /** the literal to decide on */
140   Node d_literal;
141 };
142 
143 }  // namespace theory
144 }  // namespace CVC4
145 
146 #endif /* __CVC4__THEORY__DECISION_STRATEGY__H */
147