1 /********************* */ 2 /*! \file inst_propagator.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Mathias Preiner, 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 Propagate mechanism for instantiations 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H 18 #define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H 19 20 #include <iostream> 21 #include <map> 22 #include <string> 23 #include <vector> 24 #include "expr/node.h" 25 #include "expr/node_trie.h" 26 #include "expr/type_node.h" 27 #include "theory/quantifiers/instantiate.h" 28 #include "theory/quantifiers_engine.h" 29 30 namespace CVC4 { 31 namespace theory { 32 namespace quantifiers { 33 34 class EqualityQueryInstProp : public EqualityQuery { 35 private: 36 /** pointer to quantifiers engine */ 37 QuantifiersEngine* d_qe; 38 public: 39 EqualityQueryInstProp( QuantifiersEngine* qe ); ~EqualityQueryInstProp()40 ~EqualityQueryInstProp(){}; 41 /** reset */ 42 bool reset(Theory::Effort e) override; 43 /* Called for new quantifiers */ registerQuantifier(Node q)44 void registerQuantifier(Node q) override {} 45 /** identify */ identify()46 std::string identify() const override { return "EqualityQueryInstProp"; } 47 /** extends engine */ extendsEngine()48 bool extendsEngine() override { return true; } 49 /** contains term */ 50 bool hasTerm(Node a) override; 51 /** get the representative of the equivalence class of a */ 52 Node getRepresentative(Node a) override; 53 /** returns true if a and b are equal in the current context */ 54 bool areEqual(Node a, Node b) override; 55 /** returns true is a and b are disequal in the current context */ 56 bool areDisequal(Node a, Node b) override; 57 /** get the equality engine associated with this query */ 58 eq::EqualityEngine* getEngine() override; 59 /** get the equivalence class of a */ 60 void getEquivalenceClass(Node a, std::vector<Node>& eqc) override; 61 /** get congruent term */ 62 TNode getCongruentTerm(Node f, std::vector<TNode>& args) override; 63 64 public: 65 /** get the representative of the equivalence class of a, with explanation */ 66 Node getRepresentativeExp( Node a, std::vector< Node >& exp ); 67 /** returns true if a and b are equal in the current context */ 68 bool areEqualExp( Node a, Node b, std::vector< Node >& exp ); 69 /** returns true is a and b are disequal in the current context */ 70 bool areDisequalExp( Node a, Node b, std::vector< Node >& exp ); 71 /** get congruent term */ 72 TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ); 73 private: 74 /** term index */ 75 std::map<Node, TNodeTrie> d_uf_func_map_trie; 76 /** union find for terms beyond what is stored in equality engine */ 77 std::map<Node, Node> d_uf; 78 std::map<Node, std::vector<Node> > d_uf_exp; 79 Node getUfRepresentative(Node a, std::vector<Node>& exp); 80 /** disequality list, stores explanations */ 81 std::map<Node, std::map<Node, std::vector<Node> > > d_diseq_list; 82 /** add arg */ 83 void addArgument(Node n, 84 std::vector<Node>& args, 85 std::vector<Node>& watch, 86 bool is_watch); 87 /** register term */ 88 void registerUfTerm(TNode n); 89 90 public: 91 enum { 92 STATUS_CONFLICT, 93 STATUS_MERGED_KNOWN, 94 STATUS_MERGED_UNKNOWN, 95 STATUS_NONE, 96 }; 97 /** set equal */ 98 int setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ); 99 Node d_true; 100 Node d_false; 101 public: 102 //for explanations 103 static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 ); 104 //for watch list 105 static void setWatchList( Node n, std::vector< Node >& watch, std::map< Node, std::vector< Node > >& watch_list_out ); 106 static void collectWatchList( Node n, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& watch_list ); 107 108 Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< int, std::map< Node, Node > >& visited, 109 bool hasPol, bool pol, std::map< Node, std::vector< Node > >& watch_list_out, std::vector< Node >& props ); 110 bool isPropagateLiteral( Node n ); 111 }; 112 113 class InstPropagator : public QuantifiersUtil { 114 private: 115 /** pointer to quantifiers engine */ 116 QuantifiersEngine* d_qe; 117 /** notify class */ 118 class InstantiationNotifyInstPropagator : public InstantiationNotify { 119 InstPropagator& d_ip; 120 public: InstantiationNotifyInstPropagator(InstPropagator & ip)121 InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {} notifyInstantiation(QuantifiersModule::QEffort quant_e,Node q,Node lem,std::vector<Node> & terms,Node body)122 bool notifyInstantiation(QuantifiersModule::QEffort quant_e, 123 Node q, 124 Node lem, 125 std::vector<Node>& terms, 126 Node body) override 127 { 128 return d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); 129 } filterInstantiations()130 void filterInstantiations() override { d_ip.filterInstantiations(); } 131 }; 132 InstantiationNotifyInstPropagator d_notify; 133 /** notify instantiation method */ 134 bool notifyInstantiation(QuantifiersModule::QEffort quant_e, 135 Node q, 136 Node lem, 137 std::vector<Node>& terms, 138 Node body); 139 /** remove instance ids */ 140 void filterInstantiations(); 141 /** allocate instantiation */ 142 unsigned allocateInstantiation( Node q, Node lem, std::vector< Node >& terms, Node body ); 143 /** equality query */ 144 EqualityQueryInstProp d_qy; 145 class InstInfo { 146 public: 147 bool d_active; 148 Node d_q; 149 Node d_lem; 150 std::vector< Node > d_terms; 151 // the current entailed body 152 Node d_curr; 153 //explanation for current entailed body 154 std::vector< Node > d_curr_exp; 155 void init( Node q, Node lem, std::vector< Node >& terms, Node body ); 156 }; 157 /** instantiation count/info */ 158 unsigned d_icount; 159 std::map< unsigned, InstInfo > d_ii; 160 std::map< Node, unsigned > d_conc_to_id[2]; 161 /** are we in conflict */ 162 bool d_conflict; 163 /** watch list */ 164 std::map< Node, std::map< unsigned, bool > > d_watch_list; 165 /** update list */ 166 std::vector< unsigned > d_update_list; 167 /** relevant instances */ 168 std::map< unsigned, bool > d_relevant_inst; 169 bool d_has_relevant_inst; 170 private: 171 bool update( unsigned id, InstInfo& i, bool firstTime = false ); 172 void propagate( Node a, Node b, bool pol, std::vector< Node >& exp ); 173 void conflict( std::vector< Node >& exp ); 174 bool cacheConclusion( unsigned id, Node body, int prop_index = 0 ); 175 void addRelevantInstances( std::vector< Node >& exp, const char * c ); 176 void debugPrintExplanation( std::vector< Node >& exp, const char * c ); 177 public: 178 InstPropagator( QuantifiersEngine* qe ); ~InstPropagator()179 ~InstPropagator(){} 180 /** reset */ 181 bool reset(Theory::Effort e) override; 182 /* Called for new quantifiers */ registerQuantifier(Node q)183 void registerQuantifier(Node q) override {} 184 /** identify */ identify()185 std::string identify() const override { return "InstPropagator"; } 186 /** get the notify mechanism */ getInstantiationNotify()187 InstantiationNotify* getInstantiationNotify() { return &d_notify; } 188 }; 189 190 } 191 } 192 } 193 194 #endif 195