More fixes for quantifier elimination (#5533)

Fixes #5506, fixes #5507.

7 files changed, 55 insertions, 4 deletions

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index e5ecafd4a..4636cf17a 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/quant_elim_solver.h"
 
+#include "expr/skolem_manager.h"
 #include "expr/subs.h"
 #include "smt/smt_solver.h"
 #include "theory/quantifiers/cegqi/nested_qe.h"
@@ -33,7 +34,8 @@ QuantElimSolver::~QuantElimSolver() {}
 
 Node QuantElimSolver::getQuantifierElimination(Assertions& as,
                                                Node q,
-                                               bool doFull)
+                                               bool doFull,
+                                               bool isInternalSubsolver)
 {
   Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl;
   if (q.getKind() != EXISTS && q.getKind() != FORALL)
@@ -41,11 +43,13 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     throw ModalException(
         "Expecting a quantified formula as argument to get-qe.");
   }
+  NodeManager* nm = NodeManager::currentNM();
+  // ensure the body is rewritten
+  q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
   // do nested quantifier elimination if necessary
   q = quantifiers::NestedQe::doNestedQe(q, true);
   Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
                   << q << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
   // tag the quantified formula with the quant-elim attribute
   TypeNode t = nm->booleanType();
   Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
@@ -121,6 +125,12 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     // do extended rewrite to minimize the size of the formula aggressively
     theory::quantifiers::ExtendedRewriter extr(true);
     ret = extr.extendedRewrite(ret);
+    // if we are not an internal subsolver, convert to witness form, since
+    // internally generated skolems should not escape
+    if (!isInternalSubsolver)
+    {
+      ret = SkolemManager::getWitnessForm(ret);
+    }
     return ret;
   }
   // otherwise, just true/false
diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h
index 96ed1f73d..ca55fc618 100644
--- a/src/smt/quant_elim_solver.h
+++ b/src/smt/quant_elim_solver.h
@@ -79,8 +79,19 @@ class QuantElimSolver
    * extended command get-qe-disjunct, which can be used
    * for incrementally computing the result of a
    * quantifier elimination.
+   *
+   * @param as The assertions of the SmtEngine
+   * @param q The quantified formula we are eliminating quantifiers from
+   * @param doFull Whether we are doing full quantifier elimination on q
+   * @param isInternalSubsolver Whether the SmtEngine we belong to is an
+   * internal subsolver. If it is not, then we convert the final result to
+   * witness form.
+   * @return The result of eliminating quantifiers from q.
    */
-  Node getQuantifierElimination(Assertions& as, Node q, bool doFull);
+  Node getQuantifierElimination(Assertions& as,
+                                Node q,
+                                bool doFull,
+                                bool isInternalSubsolver);
 
  private:
   /** The SMT solver, which is used during doQuantifierElimination. */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 722f6a080..d3ba676fc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1498,7 +1498,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
   if(!d_logic.isPure(THEORY_ARITH) && strict){
     Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
   }
-  return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull);
+  return d_quantElimSolver->getQuantifierElimination(
+      *d_asserts, q, doFull, d_isInternalSubsolver);
 }
 
 bool SmtEngine::getInterpol(const Node& conj,
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 297f11690..da9fdd022 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -336,6 +336,8 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
 
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
+  d_lemmas_waiting.clear();
+  d_phase_req_waiting.clear();
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 816202fa9..4445a28d0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1622,6 +1622,8 @@ set(regress_1_tests
   regress1/quantifiers/issue5482-rtf-no-fv.smt2
   regress1/quantifiers/issue5484-qe.smt2
   regress1/quantifiers/issue5484b-qe.smt2
+  regress1/quantifiers/issue5506-qe.smt2
+  regress1/quantifiers/issue5507-qe.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
diff --git a/test/regress/regress1/quantifiers/issue5506-qe.smt2 b/test/regress/regress1/quantifiers/issue5506-qe.smt2
new file mode 100644
index 000000000..3839f2d75
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5506-qe.smt2
@@ -0,0 +1,6 @@
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(get-qe (forall ((b Int)) (= a 0)))
diff --git a/test/regress/regress1/quantifiers/issue5507-qe.smt2 b/test/regress/regress1/quantifiers/issue5507-qe.smt2
new file mode 100644
index 000000000..3b7ddbcf3
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5507-qe.smt2
@@ -0,0 +1,19 @@
+; EXPECT: false
+; EXIT: 0
+(set-logic LIA)
+(declare-fun v0 () Bool)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(declare-fun v3 () Bool)
+(declare-fun v5 () Bool)
+(declare-fun v6 () Bool)
+(declare-fun v9 () Bool)
+(declare-fun v10 () Bool)
+(declare-fun v15 () Bool)
+(declare-fun v16 () Bool)
+(declare-fun i0 () Int)
+(declare-fun i2 () Int)
+(declare-fun i9 () Int)
+(declare-fun v26 () Bool)
+(declare-fun v33 () Bool)
+(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0)))