From a08914e449c3df26322551a968b4edee12a615f9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 27 May 2018 15:10:08 -0500 Subject: [PATCH] Fix cegqi assertions for quantified non-linear cases. (#1999) --- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 10 +++++++++- src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp | 6 +++++- src/theory/quantifiers_engine.cpp | 5 +++++ src/theory/quantifiers_engine.h | 2 ++ src/theory/theory_engine.cpp | 1 + src/theory/theory_engine.h | 3 ++- 6 files changed, 24 insertions(+), 3 deletions(-) diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index df51ace2d..72633e86f 100644 --- 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 a4599627d..203697fd7 100644 --- 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 3746c2e1c..8e6aab06c 100644 --- 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 e031bb64b..456a268da 100644 --- 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 4d78482c5..3977a9938 100644 --- 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 fb33b45de..8926e0593 100644 --- 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. -- 2.30.2