From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 14 Jun 2012 18:51:34 +0000 (+0000)
Subject: fix quantifier non-bug
X-Git-Tag: cvc5-1.0.0~8013
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=31e1f3402d4cd3da7cdfabc440c3b622432849b8;p=cvc5.git

fix quantifier non-bug
---

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 9aefda75a..dcf60e8f1 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1095,7 +1095,7 @@ lbool Solver::search(int nof_conflicts)
 		  (!order_heap.empty() || qhead < trail.size()) ) {
                 check_type = CHECK_WITH_THEORY;
                 continue;
-              } else if (!decisionEngineDone && recheck) {
+              } else if (recheck) {
                 // There some additional stuff added, so we go for another full-check
                 continue;
               } else {
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 11ff9ecad..c1476acb8 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -183,6 +183,8 @@ void InstantiationEngine::check( Theory::Effort e ){
     // such that the counterexample literal is not in positive in d_counterexample_asserts
    // for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) {
     //  if( (*i).second ) {
+    Debug("quantifiers") << "quantifiers:  check:  asserted quantifiers size" 
+                         << getQuantifiersEngine()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)getQuantifiersEngine()->getNumAssertedQuantifiers(); i++ ){
       Node n = getQuantifiersEngine()->getAssertedQuantifier( i );
       if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ff7648843..2440a2e53 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -265,6 +265,7 @@ class TheoryEngine {
     }
 
     void setIncomplete() throw(AssertionException) {
+      Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
       d_engine->setIncomplete(d_theory);
     }
 
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 1cc605227..70b47a3a9 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -16,6 +16,8 @@ TESTS =	\
 	bitvec0.delta01.smt \
 	bitvec5.smt \
 	quant-Arrays_Q1-noinfer.smt2 \
+	quant-ex1.smt2 \
+	quant-ex1.disable_miniscope.smt2 \
 	quant-symmetric_unsat_7.smt2 \
 	uflia-error0.smt2 \
 	uflia-xs-09-16-3-4-1-5.smt \
@@ -24,7 +26,6 @@ TESTS =	\
 
 # Incorrect answers:
 #	aufbv-fuzz01.smt \
-#	quant-ex1.smt2 \
 #
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2 b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
new file mode 100644
index 000000000..a8f4ff2b9
--- /dev/null
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2
@@ -0,0 +1,12 @@
+(set-logic AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun f (U) U)
+(declare-fun p () Bool)
+(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
new file mode 100644
index 000000000..9d5c95cdd
--- /dev/null
+++ b/test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect
@@ -0,0 +1,3 @@
+% COMMAND-LINE: --decision=justification --disable-miniscope-quant-fv --disable-miniscope-quant
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0
diff --git a/test/regress/regress0/decision/quant-ex1.smt2.expect b/test/regress/regress0/decision/quant-ex1.smt2.expect
index 66f5e51ba..38a730c57 100644
--- a/test/regress/regress0/decision/quant-ex1.smt2.expect
+++ b/test/regress/regress0/decision/quant-ex1.smt2.expect
@@ -1,3 +1,3 @@
-% COMMAND-LINE: --decision=justificationo
-% EXPECT: unknown (INCOMPLETE)
-% EXIT: 0
+% COMMAND-LINE: --decision=justification
+% EXPECT: sat
+% EXIT: 10