Make alpha equivalence user context dependent (#7889)

Fixes #5373

Issues were occurring due to using quantified formulas in alpha equivalence that were stale.

This also removes spurious warnings from quantifier elimination (dropping the "strict" requirement, which unnecessarily warns if we are in a non-arithmetic logic).

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index a6036485fb9d48754558b634024a5de6e376dad4..868fdd028c6c3604df0abe4b2da46378533e5d30 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7466,7 +7466,7 @@ Term Solver::getQuantifierElimination(const Term& q) const
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(q);
   //////// all checks before this line
-  return Term(this, d_slv->getQuantifierElimination(q.getNode(), true, true));
+  return Term(this, d_slv->getQuantifierElimination(q.getNode(), true));
   ////////
   CVC5_API_TRY_CATCH_END;
 }
@@ -7476,7 +7476,7 @@ Term Solver::getQuantifierEliminationDisjunct(const Term& q) const
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(q);
   //////// all checks before this line
-  return Term(this, d_slv->getQuantifierElimination(q.getNode(), false, true));
+  return Term(this, d_slv->getQuantifierElimination(q.getNode(), false));
   ////////
   CVC5_API_TRY_CATCH_END;
 }

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 4bb3bfabf8cb3bb3f5561cffd1a787be11bf562a..97774a739fc71a1ad5b86a27291e1c03c9543af5 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1622,16 +1622,10 @@ bool SolverEngine::getSubsolverSynthSolutions(std::map<Node, Node>& solMap)
   return d_sygusSolver->getSubsolverSynthSolutions(solMap);
 }
 
-Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
+Node SolverEngine::getQuantifierElimination(Node q, bool doFull)
 {
   SolverEngineScope smts(this);
   finishInit();
-  const LogicInfo& logic = getLogicInfo();
-  if (!logic.isPure(THEORY_ARITH) && strict)
-  {
-    d_env->warning() << "Unexpected logic for quantifier elimination " << logic
-              << endl;
-  }
   return d_quantElimSolver->getQuantifierElimination(
       *d_asserts, q, doFull, d_isInternalSubsolver);
 }

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 99d2502b912d2f44ba7114eda96748e524173841..dd98c674ee421106b1f05a34b3be865958eaa3b8 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -617,13 +617,8 @@ class CVC5_EXPORT SolverEngine
    * extended command get-qe-disjunct, which can be used
    * for incrementally computing the result of a
    * quantifier elimination.
-   *
-   * The argument strict is whether to output
-   * warnings, such as when an unexpected logic is used.
-   *
-   * throw@ Exception
    */
