mergecav2019strings_countRewRed

1 files changed, 40 insertions, 14 deletions

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index cc9a24d08..148a18958 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
-#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
 #include <map>
 #include <unordered_set>
@@ -178,17 +178,37 @@ class TermDb : public QuantifiersUtil {
   bool inRelevantDomain(TNode f, unsigned i, TNode r);
   /** evaluate term
    *
-  * Returns a term n' such that n = n' is entailed based on the equality
-  * information qy.  This function may generate new terms. In particular,
-  * we typically rewrite maximal
-  * subterms of n to terms that exist in the equality engine specified by qy.
-  *
-  * useEntailmentTests is whether to use the theory engine's entailmentCheck
-  * call, for increased precision. This is not frequently used.
-  */
+   * Returns a term n' such that n = n' is entailed based on the equality
+   * information qy.  This function may generate new terms. In particular,
+   * we typically rewrite subterms of n of maximal size to terms that exist in
+   * the equality engine specified by qy.
+   *
+   * useEntailmentTests is whether to call the theory engine's entailmentTest
+   * on literals n for which this call fails to find a term n' that is
+   * equivalent to n, for increased precision. This is not frequently used.
+   *
+   * The vector exp stores the explanation for why n evaluates to that term,
+   * that is, if this call returns a non-null node n', then:
+   *   exp => n = n'
+   *
+   * If reqHasTerm, then we require that the returned term is a Boolean
+   * combination of terms that exist in the equality engine used by this call.
+   * If no such term is constructable, this call returns null. The motivation
+   * for setting this to true is to "fail fast" if we require the return value
+   * of this function to only involve existing terms. This is used e.g. in
+   * the "propagating instances" portion of conflict-based instantiation
+   * (quant_conflict_find.h).
+   */
+  Node evaluateTerm(TNode n,
+                    std::vector<Node>& exp,
+                    EqualityQuery* qy = NULL,
+                    bool useEntailmentTests = false,
+                    bool reqHasTerm = false);
+  /** same as above, without exp */
   Node evaluateTerm(TNode n,
                     EqualityQuery* qy = NULL,
-                    bool useEntailmentTests = false);
+                    bool useEntailmentTests = false,
+                    bool reqHasTerm = false);
   /** get entailed term
    *
   * If possible, returns a term n' such that:
@@ -307,7 +327,13 @@ class TermDb : public QuantifiersUtil {
   /** set has term */
   void setHasTerm( Node n );
   /** helper for evaluate term */
-  Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests );
+  Node evaluateTerm2(TNode n,
+                     std::map<TNode, Node>& visited,
+                     std::vector<Node>& exp,
+                     EqualityQuery* qy,
+                     bool useEntailmentTests,
+                     bool computeExp,
+                     bool reqHasTerm);
   /** helper for get entailed term */
   TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
   /** helper for is entailed */
@@ -383,4 +409,4 @@ class TermDb : public QuantifiersUtil {
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
+#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */