From 977bdcdcbab6ffdf757e3837d2f555a53cbb6daf Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 13 May 2014 17:18:18 +0200 Subject: [PATCH] Add lazy strategy for bounded integers to avoid non-terminating unsat cases. Add regressions. --- src/smt/smt_engine.cpp | 6 ++ src/theory/quantifiers/bounded_integers.cpp | 55 +++++++++++++++++-- src/theory/quantifiers/bounded_integers.h | 6 +- src/theory/quantifiers/options | 2 + src/theory/quantifiers_engine.cpp | 4 +- test/regress/regress0/quantifiers/Makefile.am | 3 +- .../regress0/quantifiers/bi-artm-s.smt2 | 29 ++++++++++ test/regress/regress0/strings/Makefile.am | 3 +- .../strings/artemis-0512-nonterm.smt2 | 25 +++++++++ 9 files changed, 123 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress0/quantifiers/bi-artm-s.smt2 create mode 100644 test/regress/regress0/strings/artemis-0512-nonterm.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0604988d3..4deb43f42 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -941,6 +941,9 @@ void SmtEngine::setDefaults() { Trace("smt") << "turning on finite-model-find, for strings-exp" << std::endl; } if(! options::fmfBoundInt.wasSetByUser()) { + if(! options::fmfBoundIntLazy.wasSetByUser()) { + options::fmfBoundIntLazy.set( true ); + } options::fmfBoundInt.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } @@ -1178,6 +1181,9 @@ void SmtEngine::setDefaults() { if( options::recurseCbqi() ){ options::cbqi.set( true ); } + if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) { + options::fmfBoundInt.set( true ); + } if( options::fmfBoundInt() ){ //must have finite model finding on options::finiteModelFind.set( true ); diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index a294eec5a..17446358c 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/options.h" using namespace CVC4; using namespace std; @@ -26,9 +27,22 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; + +BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, bool isProxy) : d_bi(bi), + d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) { + if( options::fmfBoundIntLazy() ){ + d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() ); + }else{ + d_proxy_range = r; + } + if( !isProxy ){ + Trace("bound-int") << "Introduce proxy " << d_proxy_range << " for " << d_range << std::endl; + } +} + void BoundedIntegers::RangeModel::initialize() { //add initial split lemma - Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) ); + Node ltr = NodeManager::currentNM()->mkNode( LT, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(0) ) ); ltr = Rewriter::rewrite( ltr ); Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl; d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); @@ -55,6 +69,7 @@ void BoundedIntegers::RangeModel::assertNode(Node n) { bool needsRange = true; for( std::map< Node, int >::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ if( d_range_assertions.find( it->first )==d_range_assertions.end() ){ + Trace("bound-int-debug") << "Does not need range because of " << it->first << std::endl; needsRange = false; break; } @@ -82,7 +97,7 @@ void BoundedIntegers::RangeModel::allocateRange() { int newBound = d_curr_max; Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl; //TODO: newBound should be chosen in a smarter way - Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) ); + Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) ); ltr = Rewriter::rewrite( ltr ); Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl; d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); @@ -113,6 +128,24 @@ Node BoundedIntegers::RangeModel::getNextDecisionRequest() { return Node::null(); } +bool BoundedIntegers::RangeModel::proxyCurrentRange() { + //Trace("model-engine") << "Range(" << d_range << ") currently is " << d_curr_max.get() << std::endl; + if( d_range!=d_proxy_range ){ + //int curr = d_curr_range.get(); + int curr = d_curr_max; + if( d_ranges_proxied.find( curr )==d_ranges_proxied.end() ){ + d_ranges_proxied[curr] = true; + Assert( d_range_literal.find( curr )!=d_range_literal.end() ); + Node lem = NodeManager::currentNM()->mkNode( IFF, d_range_literal[curr].negate(), + NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(curr) ) ) ); + Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << lem << std::endl; + d_bi->getQuantifiersEngine()->addLemma( lem ); + return true; + } + } + return false; +} + BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) : QuantifiersModule(qe), d_assertions(c){ @@ -211,7 +244,18 @@ void BoundedIntegers::process( Node f, Node n, bool pol, } void BoundedIntegers::check( Theory::Effort e ) { - + if( e==Theory::EFFORT_LAST_CALL ){ + bool addedLemma = false; + //make sure proxies are up-to-date with range + for( unsigned i=0; iproxyCurrentRange() ){ + addedLemma = true; + } + } + if( addedLemma ){ + d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); + } + } } @@ -275,18 +319,20 @@ void BoundedIntegers::registerQuantifier( Node f ) { for( unsigned i=0; imkSkolem( "bir", r.getType(), "bound for term" ); d_nground_range[f][v] = d_range[f][v]; d_range[f][v] = new_range; r = new_range; + isProxy = true; } if( r.getKind()!=CONST_RATIONAL ){ if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){ Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl; d_ranges.push_back( r ); - d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() ); + d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), isProxy ); d_rms[r]->initialize(); } } @@ -387,3 +433,4 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node bool BoundedIntegers::isGroundRange(Node f, Node v) { return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar(); } + diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 4130bffee..a6e85b392 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -60,9 +60,9 @@ private: private: BoundedIntegers * d_bi; void allocateRange(); + Node d_proxy_range; public: - RangeModel(BoundedIntegers * bi, Node r, context::Context* c) : d_bi(bi), - d_range(r), d_curr_max(-1), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1) {} + RangeModel(BoundedIntegers * bi, Node r, context::Context* c, bool isProxy); Node d_range; int d_curr_max; std::map< int, Node > d_range_literal; @@ -71,9 +71,11 @@ private: NodeBoolMap d_range_assertions; context::CDO< bool > d_has_range; context::CDO< int > d_curr_range; + std::map< int, bool > d_ranges_proxied; void initialize(); void assertNode(Node n); Node getNextDecisionRequest(); + bool proxyCurrentRange(); }; private: //information for minimizing ranges diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index f02a3bce1..f8f1744ed 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -119,6 +119,8 @@ option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write finite model finding on bounded integer quantification +option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write + enforce bounds for bounded integer quantification lazily via use of proxy variables option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" policy for instantiating axioms diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 53163cd5f..83733da42 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -91,14 +91,14 @@ d_lemmas_produced_c(u){ d_inst_engine = NULL; } if( options::finiteModelFind() ){ - d_model_engine = new quantifiers::ModelEngine( c, this ); - d_modules.push_back( d_model_engine ); if( options::fmfBoundInt() ){ d_bint = new quantifiers::BoundedIntegers( c, this ); d_modules.push_back( d_bint ); }else{ d_bint = NULL; } + d_model_engine = new quantifiers::ModelEngine( c, this ); + d_modules.push_back( d_model_engine ); }else{ d_model_engine = NULL; d_bint = NULL; diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index f12e67401..e399b4b23 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -41,7 +41,8 @@ TESTS = \ qcft-smtlib3dbc51.smt2 \ symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ - ARI176e1.smt2 + ARI176e1.smt2 \ + bi-artm-s.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/bi-artm-s.smt2 b/test/regress/regress0/quantifiers/bi-artm-s.smt2 new file mode 100644 index 000000000..5fb7522e9 --- /dev/null +++ b/test/regress/regress0/quantifiers/bi-artm-s.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --fmf-bound-int-lazy +; EXPECT: unsat +(set-option :incremental "false") +(set-info :status unsat) +(set-logic ALL_SUPPORTED) +(declare-fun Y () String) +(set-info :notes "ufP_1 is uf type conv P") +(declare-fun ufP_1 (Int) Int) +(set-info :notes "ufM_2 is uf type conv M") +(declare-fun ufM_2 (Int) Int) +(declare-fun z1_3 () String) +(declare-fun z2_4 () String) +(declare-fun z3_5 () String) +(declare-fun V_253 () String) +(declare-fun V_254 () String) + +(assert (or (= Y "1") (= Y "0"))) +(assert (>= (ufP_1 0) 32)) +(assert + +(forall ((V_243 Int)) +(or +(not (and (>= V_243 0) (>= (+ (str.len Y) (* (- 1) V_243)) 1))) +(and +(or (not (= (str.len Y) (+ 1 V_243))) (= (ufP_1 V_243) (ufM_2 V_243))) +(not (>= (ufM_2 V_243) 10)) +(not (or (not (= (str.len Y) (+ 1 V_243 (str.len V_253)))) (not (= Y (str.++ V_253 (ite (= (ufM_2 V_243) 0) "0" "1") V_254)))) ))) )) + +(check-sat) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index dd3c6b53a..ddc0eae7c 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -47,7 +47,8 @@ TESTS = \ loop007.smt2 \ loop008.smt2 \ loop009.smt2 \ - reloop.smt2 + reloop.smt2 \ + artemis-0512-nonterm.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2 new file mode 100644 index 000000000..ed97f36dd --- /dev/null +++ b/test/regress/regress0/strings/artemis-0512-nonterm.smt2 @@ -0,0 +1,25 @@ +(set-logic QF_S) +(set-info :status unsat) + +(declare-const Y String) +(assert + (or + (= Y "01") + (= Y "02") + (= Y "03") + (= Y "04") + (= Y "05") + (= Y "06") + (= Y "07") + (= Y "08") + (= Y "09") + (= Y "10") + (= Y "11") + (= Y "12") + ) +) + +(assert (= (<= (str.to.int Y) 31) false)) + +(check-sat) + -- 2.30.2