1 /********************* */ 2 /*! \file term_database.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Morgan Deters, 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 term database class 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H 18 #define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H 19 20 #include <map> 21 #include <unordered_set> 22 23 #include "expr/attribute.h" 24 #include "expr/node_trie.h" 25 #include "theory/quantifiers/quant_util.h" 26 #include "theory/theory.h" 27 #include "theory/type_enumerator.h" 28 29 namespace CVC4 { 30 namespace theory { 31 32 class QuantifiersEngine; 33 34 namespace inst{ 35 class Trigger; 36 class HigherOrderTrigger; 37 } 38 39 namespace quantifiers { 40 41 namespace fmcheck { 42 class FullModelChecker; 43 } 44 45 class TermDbSygus; 46 class QuantConflictFind; 47 class RelevantDomain; 48 class ConjectureGenerator; 49 class TermGenerator; 50 class TermGenEnv; 51 52 /** Term Database 53 * 54 * This class is a key utility used by 55 * a number of approaches for quantifier instantiation, 56 * including E-matching, conflict-based instantiation, 57 * and model-based instantiation. 58 * 59 * The primary responsibilities for this class are to : 60 * (1) Maintain a list of all ground terms that exist in the quantifier-free 61 * solvers, as notified through the master equality engine. 62 * (2) Build TNodeTrie objects that index all ground terms, per operator. 63 * 64 * Like other utilities, its reset(...) function is called 65 * at the beginning of full or last call effort checks. 66 * This initializes the database for the round. However, 67 * notice that TNodeTrie objects are computed 68 * lazily for performance reasons. 69 */ 70 class TermDb : public QuantifiersUtil { 71 friend class ::CVC4::theory::QuantifiersEngine; 72 // TODO: eliminate these 73 friend class ::CVC4::theory::quantifiers::ConjectureGenerator; 74 friend class ::CVC4::theory::quantifiers::TermGenEnv; 75 typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; 76 typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; 77 78 public: 79 TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe); 80 ~TermDb(); 81 /** presolve (called once per user check-sat) */ 82 void presolve(); 83 /** reset (calculate which terms are active) */ 84 bool reset(Theory::Effort effort) override; 85 /** register quantified formula */ 86 void registerQuantifier(Node q) override; 87 /** identify */ identify()88 std::string identify() const override { return "TermDb"; } 89 /** get number of operators */ 90 unsigned getNumOperators(); 91 /** get operator at index i */ 92 Node getOperator(unsigned i); 93 /** ground terms for operator 94 * Get the number of ground terms with operator f that have been added to the 95 * database 96 */ 97 unsigned getNumGroundTerms(Node f) const; 98 /** get ground term for operator 99 * Get the i^th ground term with operator f that has been added to the database 100 */ 101 Node getGroundTerm(Node f, unsigned i) const; 102 /** get num type terms 103 * Get the number of ground terms of tn that have been added to the database 104 */ 105 unsigned getNumTypeGroundTerms(TypeNode tn) const; 106 /** get type ground term 107 * Returns the i^th ground term of type tn 108 */ 109 Node getTypeGroundTerm(TypeNode tn, unsigned i) const; 110 /** get or make ground term 111 * Returns the first ground term of type tn, 112 * or makes one if none exist. 113 */ 114 Node getOrMakeTypeGroundTerm(TypeNode tn); 115 /** make fresh variable 116 * Returns a fresh variable of type tn. 117 * This will return only a single fresh 118 * variable per type. 119 */ 120 Node getOrMakeTypeFreshVariable(TypeNode tn); 121 /** add a term to the database 122 * withinQuant is whether n is within the body of a quantified formula 123 * withinInstClosure is whether n is within an inst-closure operator (see 124 * Bansal et al CAV 2015). 125 */ 126 void addTerm(Node n, 127 std::set<Node>& added, 128 bool withinQuant = false, 129 bool withinInstClosure = false); 130 /** get match operator for term n 131 * 132 * If n has a kind that we index, this function will 133 * typically return n.getOperator(). 134 * 135 * However, for parametric operators f, the match operator is an arbitrary 136 * chosen f-application. For example, consider array select: 137 * A : (Array Int Int) 138 * B : (Array Bool Int) 139 * We require that terms like (select A 1) and (select B 2) are indexed in 140 * separate 141 * data structures despite the fact that 142 * (select A 1).getOperator()==(select B 2).getOperator(). 143 * Hence, for the above terms, we may return: 144 * getMatchOperator( (select A 1) ) = (select A 1), and 145 * getMatchOperator( (select B 2) ) = (select B 2). 146 * The match operator is the first instance of an application of the parametric 147 * operator of its type. 148 * 149 * If n has a kind that we do not index (like PLUS), 150 * then this function returns Node::null(). 151 */ 152 Node getMatchOperator(Node n); 153 /** get term arg index for all f-applications in the current context */ 154 TNodeTrie* getTermArgTrie(Node f); 155 /** get the term arg trie for f-applications in the equivalence class of eqc. 156 */ 157 TNodeTrie* getTermArgTrie(Node eqc, Node f); 158 /** get congruent term 159 * If possible, returns a term t such that: 160 * (1) t is a term that is currently indexed by this database, 161 * (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk ), 162 * where ti is in the equivalence class of si for i=1...k. 163 */ 164 TNode getCongruentTerm(Node f, Node n); 165 /** get congruent term 166 * If possible, returns a term t such that: 167 * (1) t is a term that is currently indexed by this database, 168 * (2) t is of the form f( t1, ..., tk ) where ti is in the 169 * equivalence class of args[i] for i=1...k. 170 */ 171 TNode getCongruentTerm(Node f, std::vector<TNode>& args); 172 /** in relevant domain 173 * Returns true if there is at least one term t such that: 174 * (1) t is a term that is currently indexed by this database, 175 * (2) t is of the form f( t1, ..., tk ) and ti is in the 176 * equivalence class of r. 177 */ 178 bool inRelevantDomain(TNode f, unsigned i, TNode r); 179 /** evaluate term 180 * 181 * Returns a term n' such that n = n' is entailed based on the equality 182 * information qy. This function may generate new terms. In particular, 183 * we typically rewrite maximal 184 * subterms of n to terms that exist in the equality engine specified by qy. 185 * 186 * useEntailmentTests is whether to use the theory engine's entailmentCheck 187 * call, for increased precision. This is not frequently used. 188 */ 189 Node evaluateTerm(TNode n, 190 EqualityQuery* qy = NULL, 191 bool useEntailmentTests = false); 192 /** get entailed term 193 * 194 * If possible, returns a term n' such that: 195 * (1) n' exists in the current equality engine (as specified by qy), 196 * (2) n = n' is entailed in the current context. 197 * It returns null if no such term can be found. 198 * Wrt evaluateTerm, this version does not construct new terms, and 199 * thus is less aggressive. 200 */ 201 TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL); 202 /** get entailed term 203 * 204 * If possible, returns a term n' such that: 205 * (1) n' exists in the current equality engine (as specified by qy), 206 * (2) n * subs = n' is entailed in the current context, where * is denotes 207 * substitution application. 208 * It returns null if no such term can be found. 209 * subsRep is whether the substitution maps to terms that are representatives 210 * according to qy. 211 * Wrt evaluateTerm, this version does not construct new terms, and 212 * thus is less aggressive. 213 */ 214 TNode getEntailedTerm(TNode n, 215 std::map<TNode, TNode>& subs, 216 bool subsRep, 217 EqualityQuery* qy = NULL); 218 /** is entailed 219 * Checks whether the current context entails n with polarity pol, based on the 220 * equality information qy. 221 * Returns true if the entailment can be successfully shown. 222 */ 223 bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL); 224 /** is entailed 225 * 226 * Checks whether the current context entails ( n * subs ) with polarity pol, 227 * based on the equality information qy, 228 * where * denotes substitution application. 229 * subsRep is whether the substitution maps to terms that are representatives 230 * according to qy. 231 */ 232 bool isEntailed(TNode n, 233 std::map<TNode, TNode>& subs, 234 bool subsRep, 235 bool pol, 236 EqualityQuery* qy = NULL); 237 /** is the term n active in the current context? 238 * 239 * By default, all terms are active. A term is inactive if: 240 * (1) it is congruent to another term 241 * (2) it is irrelevant based on the term database mode. This includes terms 242 * that only appear in literals that are not relevant. 243 * (3) it contains instantiation constants (used for CEGQI and cannot be used 244 * in instantiation). 245 * (4) it is explicitly set inactive by a call to setTermInactive(...). 246 * We store whether a term is inactive in a SAT-context-dependent map. 247 */ 248 bool isTermActive(Node n); 249 /** set that term n is inactive in this context. */ 250 void setTermInactive(Node n); 251 /** has term current 252 * 253 * This function is used in cases where we restrict which terms appear in the 254 * database, such as for heuristics used in local theory extensions 255 * and for --term-db-mode=relevant. 256 * It returns whether the term n should be indexed in the current context. 257 */ 258 bool hasTermCurrent(Node n, bool useMode = true); 259 /** is term eligble for instantiation? */ 260 bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false); 261 /** get eligible term in equivalence class of r */ 262 Node getEligibleTermInEqc(TNode r); 263 /** is r a inst closure node? 264 * This terminology was used for specifying 265 * a particular status of nodes for 266 * Bansal et al., CAV 2015. 267 */ 268 bool isInstClosure(Node r); 269 270 private: 271 /** reference to the quantifiers engine */ 272 QuantifiersEngine* d_quantEngine; 273 /** terms processed */ 274 std::unordered_set< Node, NodeHashFunction > d_processed; 275 /** terms processed */ 276 std::unordered_set< Node, NodeHashFunction > d_iclosure_processed; 277 /** select op map */ 278 std::map< Node, std::map< TypeNode, Node > > d_par_op_map; 279 /** whether master equality engine is UF-inconsistent */ 280 bool d_consistent_ee; 281 /** boolean terms */ 282 Node d_true; 283 Node d_false; 284 /** list of all operators */ 285 std::vector<Node> d_ops; 286 /** map from operators to ground terms for that operator */ 287 std::map< Node, std::vector< Node > > d_op_map; 288 /** map from type nodes to terms of that type */ 289 std::map< TypeNode, std::vector< Node > > d_type_map; 290 /** map from type nodes to a fresh variable we introduced */ 291 std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv; 292 /** inactive map */ 293 NodeBoolMap d_inactive_map; 294 /** count of the number of non-redundant ground terms per operator */ 295 std::map< Node, int > d_op_nonred_count; 296 /** mapping from terms to representatives of their arguments */ 297 std::map< TNode, std::vector< TNode > > d_arg_reps; 298 /** map from operators to trie */ 299 std::map<Node, TNodeTrie> d_func_map_trie; 300 std::map<Node, TNodeTrie> d_func_map_eqc_trie; 301 /** mapping from operators to their representative relevant domains */ 302 std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom; 303 /** has map */ 304 std::map< Node, bool > d_has_map; 305 /** map from reps to a term in eqc in d_has_map */ 306 std::map< Node, Node > d_term_elig_eqc; 307 /** set has term */ 308 void setHasTerm( Node n ); 309 /** helper for evaluate term */ 310 Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ); 311 /** helper for get entailed term */ 312 TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); 313 /** helper for is entailed */ 314 bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ); 315 /** compute uf eqc terms : 316 * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes 317 */ 318 void computeUfEqcTerms( TNode f ); 319 /** compute uf terms 320 * Ensure that an entry for f is in d_func_map_trie 321 */ 322 void computeUfTerms( TNode f ); 323 /** compute arg reps 324 * Ensure that an entry for n is in d_arg_reps 325 */ 326 void computeArgReps(TNode n); 327 //------------------------------higher-order term indexing 328 /** 329 * Map from non-variable function terms to the operator used to purify it in 330 * this database. For details, see addTermHo. 331 */ 332 std::map<Node, Node> d_ho_fun_op_purify; 333 /** 334 * Map from terms to the term that they purified. For details, see addTermHo. 335 */ 336 std::map<Node, Node> d_ho_purify_to_term; 337 /** 338 * Map from terms in the domain of the above map to an equality between that 339 * term and its range in the above map. 340 */ 341 std::map<Node, Node> d_ho_purify_to_eq; 342 /** a map from matchable operators to their representative */ 343 std::map< TNode, TNode > d_ho_op_rep; 344 /** for each representative matchable operator, the list of other matchable operators in their equivalence class */ 345 std::map<TNode, std::vector<TNode> > d_ho_op_slaves; 346 /** add term higher-order 347 * 348 * This registers additional terms corresponding to (possibly multiple) 349 * purifications of a higher-order term n. 350 * 351 * Consider the example: 352 * g : Int -> Int, f : Int x Int -> Int 353 * constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3 354 * pattern: (g x) 355 * where @ is HO_APPLY. 356 * We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1). 357 * With the standard registration in addTerm, we construct term indices for 358 * f, g, @ : Int x Int -> Int, @ : Int -> Int. 359 * However, to match (g x) with (@ (@ f 0) 1), we require that 360 * [1] -> (@ (@ f 0) 1) 361 * is an entry in the term index of g. To do this, we maintain a term 362 * index for a fresh variable pfun, the purification variable for 363 * (@ f 0). Thus, we register the term (psk 1) in the call to this function 364 * for (@ (@ f 0) 1). This ensures that, when processing the equality 365 * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry 366 * [1] -> (@ (@ f 0) 1) 367 * is added to the term index of g, assuming g is the representative of 368 * the equivalence class of g and pfun. 369 * 370 * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and 371 * d_ho_purify_to_term[(@ (@ f 0) 1)] = (psk 1). 372 */ 373 void addTermHo(Node n, 374 std::set<Node>& added, 375 bool withinQuant, 376 bool withinInstClosure); 377 /** get operator representative */ 378 Node getOperatorRepresentative( TNode op ) const; 379 //------------------------------end higher-order term indexing 380 };/* class TermDb */ 381 382 }/* CVC4::theory::quantifiers namespace */ 383 }/* CVC4::theory namespace */ 384 }/* CVC4 namespace */ 385 386 #endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ 387