1 /********************* */ 2 /*! \file theory_sets_rels.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Paul Meng, Tim King 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 Sets theory implementation. 13 ** 14 ** Extension to Sets theory. 15 **/ 16 17 #ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_ 18 #define SRC_THEORY_SETS_THEORY_SETS_RELS_H_ 19 20 #include <unordered_set> 21 22 #include "context/cdhashset.h" 23 #include "context/cdlist.h" 24 #include "theory/sets/rels_utils.h" 25 #include "theory/theory.h" 26 #include "theory/uf/equality_engine.h" 27 28 namespace CVC4 { 29 namespace theory { 30 namespace sets { 31 32 class TheorySets; 33 34 35 class TupleTrie { 36 public: 37 /** the data */ 38 std::map< Node, TupleTrie > d_data; 39 public: 40 std::vector<Node> findTerms( std::vector< Node >& reps, int argIndex = 0 ); 41 std::vector<Node> findSuccessors( std::vector< Node >& reps, int argIndex = 0 ); 42 Node existsTerm( std::vector< Node >& reps, int argIndex = 0 ); 43 bool addTerm( Node n, std::vector< Node >& reps, int argIndex = 0 ); 44 void debugPrint( const char * c, Node n, unsigned depth = 0 ); clear()45 void clear() { d_data.clear(); } 46 };/* class TupleTrie */ 47 48 class TheorySetsRels { 49 typedef context::CDList<Node> NodeList; 50 typedef context::CDHashSet< Node, NodeHashFunction > NodeSet; 51 typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; 52 53 public: 54 TheorySetsRels(context::Context* c, 55 context::UserContext* u, 56 eq::EqualityEngine*, 57 context::CDO<bool>*, 58 TheorySets&); 59 60 ~TheorySetsRels(); 61 void check(Theory::Effort); 62 void doPendingLemmas(); 63 64 bool isRelationKind( Kind k ); 65 private: 66 /** equivalence class info 67 * d_mem tuples that are members of this equivalence class 68 * d_not_mem tuples that are not members of this equivalence class 69 * d_tp is a node of kind TRANSPOSE (if any) in this equivalence class, 70 * d_pt is a node of kind PRODUCT (if any) in this equivalence class, 71 * d_tc is a node of kind TCLOSURE (if any) in this equivalence class, 72 */ 73 class EqcInfo 74 { 75 public: 76 EqcInfo( context::Context* c ); ~EqcInfo()77 ~EqcInfo(){} 78 NodeSet d_mem; 79 NodeMap d_mem_exp; 80 context::CDO< Node > d_tp; 81 context::CDO< Node > d_pt; 82 context::CDO< Node > d_tc; 83 context::CDO< Node > d_rel_tc; 84 }; 85 86 private: 87 88 /** has eqc info */ hasEqcInfo(TNode n)89 bool hasEqcInfo( TNode n ) { return d_eqc_info.find( n )!=d_eqc_info.end(); } 90 91 eq::EqualityEngine *d_eqEngine; 92 context::CDO<bool> *d_conflict; 93 TheorySets& d_sets_theory; 94 95 /** True and false constant nodes */ 96 Node d_trueNode; 97 Node d_falseNode; 98 99 /** Facts and lemmas to be sent to EE */ 100 NodeList d_pending_merge; 101 NodeSet d_lemmas_produced; 102 NodeSet d_shared_terms; 103 std::vector< Node > d_lemmas_out; 104 std::map< Node, Node > d_pending_facts; 105 106 107 std::unordered_set< Node, NodeHashFunction > d_rel_nodes; 108 std::map< Node, std::vector<Node> > d_tuple_reps; 109 std::map< Node, TupleTrie > d_membership_trie; 110 111 /** Symbolic tuple variables that has been reduced to concrete ones */ 112 std::unordered_set< Node, NodeHashFunction > d_symbolic_tuples; 113 114 /** Mapping between relation and its member representatives */ 115 std::map< Node, std::vector< Node > > d_rReps_memberReps_cache; 116 117 /** Mapping between relation and its member representatives explanation */ 118 std::map< Node, std::vector< Node > > d_rReps_memberReps_exp_cache; 119 120 /** Mapping between a relation representative and its equivalent relations involving relational operators */ 121 std::map< Node, std::map<kind::Kind_t, std::vector<Node> > > d_terms_cache; 122 123 /** Mapping between transitive closure relation TC(r) and its TC graph constructed based on the members of r*/ 124 std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_rRep_tcGraph; 125 std::map< Node, std::map< Node, std::unordered_set<Node, NodeHashFunction> > > d_tcr_tcGraph; 126 std::map< Node, std::map< Node, Node > > d_tcr_tcGraph_exps; 127 std::map< Node, std::vector< Node > > d_tc_lemmas_last; 128 129 std::map< Node, EqcInfo* > d_eqc_info; 130 131 public: 132 /** Standard effort notifications */ 133 void eqNotifyNewClass(Node t); 134 void eqNotifyPostMerge(Node t1, Node t2); 135 136 private: 137 138 /** Methods used in standard effort */ 139 void doPendingMerge(); 140 void sendInferProduct(Node member, Node pt_rel, Node exp); 141 void sendInferTranspose(Node t1, Node t2, Node exp ); 142 void sendInferTClosure( Node mem_rep, EqcInfo* ei ); 143 void sendMergeInfer( Node fact, Node reason, const char * c ); 144 EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); 145 146 /** Methods used in full effort */ 147 void check(); 148 void collectRelsInfo(); 149 void applyTransposeRule( std::vector<Node> tp_terms ); 150 void applyTransposeRule( Node rel, Node rel_rep, Node exp ); 151 void applyProductRule( Node rel, Node rel_rep, Node exp ); 152 void applyJoinRule( Node rel, Node rel_rep, Node exp); 153 void applyJoinImageRule( Node mem_rep, Node rel_rep, Node exp); 154 void applyIdenRule( Node mem_rep, Node rel_rep, Node exp); 155 void applyTCRule( Node mem, Node rel, Node rel_rep, Node exp); 156 void buildTCGraphForRel( Node tc_rel ); 157 void doTCInference(); 158 void doTCInference( std::map< Node, std::unordered_set<Node, NodeHashFunction> > rel_tc_graph, std::map< Node, Node > rel_tc_graph_exps, Node tc_rel ); 159 void doTCInference(Node tc_rel, std::vector< Node > reasons, std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, 160 std::map< Node, Node >& rel_tc_graph_exps, Node start_node_rep, Node cur_node_rep, std::unordered_set< Node, NodeHashFunction >& seen ); 161 162 void composeMembersForRels( Node ); 163 void computeMembersForBinOpRel( Node ); 164 void computeMembersForIdenTerm( Node ); 165 void computeMembersForUnaryOpRel( Node ); 166 void computeMembersForJoinImageTerm( Node ); 167 168 bool isTCReachable( Node mem_rep, Node tc_rel ); 169 void isTCReachable( Node start, Node dest, std::unordered_set<Node, NodeHashFunction>& hasSeen, 170 std::map< Node, std::unordered_set< Node, NodeHashFunction > >& tc_graph, bool& isReachable ); 171 172 173 void addSharedTerm( TNode n ); 174 void sendInfer( Node fact, Node exp, const char * c ); 175 void sendLemma( Node fact, Node reason, const char * c ); 176 void doTCLemmas(); 177 178 /** Helper functions */ 179 bool holds( Node ); 180 bool hasTerm( Node a ); 181 void makeSharedTerm( Node ); 182 void reduceTupleVar( Node ); 183 bool hasMember( Node, Node ); 184 void computeTupleReps( Node ); 185 bool areEqual( Node a, Node b ); 186 Node getRepresentative( Node t ); 187 bool exists( std::vector<Node>&, Node ); 188 inline void addToMembershipDB( Node, Node, Node ); 189 static void printNodeMap(const char* fst, 190 const char* snd, 191 const NodeMap& map); 192 inline Node constructPair(Node tc_rep, Node a, Node b); 193 void addToMap( std::map< Node, std::vector<Node> >&, Node, Node ); 194 bool safelyAddToMap( std::map< Node, std::vector<Node> >&, Node, Node ); isRel(Node n)195 bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();} 196 }; 197 198 199 }/* CVC4::theory::sets namespace */ 200 }/* CVC4::theory namespace */ 201 }/* CVC4 namespace */ 202 203 204 205 #endif /* SRC_THEORY_SETS_THEORY_SETS_RELS_H_ */ 206