src/theory/quantifiers/term_database.h

   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 */
  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 subterms of n of maximal size to terms that exist in
 184    * the equality engine specified by qy.
 185    *
 186    * useEntailmentTests is whether to call the theory engine's entailmentTest
 187    * on literals n for which this call fails to find a term n' that is
 188    * equivalent to n, for increased precision. This is not frequently used.
 189    *
 190    * The vector exp stores the explanation for why n evaluates to that term,
 191    * that is, if this call returns a non-null node n', then:
 192    *   exp => n = n'
 193    *
 194    * If reqHasTerm, then we require that the returned term is a Boolean
 195    * combination of terms that exist in the equality engine used by this call.
 196    * If no such term is constructable, this call returns null. The motivation
 197    * for setting this to true is to "fail fast" if we require the return value
 198    * of this function to only involve existing terms. This is used e.g. in
 199    * the "propagating instances" portion of conflict-based instantiation
 200    * (quant_conflict_find.h).
 201    */
 202   Node evaluateTerm(TNode n,
 203                     std::vector<Node>& exp,
 204                     EqualityQuery* qy = NULL,
 205                     bool useEntailmentTests = false,
 206                     bool reqHasTerm = false);
 207   /** same as above, without exp */
 208   Node evaluateTerm(TNode n,
 209                     EqualityQuery* qy = NULL,
 210                     bool useEntailmentTests = false,
 211                     bool reqHasTerm = false);
 212   /** get entailed term
 213    *
 214   * If possible, returns a term n' such that:
 215   * (1) n' exists in the current equality engine (as specified by qy),
 216   * (2) n = n' is entailed in the current context.
 217   * It returns null if no such term can be found.
 218   * Wrt evaluateTerm, this version does not construct new terms, and
 219   * thus is less aggressive.
 220   */
 221   TNode getEntailedTerm(TNode n, EqualityQuery* qy = NULL);
 222   /** get entailed term
 223    *
 224   * If possible, returns a term n' such that:
 225   * (1) n' exists in the current equality engine (as specified by qy),
 226   * (2) n * subs = n' is entailed in the current context, where * is denotes
 227   * substitution application.
 228   * It returns null if no such term can be found.
 229   * subsRep is whether the substitution maps to terms that are representatives
 230   * according to qy.
 231   * Wrt evaluateTerm, this version does not construct new terms, and
 232   * thus is less aggressive.
 233   */
 234   TNode getEntailedTerm(TNode n,
 235                         std::map<TNode, TNode>& subs,
 236                         bool subsRep,
 237                         EqualityQuery* qy = NULL);
 238   /** is entailed
 239   * Checks whether the current context entails n with polarity pol, based on the
 240   * equality information qy.
 241   * Returns true if the entailment can be successfully shown.
 242   */
 243   bool isEntailed(TNode n, bool pol, EqualityQuery* qy = NULL);
 244   /** is entailed
 245    *
 246   * Checks whether the current context entails ( n * subs ) with polarity pol,
 247   * based on the equality information qy,
 248   * where * denotes substitution application.
 249   * subsRep is whether the substitution maps to terms that are representatives
 250   * according to qy.
 251   */
 252   bool isEntailed(TNode n,
 253                   std::map<TNode, TNode>& subs,
 254                   bool subsRep,
 255                   bool pol,
 256                   EqualityQuery* qy = NULL);
 257   /** is the term n active in the current context?
 258    *
 259   * By default, all terms are active. A term is inactive if:
 260   * (1) it is congruent to another term
 261   * (2) it is irrelevant based on the term database mode. This includes terms
 262   * that only appear in literals that are not relevant.
 263   * (3) it contains instantiation constants (used for CEGQI and cannot be used
 264   * in instantiation).
 265   * (4) it is explicitly set inactive by a call to setTermInactive(...).
 266   * We store whether a term is inactive in a SAT-context-dependent map.
 267   */
 268   bool isTermActive(Node n);
 269   /** set that term n is inactive in this context. */
 270   void setTermInactive(Node n);
 271   /** has term current
 272    *
 273   * This function is used in cases where we restrict which terms appear in the
 274   * database, such as for heuristics used in local theory extensions
 275   * and for --term-db-mode=relevant.
 276   * It returns whether the term n should be indexed in the current context.
 277   */
 278   bool hasTermCurrent(Node n, bool useMode = true);
 279   /** is term eligble for instantiation? */
 280   bool isTermEligibleForInstantiation(TNode n, TNode f, bool print = false);
 281   /** get eligible term in equivalence class of r */
 282   Node getEligibleTermInEqc(TNode r);
 283   /** is r a inst closure node?
 284    * This terminology was used for specifying
 285    * a particular status of nodes for
 286    * Bansal et al., CAV 2015.
 287    */
 288   bool isInstClosure(Node r);
 289
 290  private:
 291   /** reference to the quantifiers engine */
 292   QuantifiersEngine* d_quantEngine;
 293   /** terms processed */
 294   std::unordered_set< Node, NodeHashFunction > d_processed;
 295   /** terms processed */
 296   std::unordered_set< Node, NodeHashFunction > d_iclosure_processed;
 297   /** select op map */
 298   std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
 299   /** whether master equality engine is UF-inconsistent */
 300   bool d_consistent_ee;
 301   /** boolean terms */
 302   Node d_true;
 303   Node d_false;
 304   /** list of all operators */
 305   std::vector<Node> d_ops;
 306   /** map from operators to ground terms for that operator */
 307   std::map< Node, std::vector< Node > > d_op_map;
 308   /** map from type nodes to terms of that type */
 309   std::map< TypeNode, std::vector< Node > > d_type_map;
 310   /** map from type nodes to a fresh variable we introduced */
 311   std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv;
 312   /** inactive map */
 313   NodeBoolMap d_inactive_map;
 314   /** count of the number of non-redundant ground terms per operator */
 315   std::map< Node, int > d_op_nonred_count;
 316   /** mapping from terms to representatives of their arguments */
 317   std::map< TNode, std::vector< TNode > > d_arg_reps;
 318   /** map from operators to trie */
 319   std::map<Node, TNodeTrie> d_func_map_trie;
 320   std::map<Node, TNodeTrie> d_func_map_eqc_trie;
 321   /** mapping from operators to their representative relevant domains */
 322   std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom;
 323   /** has map */
 324   std::map< Node, bool > d_has_map;
 325   /** map from reps to a term in eqc in d_has_map */
 326   std::map< Node, Node > d_term_elig_eqc;
 327   /** set has term */
 328   void setHasTerm( Node n );
 329   /** helper for evaluate term */
 330   Node evaluateTerm2(TNode n,
 331                      std::map<TNode, Node>& visited,
 332                      std::vector<Node>& exp,
 333                      EqualityQuery* qy,
 334                      bool useEntailmentTests,
 335                      bool computeExp,
 336                      bool reqHasTerm);
 337   /** helper for get entailed term */
 338   TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
 339   /** helper for is entailed */
 340   bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
 341   /** compute uf eqc terms :
 342   * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
 343   */
 344   void computeUfEqcTerms( TNode f );
 345   /** compute uf terms
 346   * Ensure that an entry for f is in d_func_map_trie
 347   */
 348   void computeUfTerms( TNode f );
 349   /** compute arg reps
 350   * Ensure that an entry for n is in d_arg_reps
 351   */
 352   void computeArgReps(TNode n);
 353   //------------------------------higher-order term indexing
 354   /**
 355    * Map from non-variable function terms to the operator used to purify it in
 356    * this database. For details, see addTermHo.
 357    */
 358   std::map<Node, Node> d_ho_fun_op_purify;
 359   /**
 360    * Map from terms to the term that they purified. For details, see addTermHo.
 361    */
 362   std::map<Node, Node> d_ho_purify_to_term;
 363   /**
 364    * Map from terms in the domain of the above map to an equality between that
 365    * term and its range in the above map.
 366    */
 367   std::map<Node, Node> d_ho_purify_to_eq;
 368   /** a map from matchable operators to their representative */
 369   std::map< TNode, TNode > d_ho_op_rep;
 370   /** for each representative matchable operator, the list of other matchable operators in their equivalence class */
 371   std::map<TNode, std::vector<TNode> > d_ho_op_slaves;
 372   /** add term higher-order
 373    *
 374    * This registers additional terms corresponding to (possibly multiple)
 375    * purifications of a higher-order term n.
 376    *
 377    * Consider the example:
 378    *    g : Int -> Int, f : Int x Int -> Int
 379    *    constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3
 380    *    pattern: (g x)
 381    * where @ is HO_APPLY.
 382    * We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1).
 383    * With the standard registration in addTerm, we construct term indices for
 384    *   f, g, @ : Int x Int -> Int, @ : Int -> Int.
 385    * However, to match (g x) with (@ (@ f 0) 1), we require that
 386    *   [1] -> (@ (@ f 0) 1)
 387    * is an entry in the term index of g. To do this, we maintain a term
 388    * index for a fresh variable pfun, the purification variable for
 389    * (@ f 0). Thus, we register the term (psk 1) in the call to this function
 390    * for (@ (@ f 0) 1). This ensures that, when processing the equality
 391    * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry
 392    *   [1] -> (@ (@ f 0) 1)
 393    * is added to the term index of g, assuming g is the representative of
 394    * the equivalence class of g and pfun.
 395    *
 396    * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and
 397    * d_ho_purify_to_term[(@ (@ f 0) 1)] = (psk 1).
 398    */
 399   void addTermHo(Node n,
 400                  std::set<Node>& added,
 401                  bool withinQuant,
 402                  bool withinInstClosure);
 403   /** get operator representative */
 404   Node getOperatorRepresentative( TNode op ) const;
 405   //------------------------------end higher-order term indexing
 406 };/* class TermDb */
 407
 408 }/* CVC4::theory::quantifiers namespace */
 409 }/* CVC4::theory namespace */
 410 }/* CVC4 namespace */
 411
 412 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */