diff options
-rwxr-xr-x | src/theory/quantifiers/full_model_check.cpp | 25 | ||||
-rwxr-xr-x | src/theory/quantifiers/rewrite_engine.cpp | 23 | ||||
-rwxr-xr-x | src/theory/quantifiers/rewrite_engine.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 1 | ||||
-rw-r--r-- | 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<Node> & 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; i<c.getNumChildren(); i++ ){
- 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];
+ 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; i<c.getNumChildren(); i++) {
if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
@@ -765,9 +771,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh-debug") << " ";
inst.push_back(r);
}
-
int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);
- Trace("fmc-exh-debug") << ", index = " << ev_index;
+ Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
if (ev!=d_true) {
InstMatch m;
@@ -780,6 +785,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh-debug") << " ...success.";
addedLemmas++;
}
+ }else{
+ Trace("fmc-exh-debug") << ", already true";
}
Trace("fmc-exh-debug") << std::endl;
int index = riter.increment();
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 84d465579..aa0569ef4 100755 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -30,7 +30,10 @@ RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : Qua }
void RewriteEngine::check( Theory::Effort e ) {
- if( e==Theory::EFFORT_FULL ){
+ if( e==Theory::EFFORT_LAST_CALL ){
+ if( d_true.isNull() ){
+ d_true = NodeManager::currentNM()->mkConst( true );
+ }
//apply rewrite rules
int addedLemmas = 0;
for( unsigned i=0; i<d_rr_quant.size(); i++ ) {
@@ -82,9 +85,19 @@ int RewriteEngine::checkRewriteRule( Node f ) { success = d_rr_triggers[f][i]->getNextMatch( 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<Node, int, NodeHashFunction> NodeIntMap;
typedef context::CDHashMap<Node, Node, NodeHashFunction> 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<Rational>() > l.getConst<Rational>()) ){ + l = d_bounds[b][ii]; + }else if( b==1 && (u.isNull() || d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>()) ){ + 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<Rational>() > l.getConst<Rational>() ){ - l = d_bounds[b][ii]; - }else if( b==1 && d_bounds[b][ii].getConst<Rational>() <= u.getConst<Rational>() ){ - 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(); |