diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-27 15:10:08 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-27 13:10:08 -0700 |
commit | a08914e449c3df26322551a968b4edee12a615f9 (patch) | |
tree | e96f2c19484c4ecf413ab220a2aed915d56a30b4 /src/theory/quantifiers/cegqi | |
parent | 97914ba14805c6e6d84e45f33b3eea711a1e01a5 (diff) |
Fix cegqi assertions for quantified non-linear cases. (#1999)
Diffstat (limited to 'src/theory/quantifiers/cegqi')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp | 6 |
2 files changed, 14 insertions, 2 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() ); |