1 /********************* */ 2 /*! \file full_model_check.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Morgan Deters, Mathias Preiner 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 Full model check class 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H 18 #define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H 19 20 #include "theory/quantifiers/fmf/model_builder.h" 21 #include "theory/quantifiers/first_order_model.h" 22 23 namespace CVC4 { 24 namespace theory { 25 namespace quantifiers { 26 namespace fmcheck { 27 28 29 class FirstOrderModelFmc; 30 class FullModelChecker; 31 32 class EntryTrie 33 { 34 private: 35 int d_complete; 36 public: EntryTrie()37 EntryTrie() : d_complete(-1), d_data(-1){} 38 std::map<Node,EntryTrie> d_child; 39 int d_data; reset()40 void reset() { d_data = -1; d_child.clear(); d_complete = -1; } 41 void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 ); 42 bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 ); 43 int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 ); 44 void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true ); 45 };/* class EntryTrie */ 46 47 48 class Def 49 { 50 public: 51 EntryTrie d_et; 52 //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative 53 std::vector< Node > d_cond; 54 //value is returned by FullModelChecker::getRepresentative 55 std::vector< Node > d_value; 56 void basic_simplify( FirstOrderModelFmc * m ); 57 private: 58 enum { 59 status_unk, 60 status_redundant, 61 status_non_redundant 62 }; 63 std::vector< int > d_status; 64 bool d_has_simplified; 65 public: Def()66 Def() : d_has_simplified(false){} reset()67 void reset() { 68 d_et.reset(); 69 d_cond.clear(); 70 d_value.clear(); 71 d_status.clear(); 72 d_has_simplified = false; 73 } 74 bool addEntry( FirstOrderModelFmc * m, Node c, Node v); 75 Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ); 76 int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ); 77 void simplify( FullModelChecker * mc, FirstOrderModelFmc * m ); 78 void debugPrint(const char * tr, Node op, FullModelChecker * m); 79 };/* class Def */ 80 81 82 class FullModelChecker : public QModelBuilder 83 { 84 protected: 85 Node d_true; 86 Node d_false; 87 std::map<TypeNode, std::map< Node, int > > d_rep_ids; 88 std::map<Node, Def > d_quant_models; 89 std::map<Node, Node > d_quant_cond; 90 std::map< TypeNode, Node > d_array_cond; 91 std::map< Node, Node > d_array_term_cond; 92 std::map< Node, std::vector< int > > d_star_insts; 93 //--------------------for preinitialization 94 /** preInitializeType 95 * 96 * This function ensures that the model fm is properly initialized with 97 * respect to type tn. 98 * 99 * In particular, this class relies on the use of "model basis" terms, which 100 * are distinguished terms that are used to specify default values for 101 * uninterpreted functions. This method enforces that the model basis term 102 * occurs in the model for each relevant type T, where a type T is relevant 103 * if a bound variable is of type T, or an uninterpreted function has an 104 * argument or a return value of type T. 105 */ 106 void preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ); 107 /** for each type, an equivalence class of that type from the model */ 108 std::map<TypeNode, Node> d_preinitialized_eqc; 109 /** map from types to whether we have called the method above */ 110 std::map<TypeNode, bool> d_preinitialized_types; 111 //--------------------end for preinitialization 112 Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); 113 bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); 114 private: 115 void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ); 116 117 void doNegate( Def & dc ); 118 void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ); 119 void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v); 120 void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc ); 121 122 void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, 123 Def & df, std::vector< Def > & dc, int index, 124 std::vector< Node > & cond, std::vector<Node> & val ); 125 void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, 126 std::map< int, Node > & entries, int index, 127 std::vector< Node > & cond, std::vector< Node > & val, 128 EntryTrie & curr); 129 130 void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, 131 std::vector< Def > & dc, int index, 132 std::vector< Node > & cond, std::vector<Node> & val ); 133 int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); 134 bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); 135 Node mkCond( std::vector< Node > & cond ); 136 Node mkCondDefault( FirstOrderModelFmc * fm, Node f ); 137 void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ); 138 void mkCondVec( Node n, std::vector< Node > & cond ); 139 Node evaluateInterpreted( Node n, std::vector< Node > & vals ); 140 Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); 141 public: 142 FullModelChecker( context::Context* c, QuantifiersEngine* qe ); 143 144 void debugPrintCond(const char * tr, Node n, bool dispStar = false); 145 void debugPrint(const char * tr, Node n, bool dispStar = false); 146 147 int doExhaustiveInstantiation(FirstOrderModel* fm, 148 Node f, 149 int effort) override; 150 151 Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ); 152 153 /** process build model */ 154 bool preProcessBuildModel(TheoryModel* m) override; 155 bool processBuildModel(TheoryModel* m) override; 156 157 bool useSimpleModels(); 158 };/* class FullModelChecker */ 159 160 }/* CVC4::theory::quantifiers::fmcheck namespace */ 161 }/* CVC4::theory::quantifiers namespace */ 162 }/* CVC4::theory namespace */ 163 }/* CVC4 namespace */ 164 165 #endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ 166