From: ajreynol Date: Mon, 15 Aug 2016 16:30:17 +0000 (-0500) Subject: Enable bounded set membership with --fmf-bound. Map to term models for bounded set... X-Git-Tag: cvc5-1.0.0~6040^2~4 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=baaab488c597e3e30dd3b929a5a612ba7fd660af;p=cvc5.git Enable bounded set membership with --fmf-bound. Map to term models for bounded set membership. --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 953150e42..85355c037 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -163,8 +163,10 @@ option fmfFmcSimple --fmf-fmc-simple bool :default true 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 fmfBound fmf-bound --fmf-bound bool :default false :read-write + finite model finding on bounded quantification +option fmfBoundLazy --fmf-bound-lazy bool :default false :read-write + enforce bounds for bounded quantification lazily via use of proxy variables ### conflict-based instantiation options diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d7b7f9c3e..32c44d224 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1350,8 +1350,8 @@ void SmtEngine::setDefaults() { Trace("smt") << "turning on quantifier logic, for strings-exp" << std::endl; } - if(! options::fmfBoundInt.wasSetByUser()) { - options::fmfBoundInt.set( true ); + if(! options::fmfBound.wasSetByUser()) { + options::fmfBound.set( true ); Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; } if(! options::fmfInstEngine.wasSetByUser()) { @@ -1753,12 +1753,13 @@ void SmtEngine::setDefaults() { options::cbqi.set(false); } - if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) { - options::fmfBoundInt.set( true ); + if( ( options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy() ) || + ( options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt() ) ) { + options::fmfBound.set( true ); } //now have determined whether fmfBoundInt is on/off //apply fmfBoundInt options - if( options::fmfBoundInt() ){ + if( options::fmfBound() ){ //must have finite model finding on options::finiteModelFind.set( true ); if( ! options::mbqiMode.wasSetByUser() || diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 7184624da..54853ceaf 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -20,6 +20,7 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace std; @@ -30,7 +31,7 @@ using namespace CVC4::kind; BoundedIntegers::IntRangeModel::IntRangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi), d_range(r), d_curr_max(-1), d_lit_to_range(u), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1), d_ranges_proxied(u) { - if( options::fmfBoundIntLazy() ){ + if( options::fmfBoundLazy() ){ d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() ); }else{ d_proxy_range = r; @@ -232,14 +233,12 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol, } }else if( lit.getKind()==MEMBER ){ //TODO: enable this when sets models are fixed - /* if( !pol && lit[0].getKind()==BOUND_VARIABLE && !isBound( q, lit[0] ) && !lit[1].hasBoundVar() ){ Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is membership." << std::endl; bound_lit_type_map[lit[0]] = BOUND_SET_MEMBER; bound_lit_map[0][lit[0]] = lit; bound_lit_pol_map[0][lit[0]] = pol; } - */ }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; } @@ -330,6 +329,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { setBoundedVar( f, v, BOUND_SET_MEMBER ); setBoundVar = true; d_setm_range[f][v] = bound_lit_map[0][v][1]; + d_setm_range_lit[f][v] = bound_lit_map[0][v]; Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl; } if( setBoundVar ){ @@ -515,6 +515,63 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; sr = d_quantEngine->getModel()->getCurrentModelValue( sr ); Trace("bound-int-rsi") << "Value is " << sr << std::endl; + //map to term model + if( sr.getKind()!=EMPTYSET ){ + std::map< Node, Node > val_to_term; + while( sr.getKind()==UNION ){ + Assert( sr[1].getKind()==kind::SINGLETON ); + val_to_term[ sr[1][0] ] = sr[1][0]; + sr = sr[0]; + } + Assert( sr.getKind()==kind::SINGLETON ); + val_to_term[ sr[0] ] = sr[0]; + //must look back at assertions, not term database (theory of sets introduces extraneous terms internally) + Theory* theory = d_quantEngine->getTheoryEngine()->theoryOf( THEORY_SETS ); + if( theory ){ + context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for( unsigned i = 0; it != it_end; ++ it, ++i ){ + Node lit = (*it).assertion; + if( lit.getKind()==kind::MEMBER ){ + Node vr = d_quantEngine->getModel()->getCurrentModelValue( lit[0] ); + Trace("bound-int-rsi-debug") << "....membership for " << lit << " ==> " << vr << std::endl; + Trace("bound-int-rsi-debug") << " " << (val_to_term.find( vr )!=val_to_term.end()) << " " << d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) << std::endl; + if( val_to_term.find( vr )!=val_to_term.end() ){ + if( d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) ){ + Trace("bound-int-rsi") << " Map value to term : " << vr << " -> " << lit[0] << std::endl; + val_to_term[ vr ] = lit[0]; + } + } + } + } + } + //rebuild value + Node nsr; + for( std::map< Node, Node >::iterator it = val_to_term.begin(); it != val_to_term.end(); ++it ){ + Node nv = NodeManager::currentNM()->mkNode( kind::SINGLETON, it->second ); + if( nsr.isNull() ){ + nsr = nv; + }else{ + nsr = NodeManager::currentNM()->mkNode( kind::UNION, nsr, nv ); + } + } + Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl; + return nsr; + + /* + Node lit = d_setm_range_lit[q][v]; + Trace("bound-int-rsi-debug") << "Bounded from lit " << lit << std::endl; + Node f = d_quantEngine->getTermDatabase()->getMatchOperator( lit ); + TermArgTrie * ta = d_quantEngine->getTermDatabase()->getTermArgTrie( f ); + if( ta ){ + Trace("bound-int-rsi-debug") << "Got term index for " << f << std::endl; + for( std::map< TNode, TermArgTrie >::iterator it = ta->d_data.begin(); it != ta->d_data.end(); ++it ){ + + } + + } + */ + } + } return sr; } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index ab4bcba96..c3fb05641 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -60,6 +60,7 @@ private: std::map< Node, std::map< Node, Node > > d_nground_range; //set membership range std::map< Node, std::map< Node, Node > > d_setm_range; + std::map< Node, std::map< Node, Node > > d_setm_range_lit; void hasFreeVar( Node f, Node n ); void process( Node f, Node n, bool pol, std::map< Node, unsigned >& bound_lit_type_map, diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index a0665cb7f..be608aeaa 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -668,7 +668,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, } } if( addInst ){ - if( options::fmfBoundInt() ){ + if( options::fmfBound() ){ std::vector< Node > cond; cond.push_back(d_quant_cond[f]); cond.insert( cond.end(), inst.begin(), inst.end() ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 10a5ae41b..7bbe06108 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -45,7 +45,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) { bool QModelBuilder::optUseModel() { - return options::mbqiMode()!=MBQI_NONE || options::fmfBoundInt(); + return options::mbqiMode()!=MBQI_NONE || options::fmfBound(); } void QModelBuilder::debugModel( FirstOrderModel* fm ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 5d575969f..7658f2b6b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -121,7 +121,7 @@ void ModelEngine::registerQuantifier( Node f ){ if( !tn.isSort() ){ if( !tn.getCardinality().isFinite() ){ if( tn.isInteger() ){ - if( !options::fmfBoundInt() ){ + if( !options::fmfBound() ){ canHandle = false; } }else{ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 75d177fdc..c08fee712 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -98,7 +98,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* //the model object if( options::mbqiMode()==quantifiers::MBQI_FMC || - options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() || + options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBound() || options::mbqiMode()==quantifiers::MBQI_TRUST ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ @@ -233,7 +233,7 @@ void QuantifiersEngine::finishInit(){ } //finite model finding if( options::finiteModelFind() ){ - if( options::fmfBoundInt() ){ + if( options::fmfBound() ){ d_bint = new quantifiers::BoundedIntegers( c, this ); d_modules.push_back( d_bint ); } @@ -282,9 +282,9 @@ void QuantifiersEngine::finishInit(){ } if( needsBuilder ){ - Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; + Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || - options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){ + options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){ Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ @@ -1241,7 +1241,7 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { if( e==Theory::EFFORT_LAST_CALL ){ //with bounded integers, skip every other last call, // since matching loops may occur with infinite quantification - if( d_ierCounter_lc%2==0 && options::fmfBoundInt() ){ + if( d_ierCounter_lc%2==0 && options::fmfBound() ){ performCheck = false; } } diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 184553ba7..86bcb2cac 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -366,12 +366,12 @@ int RepSetIterator::resetIndex( int i, bool initial ) { d_domain[v].clear(); d_setm_bounds[v].clear(); if( srv.getKind()!=EMPTYSET ){ - //TODO: need term model, not value model while( srv.getKind()==UNION ){ Assert( srv[1].getKind()==kind::SINGLETON ); d_setm_bounds[v].push_back( srv[1][0] ); srv = srv[0]; } + Assert( srv.getKind()==kind::SINGLETON ); d_setm_bounds[v].push_back( srv[0] ); d_domain[v].push_back( d_setm_bounds[v].size() ); }else{ diff --git a/test/regress/regress0/quantifiers/bi-artm-s.smt2 b/test/regress/regress0/quantifiers/bi-artm-s.smt2 index 5fb7522e9..b97c339fc 100644 --- a/test/regress/regress0/quantifiers/bi-artm-s.smt2 +++ b/test/regress/regress0/quantifiers/bi-artm-s.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound-int-lazy +; COMMAND-LINE: --fmf-bound-lazy ; EXPECT: unsat (set-option :incremental "false") (set-info :status unsat)