From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 May 2018 19:23:48 +0000 (-0500)
Subject: Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)
X-Git-Tag: cvc5-1.0.0~5096
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=af67146760804bd18cb85414c17021131d03dcf1;p=cvc5.git

Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)
---

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 358efede7..6e59363e2 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -878,10 +878,6 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
 }
   
 bool CegInstantiator::check() {
-  if( d_qe->getTheoryEngine()->needCheck() ){
-    Trace("cbqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
-    return false;
-  }
   processAssertions();
   for( unsigned r=0; r<2; r++ ){
     d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL;
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 125682e8c..86f5abf61 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -39,7 +39,8 @@ CegInstantiation::~CegInstantiation(){
 }
 
 bool CegInstantiation::needsCheck( Theory::Effort e ) {
-  return e>=Theory::EFFORT_LAST_CALL;
+  return !d_quantEngine->getTheoryEngine()->needCheck()
+         && e >= Theory::EFFORT_LAST_CALL;
 }
 
 QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e)
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 885c36bb5..edea22fbf 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -612,7 +612,8 @@ void TheoryEngine::check(Theory::Effort effort) {
           }
         }
       }
-      if( ! d_inConflict && ! needCheck() ){
+      if (!d_inConflict)
+      {
         if(d_logicInfo.isQuantified()) {
           // quantifiers engine must check at last call effort
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 3674e42bb..48c81a13b 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1255,6 +1255,7 @@ REG1_TESTS = \
 	regress1/quantifiers/model_6_1_bv.smt2 \
 	regress1/quantifiers/mutualrec2.cvc \
 	regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \
+	regress1/quantifiers/nra-interleave-inst.smt2 \
 	regress1/quantifiers/opisavailable-12.smt2 \
 	regress1/quantifiers/parametric-lists.smt2 \
 	regress1/quantifiers/psyco-001-bv.smt2 \
diff --git a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
new file mode 100644
index 000000000..8e318a372
--- /dev/null
+++ b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
@@ -0,0 +1,18 @@
+(set-info :smt-lib-version 2.6)
+(set-logic NRA)
+(set-info :status unsat)
+(declare-fun xI () Real)
+(declare-fun ts35uscore2 () Real)
+(declare-fun A () Real)
+(declare-fun B () Real)
+(declare-fun t60uscore0dollarskuscore2 () Real)
+(declare-fun I1 () Real)
+(declare-fun v () Real)
+(declare-fun V () Real)
+(declare-fun xuscore2dollarskuscore50 () Real)
+(declare-fun vuscore2dollarskuscore56 () Real)
+(declare-fun ep () Real)
+(declare-fun I1uscore2dollarskuscore52 () Real)
+(declare-fun x () Real)
+(assert (not (exists ((ts35uscore2 Real)) (let ((?v_1 (- B))) (let ((?v_0 (+ (* ?v_1 ts35uscore2) vuscore2dollarskuscore56)) (?v_3 (+ (* ?v_1 t60uscore0dollarskuscore2) vuscore2dollarskuscore56)) (?v_2 (* (/ 1 2) (+ (+ (* ?v_1 (* t60uscore0dollarskuscore2 t60uscore0dollarskuscore2)) (* (* 2 t60uscore0dollarskuscore2) vuscore2dollarskuscore56)) (* 2 xuscore2dollarskuscore50))))) (=> (and (and (and (and (and (and (and (and (and (and (and (and (and (= I1uscore2dollarskuscore52 2) (=> (and (<= 0 ts35uscore2) (<= ts35uscore2 t60uscore0dollarskuscore2)) (and (and (>= ?v_0 0) (<= ?v_0 V)) (<= ts35uscore2 ep)))) (>= t60uscore0dollarskuscore2 0)) (>= vuscore2dollarskuscore56 0)) (<= vuscore2dollarskuscore56 V)) (< xI xuscore2dollarskuscore50)) (= I1 2)) (< xI x)) (> B 0)) (>= v 0)) (<= v V)) (>= A 0)) (> V 0)) (> ep 0)) (or (< xI ?v_2) (> xI (+ ?v_2 (/ (* ?v_3 ?v_3) (* 2 B)))))))))))
+(check-sat)