From f4d9d607c3a63a1b3842e291f06a621f71b0e966 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 2 Jul 2013 13:40:26 -0500 Subject: [PATCH] Minor fixes for bounded integers, rewrite engine. --- src/theory/quantifiers/full_model_check.cpp | 25 ++++++++++------ src/theory/quantifiers/rewrite_engine.cpp | 23 ++++++++++++--- src/theory/quantifiers/rewrite_engine.h | 2 ++ src/theory/quantifiers_engine.h | 1 + src/theory/rep_set.cpp | 32 +++++++++++---------- 5 files changed, 55 insertions(+), 28 deletions(-) diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 2be9de91c..42d5bbd3a 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -86,6 +86,7 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { } int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector & inst, int index ) { + Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl; if (index==(int)inst.size()) { return d_data; }else{ @@ -717,21 +718,26 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " "; debugPrintCond("fmc-exh", c, true); Trace("fmc-exh")<< std::endl; + Trace("fmc-exh-debug") << "Set interval domains..." << std::endl; //set the bounds on the iterator based on intervals for( unsigned i=0; iisInterval(c[i]) ){ - for( unsigned b=0; b<2; b++ ){ - if( !fm->isStar(c[i][b]) ){ - riter.d_bounds[b][i] = c[i][b]; + if( c[i].getType().isInteger() ){ + if( fm->isInterval(c[i]) ){ + for( unsigned b=0; b<2; b++ ){ + if( !fm->isStar(c[i][b]) ){ + riter.d_bounds[b][i] = c[i][b]; + } } + }else if( !fm->isStar(c[i]) ){ + riter.d_bounds[0][i] = c[i]; + riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 ); } - }else if( !fm->isStar(c[i]) ){ - riter.d_bounds[0][i] = c[i]; - riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 ); } } + Trace("fmc-exh-debug") << "Set quantifier..." << std::endl; //initialize if( riter.setQuantifier( f ) ){ + Trace("fmc-exh-debug") << "Set element domains..." << std::endl; //set the domains based on the entry for (unsigned i=0; imkConst( true ); + } //apply rewrite rules int addedLemmas = 0; for( unsigned i=0; igetNextMatch( f, m ); if( success ){ //see if instantiation is true in the model - bool trueInModel = false; - - if( !trueInModel ){ + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rrg = rr[1]; + std::vector< Node > vars; + std::vector< Node > terms; + d_quantEngine->computeTermVector( f, m, vars, terms ); + Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl; + Node inst = d_rr_guard[f]; + inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl; + FirstOrderModel * fm = d_quantEngine->getModel(); + Node v = fm->getValue( inst ); + Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl; + if( v==d_true ){ Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl; if( d_quantEngine->addInstantiation( f, m ) ){ addedLemmas++; @@ -106,6 +119,8 @@ void RewriteEngine::registerQuantifier( Node f ) { Node rr = f.getAttribute(QRewriteRuleAttribute()); Trace("rewrite-engine") << " rewrite rule is : " << rr << std::endl; d_rr_quant.push_back( f ); + d_rr_guard[f] = rr[1]; + Trace("rewrite-engine") << " guard is : " << d_rr_guard[f] << std::endl; } } diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index 5160af602..fe8daca5f 100755 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -32,6 +32,8 @@ class RewriteEngine : public QuantifiersModule typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; std::vector< Node > d_rr_quant; + std::map< Node, Node > d_rr_guard; + Node d_true; /** explicitly provided patterns */ std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; private: diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 40b043752..b075f7be8 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -83,6 +83,7 @@ class EqualityQueryQuantifiersEngine; class QuantifiersEngine { friend class quantifiers::InstantiationEngine; friend class quantifiers::ModelEngine; + friend class quantifiers::RewriteEngine; friend class inst::InstMatch; private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index b44cc6779..647ef965a 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -250,29 +250,31 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl; //determine the current range if( d_enum_type[ii]==ENUM_RANGE ){ - if( initial || !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ){ + if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){ Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl; Node l, u; - d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u ); + if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ + d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u ); + } + for( unsigned b=0; b<2; b++ ){ + if( d_bounds[b].find(ii)!=d_bounds[b].end() ){ + Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl; + if( b==0 && (l.isNull() || d_bounds[b][ii].getConst() > l.getConst()) ){ + l = d_bounds[b][ii]; + }else if( b==1 && (u.isNull() || d_bounds[b][ii].getConst() <= u.getConst()) ){ + u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], + NodeManager::currentNM()->mkConst( Rational(1) ) ); + u = Rewriter::rewrite( u ); + } + } + } + if( l.isNull() || u.isNull() ){ //failed, abort the iterator d_index.clear(); return false; }else{ Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl; - for( unsigned b=0; b<2; b++ ){ - if( d_bounds[b].find(ii)!=d_bounds[b].end() ){ - Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl; - if( b==0 && d_bounds[b][ii].getConst() > l.getConst() ){ - l = d_bounds[b][ii]; - }else if( b==1 && d_bounds[b][ii].getConst() <= u.getConst() ){ - u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], - NodeManager::currentNM()->mkConst( Rational(1) ) ); - u = Rewriter::rewrite( u ); - } - } - } - Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); d_domain[ii].clear(); -- 2.30.2