1 /********************* */ 2 /*! \file first_order_model.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Paul Meng, Morgan Deters 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 Model extended classes 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__FIRST_ORDER_MODEL_H 18 #define __CVC4__FIRST_ORDER_MODEL_H 19 20 #include "theory/theory_model.h" 21 #include "theory/uf/theory_uf_model.h" 22 #include "expr/attribute.h" 23 24 namespace CVC4 { 25 namespace theory { 26 27 class QuantifiersEngine; 28 29 struct ModelBasisAttributeId 30 { 31 }; 32 typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; 33 // for APPLY_UF terms, 1 : term has direct child with model basis attribute, 34 // 0 : term has no direct child with model basis attribute. 35 struct ModelBasisArgAttributeId 36 { 37 }; 38 typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> 39 ModelBasisArgAttribute; 40 41 namespace quantifiers { 42 43 class TermDb; 44 45 namespace fmcheck { 46 class FirstOrderModelFmc; 47 }/* CVC4::theory::quantifiers::fmcheck namespace */ 48 49 struct IsStarAttributeId {}; 50 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute; 51 52 /** Quantifiers representative bound 53 * 54 * This class is used for computing (finite) 55 * bounds for the domain of a quantifier 56 * in the context of a RepSetIterator 57 * (see theory/rep_set.h). 58 */ 59 class QRepBoundExt : public RepBoundExt 60 { 61 public: QRepBoundExt(QuantifiersEngine * qe)62 QRepBoundExt(QuantifiersEngine* qe) : d_qe(qe) {} ~QRepBoundExt()63 virtual ~QRepBoundExt() {} 64 /** set bound */ 65 RepSetIterator::RsiEnumType setBound(Node owner, 66 unsigned i, 67 std::vector<Node>& elements) override; 68 /** reset index */ 69 bool resetIndex(RepSetIterator* rsi, 70 Node owner, 71 unsigned i, 72 bool initial, 73 std::vector<Node>& elements) override; 74 /** initialize representative set for type */ 75 bool initializeRepresentativesForType(TypeNode tn) override; 76 /** get variable order */ 77 bool getVariableOrder(Node owner, std::vector<unsigned>& varOrder) override; 78 79 private: 80 /** quantifiers engine associated with this bound */ 81 QuantifiersEngine* d_qe; 82 /** indices that are bound integer enumeration */ 83 std::map<unsigned, bool> d_bound_int; 84 }; 85 86 // TODO (#1301) : document and refactor this class 87 class FirstOrderModel : public TheoryModel 88 { 89 public: 90 FirstOrderModel(QuantifiersEngine* qe, context::Context* c, std::string name); 91 asFirstOrderModelFmc()92 virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; } 93 /** assert quantifier */ 94 void assertQuantifier( Node n ); 95 /** get number of asserted quantifiers */ 96 unsigned getNumAssertedQuantifiers(); 97 /** get asserted quantifier */ 98 Node getAssertedQuantifier( unsigned i, bool ordered = false ); 99 /** initialize model for term */ 100 void initializeModelForTerm( Node n, std::map< Node, bool >& visited ); 101 // initialize the model 102 void initialize(); 103 /** get variable id */ getVariableId(TNode q,TNode n)104 int getVariableId(TNode q, TNode n) { 105 return d_quant_var_id.find( q )!=d_quant_var_id.end() ? d_quant_var_id[q][n] : -1; 106 } 107 /** do we need to do any work? */ 108 bool checkNeeded(); 109 /** reset round */ 110 void reset_round(); 111 /** mark quantified formula relevant */ 112 void markRelevant( Node q ); 113 /** get relevance value */ 114 int getRelevanceValue( Node q ); 115 /** set quantified formula active/inactive 116 * a quantified formula may be set inactive if for instance: 117 * - it is entailed by other quantified formulas 118 */ 119 void setQuantifierActive( TNode q, bool active ); 120 /** is quantified formula active */ 121 bool isQuantifierActive( TNode q ); 122 /** is quantified formula asserted */ 123 bool isQuantifierAsserted( TNode q ); 124 /** get model basis term */ 125 Node getModelBasisTerm(TypeNode tn); 126 /** is model basis term */ 127 bool isModelBasisTerm(Node n); 128 /** get model basis term for op */ 129 Node getModelBasisOpTerm(Node op); 130 /** get model basis */ 131 Node getModelBasis(Node q, Node n); 132 /** get model basis arg */ 133 unsigned getModelBasisArg(Node n); 134 /** get some domain element */ 135 Node getSomeDomainElement(TypeNode tn); 136 /** initialize representative set for type 137 * 138 * This ensures that TheoryModel::d_rep_set 139 * is initialized for type tn. In particular: 140 * (1) If tn is an uninitialized (unconstrained) 141 * uninterpreted sort, then we interpret it 142 * as a set of size one, 143 * (2) If tn is a "small" enumerable finite type, 144 * then we ensure that all its values are in 145 * TheoryModel::d_rep_set. 146 * 147 * Returns true if the initialization was complete, 148 * in that the set for tn in TheoryModel::d_rep_set 149 * has all representatives of type tn. 150 */ 151 bool initializeRepresentativesForType(TypeNode tn); 152 153 protected: 154 /** quant engine */ 155 QuantifiersEngine* d_qe; 156 /** list of quantifiers asserted in the current context */ 157 context::CDList<Node> d_forall_asserts; 158 /** quantified formulas marked as relevant */ 159 unsigned d_rlv_count; 160 std::map<Node, unsigned> d_forall_rlv; 161 std::vector<Node> d_forall_rlv_vec; 162 Node d_last_forall_rlv; 163 std::vector<Node> d_forall_rlv_assert; 164 /** get variable id */ 165 std::map<Node, std::map<Node, int> > d_quant_var_id; 166 /** process initialize model for term */ processInitializeModelForTerm(Node n)167 virtual void processInitializeModelForTerm(Node n) {} 168 /** process initialize quantifier */ processInitializeQuantifier(Node q)169 virtual void processInitializeQuantifier(Node q) {} 170 /** process initialize */ processInitialize(bool ispre)171 virtual void processInitialize(bool ispre) {} 172 173 private: 174 // list of inactive quantified formulas 175 std::map<TNode, bool> d_quant_active; 176 /** map from types to model basis terms */ 177 std::map<TypeNode, Node> d_model_basis_term; 178 /** map from ops to model basis terms */ 179 std::map<Node, Node> d_model_basis_op_term; 180 /** map from instantiation terms to their model basis equivalent */ 181 std::map<Node, Node> d_model_basis_body; 182 /** map from universal quantifiers to model basis terms */ 183 std::map<Node, std::vector<Node> > d_model_basis_terms; 184 /** compute model basis arg */ 185 void computeModelBasisArgAttribute(Node n); 186 };/* class FirstOrderModel */ 187 188 namespace fmcheck { 189 190 class Def; 191 192 class FirstOrderModelFmc : public FirstOrderModel 193 { 194 friend class FullModelChecker; 195 196 private: 197 /** models for UF */ 198 std::map<Node, Def * > d_models; 199 std::map<TypeNode, Node > d_type_star; 200 /** get current model value */ 201 void processInitializeModelForTerm(Node n) override; 202 203 public: 204 FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); 205 ~FirstOrderModelFmc() override; asFirstOrderModelFmc()206 FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; } 207 // initialize the model 208 void processInitialize(bool ispre) override; 209 Node getFunctionValue(Node op, const char* argPrefix ); 210 211 bool isStar(Node n); 212 Node getStar(TypeNode tn); 213 };/* class FirstOrderModelFmc */ 214 215 }/* CVC4::theory::quantifiers::fmcheck namespace */ 216 217 }/* CVC4::theory::quantifiers namespace */ 218 }/* CVC4::theory namespace */ 219 }/* CVC4 namespace */ 220 221 #endif /* __CVC4__FIRST_ORDER_MODEL_H */ 222