From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 14 Aug 2019 15:37:03 +0000 (-0500)
Subject: Fix issue related to higher-order purification in term database (#3157)
X-Git-Tag: cvc5-1.0.0~4017
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4924138b1431d7bbc263bc4a6c63510926da3c72;p=cvc5.git

Fix issue related to higher-order purification in term database (#3157)
---

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 989609a76..84147bf6b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1039,7 +1039,21 @@ bool TermDb::reset( Theory::Effort effort ){
         }
         Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
         ee->assertEquality(eq, true, eq);
-        Assert(ee->consistent());
+        if (!ee->consistent())
+        {
+          // In some rare cases, purification functions (in the domain of
+          // d_ho_purify_to_term) may escape the term database. For example,
+          // matching algorithms may construct instantiations involving these
+          // functions. As a result, asserting these equalities internally may
+          // cause a conflict. In this case, we insist that the purification
+          // equality is sent out as a lemma here.
+          Trace("term-db-lemma")
+              << "Purify equality lemma: " << eq << std::endl;
+          d_quantEngine->addLemma(eq);
+          d_quantEngine->setConflict();
+          d_consistent_ee = false;
+          return false;
+        }
       }
     }
   }
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index d58d33673..f92bce8bd 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -271,11 +271,15 @@ class TermDb : public QuantifiersUtil {
   void setTermInactive(Node n);
   /** has term current
    *
-  * This function is used in cases where we restrict which terms appear in the
-  * database, such as for heuristics used in local theory extensions
-  * and for --term-db-mode=relevant.
-  * It returns whether the term n should be indexed in the current context.
-  */
+   * This function is used in cases where we restrict which terms appear in the
+   * database, such as for heuristics used in local theory extensions
+   * and for --term-db-mode=relevant.
+   * It returns whether the term n should be indexed in the current context.
+   *
+   * If the argument useMode is true, then this method returns a value based on
+   * the option options::termDbMode().
+   * Otherwise, it returns the lookup in the map d_has_map.
+   */
   bool hasTermCurrent(Node n, bool useMode = true);
   /** is term eligble for instantiation? */
   bool isTermEligibleForInstantiation(TNode n, TNode f);
@@ -387,7 +391,7 @@ class TermDb : public QuantifiersUtil {
    *   [1] -> (@ (@ f 0) 1)
    * is an entry in the term index of g. To do this, we maintain a term
    * index for a fresh variable pfun, the purification variable for
-   * (@ f 0). Thus, we register the term (psk 1) in the call to this function
+   * (@ f 0). Thus, we register the term (pfun 1) in the call to this function
    * for (@ (@ f 0) 1). This ensures that, when processing the equality
    * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry
    *   [1] -> (@ (@ f 0) 1)
@@ -395,7 +399,7 @@ class TermDb : public QuantifiersUtil {
    * the equivalence class of g and pfun.
    *
    * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and
-   * d_ho_purify_to_term[(@ (@ f 0) 1)] = (psk 1).
+   * d_ho_purify_to_term[(pfun 1)] = (@ (@ f 0) 1).
    */
   void addTermHo(Node n,
                  std::set<Node>& added,