-  Node getQuantifierElimination(Node q, bool doFull, bool strict = true);
+  Node getQuantifierElimination(Node q, bool doFull);
 
   /**
    * This method asks this SMT engine to find an interpolant with respect to

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 0c9a5ba46dfbdc6208d7fef8385eecb251cecd59..d36343c6bd7cd741c50dd56304245fcca6011b78 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -32,7 +32,13 @@ struct sortTypeOrder {
   }
 };
 
+AlphaEquivalenceTypeNode::AlphaEquivalenceTypeNode(context::Context* c)
+    : d_quant(c)
+{
+}
+
 Node AlphaEquivalenceTypeNode::registerNode(
+    context::Context* c,
     Node q,
     Node t,
     std::vector<TypeNode>& typs,
@@ -40,25 +46,47 @@ Node AlphaEquivalenceTypeNode::registerNode(
 {
   AlphaEquivalenceTypeNode* aetn = this;
   size_t index = 0;
+  std::map<std::pair<TypeNode, size_t>,
+           std::unique_ptr<AlphaEquivalenceTypeNode>>::iterator itc;
   while (index < typs.size())
   {
     TypeNode curr = typs[index];
     Assert(typCount.find(curr) != typCount.end());
     Trace("aeq-debug") << "[" << curr << " " << typCount[curr] << "] ";
     std::pair<TypeNode, size_t> key(curr, typCount[curr]);
-    aetn = &(aetn->d_children[key]);
+    itc = aetn->d_children.find(key);
+    if (itc == aetn->d_children.end())
+    {
+      aetn->d_children[key] = std::make_unique<AlphaEquivalenceTypeNode>(c);
+      aetn = aetn->d_children[key].get();
+    }
+    else
+    {
+      aetn = itc->second.get();
+    }
     index = index + 1;
   }
   Trace("aeq-debug") << " : ";
-  std::map<Node, Node>::iterator it = aetn->d_quant.find(t);
-  if (it != aetn->d_quant.end())
+  NodeMap::iterator it = aetn->d_quant.find(t);
+  if (it != aetn->d_quant.end() && !it->second.isNull())
   {
+    Trace("aeq-debug") << it->second << std::endl;
     return it->second;
   }
+  Trace("aeq-debug") << "(new)" << std::endl;
   aetn->d_quant[t] = q;
   return q;
 }
 
+AlphaEquivalenceDb::AlphaEquivalenceDb(context::Context* c,
+                                       expr::TermCanonize* tc,
+                                       bool sortCommChildren)
+    : d_context(c),
+      d_ae_typ_trie(c),
+      d_tc(tc),
+      d_sortCommutativeOpChildren(sortCommChildren)
+{
+}
 Node AlphaEquivalenceDb::addTerm(Node q)
 {
   Assert(q.getKind() == FORALL);
@@ -129,7 +157,7 @@ Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q)
   sto.d_tu = d_tc;
   std::sort( typs.begin(), typs.end(), sto );
   Trace("aeq-debug") << "  ";
-  Node ret = d_ae_typ_trie.registerNode(q, t, typs, typCount);
+  Node ret = d_ae_typ_trie.registerNode(d_context, q, t, typs, typCount);
   Trace("aeq") << "  ...result : " << ret << std::endl;
   return ret;
 }
@@ -137,7 +165,7 @@ Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q)
 AlphaEquivalence::AlphaEquivalence(Env& env)
     : EnvObj(env),
       d_termCanon(),
-      d_aedb(&d_termCanon, true),
+      d_aedb(userContext(), &d_termCanon, true),
       d_pnm(env.getProofNodeManager()),
       d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr)
 {

diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index d1a05e486b768a8338cd0e2df24db860d110a487..ce39eb434cefac45382932f976a0c42544f517a2 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -35,23 +35,29 @@ namespace quantifiers {
  * d_children[T1][2].d_children[T2][3].
  */
 class AlphaEquivalenceTypeNode {
-public:
- /** children of this node */
- std::map<std::pair<TypeNode, size_t>, AlphaEquivalenceTypeNode> d_children;
- /**
-  * map from canonized quantifier bodies to a quantified formula whose
-  * canonized body is that term.
-  */
- std::map<Node, Node> d_quant;
- /** register node
-  *
-  * This registers term q to this trie. The term t is the canonical form of
-  * q, typs/typCount represent a multi-set of types of free variables in t.
-  */
- Node registerNode(Node q,
-                   Node t,
-                   std::vector<TypeNode>& typs,
-                   std::map<TypeNode, size_t>& typCount);
+  using NodeMap = context::CDHashMap<Node, Node>;
+
+ public:
+  AlphaEquivalenceTypeNode(context::Context* c);
+  /** children of this node */
+  std::map<std::pair<TypeNode, size_t>,
+           std::unique_ptr<AlphaEquivalenceTypeNode>>
+      d_children;
+  /**
+   * map from canonized quantifier bodies to a quantified formula whose
+   * canonized body is that term.
+   */
+  NodeMap d_quant;
+  /** register node
+   *
+   * This registers term q to this trie. The term t is the canonical form of
+   * q, typs/typCount represent a multi-set of types of free variables in t.
+   */
+  Node registerNode(context::Context* c,
+                    Node q,
+                    Node t,
+                    std::vector<TypeNode>& typs,
+                    std::map<TypeNode, size_t>& typCount);
 };
 
 /**
@@ -60,10 +66,9 @@ public:
 class AlphaEquivalenceDb
 {
  public:
-  AlphaEquivalenceDb(expr::TermCanonize* tc, bool sortCommChildren)
-      : d_tc(tc), d_sortCommutativeOpChildren(sortCommChildren)
-  {
-  }
+  AlphaEquivalenceDb(context::Context* c,
+                     expr::TermCanonize* tc,
+                     bool sortCommChildren);
   /** adds quantified formula q to this database
    *
    * This function returns a quantified formula q' that is alpha-equivalent to
@@ -87,6 +92,8 @@ class AlphaEquivalenceDb
    * had been added to this class, or q otherwise.
    */
   Node addTermToTypeTrie(Node t, Node q);
