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