diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-04 08:14:30 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-04 08:14:36 +0200 |
commit | 32cda667fac11b1768ed75d930cb5b0e6933ffe5 (patch) | |
tree | 909ec2de9ee931f56a84dfbe68ebc110f0a95a61 | |
parent | 0fde4ed8bcaa5dabd92ba9079455ca12df9ba2ec (diff) |
Minor changes to smt comp script for quantified arith. Add option --cbqi-sat whether to disable sat for quantified arith.
-rwxr-xr-x | contrib/run-script-smtcomp2015 | 12 | ||||
-rwxr-xr-x | contrib/run-script-smtcomp2015-application | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 2 |
5 files changed, 25 insertions, 14 deletions
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index 3fc8ccec5..9b8a0ba38 100755 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -67,12 +67,12 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) finishwith --full-saturate-quant ;; LIA|LRA|NIA|NRA) - trywith 20 --cbqi --full-saturate-quant - trywith 20 --full-saturate-quant - trywith 20 --cbqi --cbqi-recurse --full-saturate-quant - trywith 60 --qcf-tconstraint --full-saturate-quant - trywith 120 --cbqi --cbqi-recurse --full-saturate-quant - finishwith --cbqi-recurse --pre-skolem-quant --full-saturate-quant + trywith 60 --cbqi --full-saturate-quant + trywith 60 --full-saturate-quant + trywith 60 --cbqi --cbqi-recurse --full-saturate-quant + trywith 180 --qcf-tconstraint --full-saturate-quant + trywith 240 --cbqi --cbqi-recurse --full-saturate-quant + finishwith --cbqi --cbqi-recurse --pre-skolem-quant --full-saturate-quant ;; QF_AUFBV) trywith 600 diff --git a/contrib/run-script-smtcomp2015-application b/contrib/run-script-smtcomp2015-application index 69b3f8b37..4219241ef 100755 --- a/contrib/run-script-smtcomp2015-application +++ b/contrib/run-script-smtcomp2015-application @@ -33,10 +33,10 @@ QF_LIA) runcvc4 --enable-miplib-trick --miplib-trick-subs=4 --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --pb-rewrites ;; ALIA|AUFLIA|AUFLIRA|AUFNIRA|BV|UF|UFBV|UFIDL|UFLIA|UFLRA|UFNIA) - runcvc4 --simplification=none --decision=internal --full-saturate-quant + runcvc4 ;; LIA|LRA|NIA|NRA) - runcvc4 --enable-cbqi --full-saturate-quant + runcvc4 --cbqi ;; QF_BV) runcvc4 --unconstrained-simp --bv-eq-slicer=auto --bv-div-zero-const --bv-intro-pow2 diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index f530f7b9d..e867aae1e 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -173,6 +173,7 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){ } void InstantiationEngine::reset_round( Theory::Effort e ) { + d_cbqi_set_quant_inactive = false; if( options::cbqi() ){ //set inactive the quantified formulas whose CE literals are asserted false for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ @@ -185,9 +186,11 @@ void InstantiationEngine::reset_round( Theory::Effort e ) { if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; if( !value ){ - d_quantEngine->getModel()->setQuantifierActive( q, false ); if( d_quantEngine->getValuation().isDecision( cel ) ){ Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; + }else{ + d_quantEngine->getModel()->setQuantifierActive( q, false ); + d_cbqi_set_quant_inactive = true; } } }else{ @@ -233,12 +236,16 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ } bool InstantiationEngine::checkComplete() { - for( unsigned i=0; i<d_quants.size(); i++ ){ - if( isIncomplete( d_quants[i] ) ){ - return false; + if( !options::cbqiSat() && d_cbqi_set_quant_inactive ){ + return false; + }else{ + for( unsigned i=0; i<d_quants.size(); i++ ){ + if( isIncomplete( d_quants[i] ) ){ + return false; + } } + return true; } - return true; } void InstantiationEngine::registerQuantifier( Node f ){ diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 21056bc05..dc5b976f0 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -87,6 +87,8 @@ private: bool doCbqi( Node f ); /** is the engine incomplete for this quantifier */ bool isIncomplete( Node f ); + /** cbqi set inactive */ + bool d_cbqi_set_quant_inactive; private: /** do instantiation round */ bool doInstantiationRound( Theory::Effort effort ); @@ -98,7 +100,7 @@ public: /** initialize */ void finishInit(); - bool needsCheck( Theory::Effort e ); + bool needsCheck( Theory::Effort e ); void reset_round( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); bool checkComplete(); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e2d9af74f..fe81df7f8 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -232,6 +232,8 @@ option cbqi2 --cbqi2 bool :read-write :default false turns on new implementation of counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default false turns on recursive counterexample-based quantifier instantiation +option cbqiSat --cbqi-sat bool :read-write :default true + answer sat when quantifiers are asserted with counterexample-based quantifier instantiation ### local theory extensions options |