From f7d88b42cefcaa6bb48c2709bfd32cf52d35d5ac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Sep 2017 18:49:41 -0500 Subject: [PATCH] Minor fixes for partial quantifier elimination. (#1147) This forces "counterexample lemmas" (the formula B => ~phi[e] on page 23 of http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf) to be added during TheoryQuantifiers::preRegisterTerm instead of at full effort check. This is required to ensure that CVC4's partial quantifier elimination algorithm produces correct results. Some background: "get-qe" and "get-qe-disjunct" are commands in the SMT2 parser. Here is how they can be used: [declarations] [assertions A] (get-qe (exists X F)) returns a ground formula F' such that A ^ F' and A ^ (exists X F) are equivalent. The command "get-qe-disjunct" provides an interface for doing an incremental version of "get-qe". [declarations] [assertions A] (get-qe-disjunct (exists X F)) returns a ground formula F1' such that A ^ F' implies A ^ (exists X F). It moreover has the property that if you call: [declarations] [assertions A] (assert F1') (get-qe-disjunct (exists X F)) this will give you a formula F2' where eventually: [declarations] [assertions A] (assert (not (or F1' ... Fn'))) (get-qe-disjunct (exists X F)) will either return "true" or "false", for some finite n. Here is an example that failed before this commit: (set-logic LIA) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c () Int) (declare-fun d () Int) (assert (or (not (>= (+ a (* (- 1) b)) 1)) (not (>= (+ c (* (- 1) d)) 0)))) (get-qe-disjunct (exists ((x Int)) (and (> a b) (> c x) (> d x)))) This should return: (not (or (not (>= (+ a (* (- 1) b)) 1)) (>= (+ c (* (- 1) d)) 1))) Previously it was returning: false This is because the cbqi algorithm needs to assume the negation of the quantified formula we are doing qe on before it makes any decision. The get-qe-partial feature is being requested by Cesare and Daniel Larraz for Kind2. This improves our performance on quantified LIA/LRA: https://www.starexec.org/starexec/secure/details/job.jsp?id=24480 see CVC4-092617-2-fixQePartial --- src/theory/quantifiers/inst_strategy_cbqi.cpp | 23 ++++++++++++------- src/theory/quantifiers_engine.cpp | 2 ++ 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 8e53c97dc..34758c431 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -167,10 +167,8 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine if( doCbqi( q ) ){ - if( registerCbqiLemma( q ) ){ - Debug("cbqi-debug") << "Registered cbqi lemma." << std::endl; - //set inactive the quantified formulas whose CE literals are asserted false - }else if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ + Assert( hasAddedCbqiLemma( q ) ); + if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ d_active_quant[q] = true; Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q ); @@ -373,7 +371,11 @@ void InstStrategyCbqi::preRegisterQuantifier( Node q ) { } void InstStrategyCbqi::registerQuantifier( Node q ) { - + if( doCbqi( q ) ){ + if( registerCbqiLemma( q ) ){ + Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; + } + } } Node InstStrategyCbqi::doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts ) { @@ -553,6 +555,7 @@ bool InstStrategyCbqi::doCbqi( Node q ){ if( it==d_do_cbqi.end() ){ int ret = 2; if( !d_quantEngine->getTermDatabase()->isQAttrQuantElim( q ) ){ + Assert( !d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( q ) ); //if has an instantiation pattern, don't do it if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ for( unsigned i=0; i