Fix cegqi assertions for quantified non-linear cases. (#1999)

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index df51ace2de3574b0e0da75a75d31452afcde3ede..72633e86f7329dc73f23487158ecb6958e2e4f96 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -707,7 +707,15 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
 #ifdef CVC4_ASSERTIONS
-      if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){
+      // the instantiation strategy for quantified linear integer/real
+      // arithmetic with arbitrary quantifier nesting is "monotonic" as a
+      // consequence of Lemmas 5, 9 and Theorem 4 of Reynolds et al, "Solving
+      // Quantified Linear Arithmetic by Counterexample Guided Instantiation",
+      // FMSD 2017. We throw an assertion failure if we detect a case where the
+      // strategy was not monotonic.
+      if (options::cbqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
+          && d_qe->getLogicInfo().isLinear())
+      {
         Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
         Assert( false );
       }

diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index a4599627d7894ba437df3627e7589d751121f970..203697fd7cf6ae4e00d4a454c76d2bebe120092b 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -354,7 +354,11 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
               lhs_value = Rewriter::rewrite( lhs_value );
             }
             Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl;
-            Assert( lhs_value!=rhs_value );
+            // it generally should be the case that lhs_value!=rhs_value
+            // however, this assertion is violated e.g. if non-linear is enabled
+            // since the quantifier-free arithmetic solver may pass full
+            // effort with no lemmas even when we are not guaranteed to have a
+            // model. By convention, we use GEQ to compare the values here.
             Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value );
             cmp = Rewriter::rewrite( cmp );
             Assert( cmp.isConst() );

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 3746c2e1c66f944edf183238c76fdcdcc7bb403b..8e6aab06c038b7472e068c5e9ee7f6dcd416f7be 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -317,6 +317,11 @@ Valuation& QuantifiersEngine::getValuation()
   return d_te->theoryOf(THEORY_QUANTIFIERS)->getValuation();
 }
 
+const LogicInfo& QuantifiersEngine::getLogicInfo() const
+{
+  return d_te->getLogicInfo();
+}
+
 QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
   std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
   if( it==d_owner.end() ){

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index e031bb64b44ec66ec1a7eb6647d1eeafa66150ee..456a268da5dcf527f4f0429d821bde8e54c84cc0 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -218,6 +218,8 @@ public:
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
   Valuation& getValuation();
+  /** get the logic info for the quantifiers engine */
+  const LogicInfo& getLogicInfo() const;
   /** get relevant domain */
   quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
   /** get the BV inverter utility */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4d78482c5ded13a502a109a617cad78854744c42..3977a993812b58b36e065ad0766a03318857f317 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1467,6 +1467,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   return !d_inConflict;
 }
 
+const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
 
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   Assert(a.getType().isComparableTo(b.getType()));

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index fb33b45de85e21d1947f4769680bf4d4e94b4386..8926e05932c5ab1c089e51aa7d6f85c47542901e 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -773,7 +773,8 @@ public:
   inline bool isTheoryEnabled(theory::TheoryId theoryId) const {
     return d_logicInfo.isTheoryEnabled(theoryId);
   }
-
+  /** get the logic info used by this theory engine */
+  const LogicInfo& getLogicInfo() const;
   /**
    * Returns the equality status of the two terms, from the theory
    * that owns the domain type.  The types of a and b must be the same.