+  /** The context we depend on */
+  context::Context* d_context;
   /** a trie per # of variables per type */
   AlphaEquivalenceTypeNode d_ae_typ_trie;
   /** pointer to the term canonize utility */

diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp
index 0d01efba7a12df18ee0e0e1d366d7806cbbffe8b..fddcb0712560b0394eb3595eca11df9d900dde1b 100644 (file)
--- a/src/theory/quantifiers/cegqi/nested_qe.cpp
+++ b/src/theory/quantifiers/cegqi/nested_qe.cpp
@@ -139,7 +139,7 @@ Node NestedQe::doQe(Env& env, Node q)
   q = nm->mkNode(kind::EXISTS, q[0], q[1].negate());
   std::unique_ptr<SolverEngine> smt_qe;
   initializeSubsolver(smt_qe, env);
-  Node qqe = smt_qe->getQuantifierElimination(q, true, false);
+  Node qqe = smt_qe->getQuantifierElimination(q, true);
   if (expr::hasBoundVar(qqe))
   {
     Trace("cegqi-nested-qe") << "  ...failed QE" << std::endl;

diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index b57c65f0fa47f5753f039a691446d7b12f9b1146..5907038796365cb8fc63adfc240ef8ca2892fa8b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -117,7 +117,7 @@ Node SygusQePreproc::preprocess(Node q)
 
   Trace("cegqi-qep") << "Run quantifier elimination on " << conj_se_ngsi_subs
                      << std::endl;
-  Node qeRes = smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true, false);
+  Node qeRes = smt_qe->getQuantifierElimination(conj_se_ngsi_subs, true);
   Trace("cegqi-qep") << "Result : " << qeRes << std::endl;
 
   // create single invocation conjecture, if QE was successful

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bc084714defad0bca0d0c82e4d1adf2ef4f116d4..66098220e1eeaa72d807d624dd0a5f1f4af7bac1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2019,6 +2019,8 @@ set(regress_1_tests
   regress1/quantifiers/issue5279-nqe.smt2
   regress1/quantifiers/issue5288-vts-real-int.smt2
   regress1/quantifiers/issue5365-nqe.smt2
+  regress1/quantifiers/issue5373-1-qe-inc.smt2 
+  regress1/quantifiers/issue5373-2.smt2 
   regress1/quantifiers/issue5378-witness.smt2
   regress1/quantifiers/issue5469-aext.smt2
   regress1/quantifiers/issue5470-aext.smt2

diff --git a/test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2 b/test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2
new file mode 100644 (file)
index 0000000..48bbe2d
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5373-1-qe-inc.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: -i
+; EXPECT: true
+; EXPECT: true
+(set-logic ALL)
+(get-qe (exists ((q Real) (q Bool) (q Bool) (q Bool) (q Real) (q Real) (q Real)) true))
+(get-qe (exists ((q Real) (q Bool) (f Bool) (q Bool) (q Real) (q Real) (q Real)) true))

diff --git a/test/regress/regress1/quantifiers/issue5373-2.smt2 b/test/regress/regress1/quantifiers/issue5373-2.smt2
new file mode 100644 (file)
index 0000000..1987b71
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5373-2.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort U 0)
+(declare-fun c (U U) U)
+(declare-fun k () U)
+(declare-fun a (U Int) Int)
+(assert (or (not (forall ((g U)) (! (or (forall ((x Int)) (! (distinct (a g x) (a k x)) :qid k!10))) :qid k!10))) (exists ((f U) (g U) (x Int)) (distinct (a (c f g) x) (a f (a g x))))))
+(check-sat)
+(check-sat-assuming ((exists ((f U) (g U) (x Int)) (distinct (a (c f g) x) (a f (a g x))))))
+(check-sat-assuming ((exists ((f U) (g U) (x Int)) (distinct (a (c f g) x) (a f (a g x))))))