From 2bf0735176e0ff5fb9720bfb255ca22443584dcc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 May 2013 17:34:23 -0500 Subject: [PATCH] Significant work on bounded integer quantification to handle non-trivial bounds. Refactoring of InstConstantAttribute to be internal to TermDb. --- src/smt/options | 2 + src/theory/arith/theory_arith_private.cpp | 2 +- src/theory/quantifiers/bounded_integers.cpp | 135 ++++++++++--- src/theory/quantifiers/bounded_integers.h | 34 +++- .../quantifiers/candidate_generator.cpp | 2 +- src/theory/quantifiers/first_order_model.cpp | 2 +- src/theory/quantifiers/full_model_check.cpp | 184 ++++++++++-------- src/theory/quantifiers/full_model_check.h | 6 +- src/theory/quantifiers/inst_gen.cpp | 4 +- src/theory/quantifiers/inst_match.cpp | 2 +- .../quantifiers/inst_match_generator.cpp | 18 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 82 +------- src/theory/quantifiers/model_builder.cpp | 48 ++++- src/theory/quantifiers/model_builder.h | 6 + src/theory/quantifiers/model_engine.cpp | 6 +- src/theory/quantifiers/options | 3 + src/theory/quantifiers/quant_util.cpp | 6 +- .../quantifiers/quantifiers_rewriter.cpp | 4 - src/theory/quantifiers/relevant_domain.cpp | 4 +- src/theory/quantifiers/term_database.cpp | 78 ++++++-- src/theory/quantifiers/term_database.h | 14 +- src/theory/quantifiers/theory_quantifiers.cpp | 6 +- src/theory/quantifiers/trigger.cpp | 24 +-- src/theory/quantifiers_engine.cpp | 15 +- src/theory/rep_set.cpp | 130 +++++++++---- src/theory/rep_set.h | 14 +- src/theory/rewriterules/rr_inst_match.cpp | 23 ++- src/theory/rewriterules/rr_inst_match.h | 2 +- src/theory/rewriterules/rr_trigger.cpp | 20 +- src/theory/rewriterules/rr_trigger.h | 3 +- src/theory/rewriterules/theory_rewriterules.h | 2 +- .../theory_rewriterules_rules.cpp | 9 +- 32 files changed, 548 insertions(+), 342 deletions(-) diff --git a/src/smt/options b/src/smt/options index 2680f4105..e5f9c2eaf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -24,6 +24,8 @@ common-option produceModels produce-models -m --produce-models bool :default fal support the get-value and get-model commands option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions +option dumpModels --dump-models bool :default false + output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation # this is just a placeholder for later; it doesn't show up in command-line options listings diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 060f6dbba..3b141bf9e 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1376,7 +1376,7 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){ Assert(!done()); TNode assertion = get(); - if( options::finiteModelFind() ){ + if( d_quantEngine && d_quantEngine->getBoundedIntegers() ){ d_quantEngine->getBoundedIntegers()->assertNode(assertion); } diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index aeac3c79b..4492e6d2d 100755 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/model_engine.h" using namespace CVC4; using namespace std; @@ -26,14 +27,14 @@ void BoundedIntegers::RangeModel::initialize() { //add initial split lemma Node ltr = NodeManager::currentNM()->mkNode( LT, d_range, NodeManager::currentNM()->mkConst( Rational(0) ) ); ltr = Rewriter::rewrite( ltr ); - Trace("bound-integers-lemma") << " *** bound int: initial split on " << ltr << std::endl; + Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl; d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr; d_range_literal[-1] = ltr_lit; d_lit_to_range[ltr_lit] = -1; d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT; //register with bounded integers - Trace("bound-integers-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl; + Trace("bound-int-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl; d_bi->addLiteralFromRange(ltr_lit, d_range); } @@ -41,9 +42,9 @@ void BoundedIntegers::RangeModel::assertNode(Node n) { bool pol = n.getKind()!=NOT; Node nlit = n.getKind()==NOT ? n[0] : n; if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){ - Trace("bound-integers-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")"; - Trace("bound-integers-assert") << ", found literal " << nlit; - Trace("bound-integers-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl; + Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")"; + Trace("bound-int-assert") << ", found literal " << nlit; + Trace("bound-int-assert") << ", it is bound literal " << d_lit_to_range[nlit] << " for " << d_range << std::endl; d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]); if( pol!=d_lit_to_pol[nlit] ){ //check if we need a new split? @@ -61,7 +62,7 @@ void BoundedIntegers::RangeModel::assertNode(Node n) { } }else{ if (!d_has_range || d_lit_to_range[nlit]mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) ); ltr = Rewriter::rewrite( ltr ); - Trace("bound-integers-lemma") << " *** bound int: split on " << ltr << std::endl; + Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl; d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr; d_range_literal[newBound] = ltr_lit; @@ -101,7 +102,7 @@ Node BoundedIntegers::RangeModel::getNextDecisionRequest() { if (!d_lit_to_pol[it->first]) { rn = rn.negate(); } - Trace("bound-integers-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl; + Trace("bound-int-dec") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl; return rn; } } @@ -121,7 +122,7 @@ bool BoundedIntegers::isBound( Node f, Node v ) { bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) { if( b.getKind()==BOUND_VARIABLE ){ - if( isBound( f, b ) ){ + if( !isBound( f, b ) ){ return true; } }else{ @@ -138,23 +139,23 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) { if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){ std::map< Node, Node > msum; if (QuantArith::getMonomialSumLit( lit, msum )){ - Trace("bound-integers-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; + Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - Trace("bound-integers-debug") << " "; + Trace("bound-int-debug") << " "; if( !it->second.isNull() ){ - Trace("bound-integers-debug") << it->second; + Trace("bound-int-debug") << it->second; if( !it->first.isNull() ){ - Trace("bound-integers-debug") << " * "; + Trace("bound-int-debug") << " * "; } } if( !it->first.isNull() ){ - Trace("bound-integers-debug") << it->first; + Trace("bound-int-debug") << it->first; } - Trace("bound-integers-debug") << std::endl; + Trace("bound-int-debug") << std::endl; } - Trace("bound-integers-debug") << std::endl; + Trace("bound-int-debug") << std::endl; for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){ + if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){ Node veq; if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){ Node n1 = veq[0]; @@ -170,11 +171,11 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) { } veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 ); } - Trace("bound-integers-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl; + Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl; Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2; if( !isBound( f, bv ) ){ if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) { - Trace("bound-integers-debug") << "The bound is relevant." << std::endl; + Trace("bound-int-debug") << "The bound is relevant." << std::endl; d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1); } } @@ -215,12 +216,13 @@ void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) { } void BoundedIntegers::registerQuantifier( Node f ) { - Trace("bound-integers") << "Register quantifier " << f << std::endl; + Trace("bound-int") << "Register quantifier " << f << std::endl; bool hasIntType = false; + std::map< Node, int > numMap; for( unsigned i=0; imkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] ); d_range[f][v] = Rewriter::rewrite( r ); - Trace("bound-integers") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl; + Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl; } if( d_set[f].size()==f[0].getNumChildren() ){ d_bound_quants.push_back( f ); for( unsigned i=0; imkSkolem( "bir_$$", r.getType(), "bound for term" ); + /* + std::vector< Node > bvs; + quantifiers::TermDb::getBoundVars(r, bvs); + Assert(bvs.size()>0); + Node body = NodeManager::currentNM()->mkNode( LEQ, r, new_range ); + std::vector< Node > children; + //get all the other bounds + for( unsigned j=0; jmkNode( LEQ, NodeManager::currentNM()->mkConst(Rational(0)), bvs[j]); + Node u = NodeManager::currentNM()->mkNode( LEQ, bvs[j], d_range[f][bvs[j]] ); + children.push_back(l); + children.push_back(u); + } + Node antec = NodeManager::currentNM()->mkNode( AND, children ); + body = NodeManager::currentNM()->mkNode( IMPLIES, antec, body ); + + Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs ); + + Node lem = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); + Trace("bound-int") << "For " << v << ", the quantified formula " << lem << " will be used to minimize the bound." << std::endl; + Trace("bound-int-lemma") << " *** bound int: bounding quantified lemma " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma( lem ); + */ + d_nground_range[f][v] = d_range[f][v]; + d_range[f][v] = new_range; + r = new_range; + } 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 << std::endl; d_ranges.push_back( r ); d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() ); d_rms[r]->initialize(); @@ -261,13 +295,13 @@ void BoundedIntegers::registerQuantifier( Node f ) { } void BoundedIntegers::assertNode( Node n ) { - Trace("bound-integers-assert") << "Assert " << n << std::endl; + Trace("bound-int-assert") << "Assert " << n << std::endl; Node nlit = n.getKind()==NOT ? n[0] : n; if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){ - Trace("bound-integers-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl; + Trace("bound-int-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl; for( unsigned i=0; iassertNode( n ); } } @@ -275,7 +309,7 @@ void BoundedIntegers::assertNode( Node n ) { } Node BoundedIntegers::getNextDecisionRequest() { - Trace("bound-integers-dec") << "bi: Get next decision request?" << std::endl; + Trace("bound-int-dec") << "bi: Get next decision request?" << std::endl; for( unsigned i=0; igetNextDecisionRequest(); if (!d.isNull()) { @@ -285,7 +319,48 @@ Node BoundedIntegers::getNextDecisionRequest() { return Node::null(); } +void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { + l = d_bounds[0][f][v]; + u = d_bounds[1][f][v]; + if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){ + //must create substitution + std::vector< Node > vars; + std::vector< Node > subs; + Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl; + for( unsigned i=0; id_var_order[d_set_nums[f][i]] << std::endl; + Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl; + vars.push_back(d_set[f][i]); + subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]])); + }else{ + break; + } + } + Trace("bound-int-rsi") << "Do substitution..." << std::endl; + //check if it has been instantiated + if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){ + //must add the lemma + Node nn = d_nground_range[f][v]; + nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] ); + Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma(lem); + l = Node::null(); + u = Node::null(); + return; + }else{ + u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + } + } + Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl; + l = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), l ); + u = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), u ); + Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl; + return; +} -Node BoundedIntegers::getValueInModel( Node n ) { - return d_quantEngine->getModel()->getValue( n ); +bool BoundedIntegers::isGroundRange(Node f, Node v) { + return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v)); } \ No newline at end of file diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 4445493c9..f40e2180c 100755 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -24,8 +24,12 @@ namespace CVC4 { namespace theory { + +class RepSetIterator; + namespace quantifiers { + class BoundedIntegers : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; @@ -37,7 +41,9 @@ private: bool hasNonBoundVar( Node f, Node b ); std::map< Node, std::map< Node, Node > > d_bounds[2]; std::map< Node, std::vector< Node > > d_set; + std::map< Node, std::vector< int > > d_set_nums; std::map< Node, std::map< Node, Node > > d_range; + std::map< Node, std::map< Node, Node > > d_nground_range; void hasFreeVar( Node f, Node n ); void process( Node f, Node n, bool pol ); void processLiteral( Node f, Node lit, bool pol ); @@ -62,7 +68,6 @@ private: void assertNode(Node n); Node getNextDecisionRequest(); }; - Node getValueInModel( Node n ); private: //information for minimizing ranges std::vector< Node > d_ranges; @@ -72,6 +77,25 @@ private: std::map< Node, std::vector< Node > > d_lit_to_ranges; //list of currently asserted arithmetic literals NodeBoolMap d_assertions; +private: + //class to store whether bounding lemmas have been added + class BoundInstTrie + { + public: + std::map< Node, BoundInstTrie > d_children; + bool hasInstantiated( std::vector< Node > & vals, int index = 0, bool madeNew = false ){ + if( index>=(int)vals.size() ){ + return !madeNew; + }else{ + Node n = vals[index]; + if( d_children.find(n)==d_children.end() ){ + madeNew = true; + } + return d_children[n].hasInstantiated(vals,index+1,madeNew); + } + } + }; + std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; private: void addLiteralFromRange( Node lit, Node r ); public: @@ -81,10 +105,14 @@ public: void registerQuantifier( Node f ); void assertNode( Node n ); Node getNextDecisionRequest(); + bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); } + unsigned getNumBoundVars( Node f ) { return d_set[f].size(); } + Node getBoundVar( Node f, int i ) { return d_set[f][i]; } + int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; } Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; } Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; } - Node getLowerBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[0][f][v] ); } - Node getUpperBoundValue( Node f, Node v ){ return getValueInModel( d_bounds[1][f][v] ); } + void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); + bool isGroundRange(Node f, Node v); }; } diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 0c423de19..6c6a80b90 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -27,7 +27,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::inst; bool CandidateGenerator::isLegalCandidate( Node n ){ - return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute()) ) ); + return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n) ) ); } void CandidateGeneratorQueue::addCandidate( Node n ) { diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index bba9c0163..a11729519 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -397,7 +397,7 @@ struct sortGetMaxVariableNum { int computeMaxVariableNum( Node n ){ if( n.getKind()==INST_CONSTANT ){ return n.getAttribute(InstVarNumAttribute()); - }else if( n.hasAttribute(InstConstantAttribute()) ){ + }else if( TermDb::hasInstConstAttr(n) ){ int maxVal = -1; for( int i=0; i<(int)n.getNumChildren(); i++ ){ int val = getMaxVariableNum( n[i] ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 445f0d6c0..b5d4648a1 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -139,7 +139,7 @@ bool Def::addEntry( FullModelChecker * m, Node c, Node v) { } } -Node Def::evaluate( FullModelChecker * m, std::vector inst ) { +Node Def::evaluate( FullModelChecker * m, std::vector& inst ) { int gindex = d_et.getGeneralizationIndex(m, inst); if (gindex!=-1) { return d_value[gindex]; @@ -148,7 +148,7 @@ Node Def::evaluate( FullModelChecker * m, std::vector inst ) { } } -int Def::getGeneralizationIndex( FullModelChecker * m, std::vector inst ) { +int Def::getGeneralizationIndex( FullModelChecker * m, std::vector& inst ) { return d_et.getGeneralizationIndex(m, inst); } @@ -163,7 +163,7 @@ void Def::simplify(FullModelChecker * m) { d_et.reset(); for (unsigned i=0; i types; - for(unsigned i=0; imkFunctionType( types, NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); - d_quant_cond[f] = op; - } - - //model check the quantifier - doCheck(fm, f, d_quant_models[f], f[1]); - Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; - d_quant_models[f].debugPrint("fmc", Node::null(), this); - Trace("fmc") << std::endl; - //consider all entries going to false - for (unsigned i=0; i inst; - for (unsigned j=0; j types; + for(unsigned i=0; imkFunctionType( types, NodeManager::currentNM()->booleanType() ); + Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); + d_quant_cond[f] = op; + } + + //model check the quantifier + doCheck(fm, f, d_quant_models[f], f[1]); + Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; + d_quant_models[f].debugPrint("fmc", Node::null(), this); + Trace("fmc") << std::endl; + //consider all entries going to false + for (unsigned i=0; i inst; + for (unsigned j=0; jaddInstantiation( f, m ) ){ - lemmas++; + if( addInst ){ + InstMatch m; + for( unsigned j=0; jaddInstantiation( f, m ) ){ + lemmas++; + }else{ + //this can happen if evaluation is unknown + //might try it next effort level + d_star_insts[f].push_back(i); + } }else{ - //this can happen if evaluation is unknown //might try it next effort level d_star_insts[f].push_back(i); } - }else{ - //might try it next effort level - d_star_insts[f].push_back(i); } } - } - }else{ - if (!d_star_insts[f].empty()) { - Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl; - Trace("fmc-exh") << "Definition was : " << std::endl; - d_quant_models[f].debugPrint("fmc-exh", Node::null(), this); - Trace("fmc-exh") << std::endl; - Def temp; - //simplify the exceptions? - for( int i=(d_star_insts[f].size()-1); i>=0; i--) { - //get witness for d_star_insts[f][i] - int j = d_star_insts[f][i]; - if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ - int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j ); - if( lem==-1 ){ - //something went wrong, resort to exhaustive instantiation - return false; - }else{ - lemmas += lem; + }else{ + if (!d_star_insts[f].empty()) { + Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl; + Trace("fmc-exh") << "Definition was : " << std::endl; + d_quant_models[f].debugPrint("fmc-exh", Node::null(), this); + Trace("fmc-exh") << std::endl; + Def temp; + //simplify the exceptions? + for( int i=(d_star_insts[f].size()-1); i>=0; i--) { + //get witness for d_star_insts[f][i] + int j = d_star_insts[f][i]; + if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){ + int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j ); + if( lem==-1 ){ + //something went wrong, resort to exhaustive instantiation + return false; + }else{ + lemmas += lem; + } } } } } + return true; } - return true; } int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) { int addedLemmas = 0; - RepSetIterator riter( &(fm->d_rep_set) ); + RepSetIterator riter( d_qe, &(fm->d_rep_set) ); Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " "; debugPrintCond("fmc-exh", c, true); Trace("fmc-exh")<< std::endl; - if( riter.setQuantifier( d_qe, f ) ){ + if( riter.setQuantifier( f ) ){ std::vector< RepDomain > dom; for (unsigned i=0; imkNode(kind::LAMBDA, boundVarList, curr); +} + +Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) { + Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl; + for(unsigned i=0; ievaluate(this, args); + }else{ + return Node::null(); + } } \ No newline at end of file diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 92c866ffd..00a910567 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -65,8 +65,8 @@ public: d_has_simplified = false; } bool addEntry( FullModelChecker * m, Node c, Node v); - Node evaluate( FullModelChecker * m, std::vector inst ); - int getGeneralizationIndex( FullModelChecker * m, std::vector inst ); + Node evaluate( FullModelChecker * m, std::vector& inst ); + int getGeneralizationIndex( FullModelChecker * m, std::vector& inst ); void simplify( FullModelChecker * m ); void debugPrint(const char * tr, Node op, FullModelChecker * m); }; @@ -141,6 +141,8 @@ public: /** process build model */ void processBuildModel(TheoryModel* m, bool fullModel); + /** get current model value */ + Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ); }; } diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 192e58d7c..157861670 100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -29,10 +29,10 @@ using namespace CVC4::theory::quantifiers; InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ - Assert( n.hasAttribute(InstConstantAttribute()) ); + Assert( TermDb::hasInstConstAttr(n) ); int count = 0; for( size_t i=0; i& t ){ if( n.getKind()==MULT ){ - if( n[1].hasAttribute(InstConstantAttribute()) ){ - f = n[1].getAttribute(InstConstantAttribute()); + if( TermDb::hasInstConstAttr(n[1]) ){ + f = TermDb::getInstConstAttr(n[1]); if( n[1].getKind()==INST_CONSTANT ){ d_ceTableaux[x][ n[1] ] = n[0]; }else{ @@ -155,8 +155,8 @@ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder t << n; } }else{ - if( n.hasAttribute(InstConstantAttribute()) ){ - f = n.getAttribute(InstConstantAttribute()); + if( TermDb::hasInstConstAttr(n) ){ + f = TermDb::getInstConstAttr(n); if( n.getKind()==INST_CONSTANT ){ d_ceTableaux[x][ n ] = Node::null(); }else{ @@ -327,81 +327,9 @@ int InstStrategyDatatypesValue::process( Node f, Theory::Effort effort, int e ){ Node InstStrategyDatatypesValue::getValueFor( Node n ){ //simply get the ground value for n in the current model, if it exists, // or return an arbitrary ground term otherwise - if( !n.hasAttribute(InstConstantAttribute()) ){ + if( !TermDb::hasInstConstAttr(n) ){ return n; }else{ return n; } - /* FIXME - - Debug("quant-datatypes-debug") << "get value for " << n << std::endl; - if( !n.hasAttribute(InstConstantAttribute()) ){ - return n; - }else{ - Assert( n.getType().isDatatype() ); - //check if in equivalence class with ground term - Node rep = getRepresentative( n ); - Debug("quant-datatypes-debug") << "Rep is " << rep << std::endl; - if( !rep.hasAttribute(InstConstantAttribute()) ){ - return rep; - }else{ - if( !n.getType().isDatatype() ){ - return n.getType().mkGroundTerm(); - }else{ - if( n.getKind()==APPLY_CONSTRUCTOR ){ - std::vector< Node > children; - children.push_back( n.getOperator() ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( getValueFor( n[i] ) ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - }else{ - const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); - TheoryDatatypes::EqLists* labels = &((TheoryDatatypes*)d_th)->d_labels; - //otherwise, use which constructor the inst constant is current chosen to be - if( labels->find( n )!=labels->end() ){ - TheoryDatatypes::EqList* lbl = (*labels->find( n )).second; - int tIndex = -1; - if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind()==APPLY_TESTER ){ - Debug("quant-datatypes-debug") << n << " tester is " << (*lbl)[ lbl->size()-1 ] << std::endl; - tIndex = Datatype::indexOf((*lbl)[ lbl->size()-1 ].getOperator().toExpr()); - }else{ - Debug("quant-datatypes-debug") << "find possible tester choice" << std::endl; - //must find a possible choice - vector< bool > possibleCons; - possibleCons.resize( dt.getNumConstructors(), true ); - for( TheoryDatatypes::EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) { - Node leqn = (*j); - possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false; - } - for( unsigned int j=0; j children; - children.push_back( cons ); - for( int i=0; i<(int)dt[ tIndex ].getNumArgs(); i++ ) { - Node sn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[tIndex][i].getSelector() ), n ); - if( n.hasAttribute(InstConstantAttribute()) ){ - InstConstantAttribute ica; - sn.setAttribute(ica,n.getAttribute(InstConstantAttribute()) ); - } - Node snn = getValueFor( sn ); - children.push_back( snn ); - } - return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - }else{ - return n.getType().mkGroundTerm(); - } - } - } - } - } - */ } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 79e36e9f5..76e61707e 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -46,6 +46,37 @@ bool QModelBuilder::optUseModel() { } +Node QModelBuilder::getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial ) { + std::vector< Node > children; + if( n.getNumChildren()>0 ){ + if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for (unsigned i=0; imkNode( n.getKind(), children ); + nn = Rewriter::rewrite( nn ); + return nn; + } + }else{ + if( n.getKind()==VARIABLE ){ + return getCurrentUfModelValue( fm, n, children, partial ); + }else{ + return n; + } + } +} + + bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ if( argIndex<(int)n.getNumChildren() ){ Node r; @@ -71,6 +102,9 @@ QModelBuilder( c, qe ) { } +Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) { + return n; +} void QModelBuilderIG::debugModel( FirstOrderModel* fm ){ //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true @@ -81,8 +115,8 @@ void QModelBuilderIG::debugModel( FirstOrderModel* fm ){ for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ vars.push_back( f[0][j] ); } - RepSetIterator riter( &(fm->d_rep_set) ); - riter.setQuantifier( d_qe, f ); + RepSetIterator riter( d_qe, &(fm->d_rep_set) ); + riter.setQuantifier( f ); while( !riter.isFinished() ){ std::vector< Node > terms; for( int i=0; i uf_terms; - if( n.hasAttribute(InstConstantAttribute()) ){ + if( TermDb::hasInstConstAttr(n) ){ isConst = false; if( gn.getKind()==APPLY_UF ){ uf_terms.push_back( gn ); @@ -418,7 +452,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ }else if( gn.getKind()==EQUAL ){ isConst = true; for( int j=0; j<2; j++ ){ - if( n[j].hasAttribute(InstConstantAttribute()) ){ + if( TermDb::hasInstConstAttr(n[j]) ){ if( n[j].getKind()==APPLY_UF && fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){ uf_terms.push_back( gn[j] ); @@ -525,17 +559,16 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ for( size_t i=0; i tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms for( int j=0; j<2; j++ ){ - if( lit[j].hasAttribute(InstConstantAttribute()) ){ + if( TermDb::hasInstConstAttr(lit[j]) ){ if( lit[j].getKind()==APPLY_UF ){ tr_terms.push_back( lit[j] ); }else{ @@ -671,7 +704,6 @@ void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ //if( !s.isNull() ){ // s = Rewriter::rewrite( s ); //} - d_qe->getTermDatabase()->setInstantiationConstantAttr( s, f ); Trace("sel-form-debug") << "Selection formula " << f << std::endl; Trace("sel-form-debug") << " " << s << std::endl; if( !s.isNull() ){ diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 2b38f3381..f41392eee 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -33,6 +33,8 @@ protected: context::CDO< FirstOrderModel* > d_curr_model; //quantifiers engine QuantifiersEngine* d_qe; + /** get current model value */ + virtual Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) = 0; public: QModelBuilder( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilder(){} @@ -48,6 +50,8 @@ public: bool d_considerAxioms; /** exist instantiation ? */ virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } + /** get current model value */ + Node getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial = false ); }; @@ -91,6 +95,8 @@ protected: bool d_didInstGen; /** process build model */ virtual void processBuildModel( TheoryModel* m, bool fullModel ); + /** get current model value */ + Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ); protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index b9dcef282..c91d9d3ab 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -187,7 +187,7 @@ int ModelEngine::checkModel(){ d_relevantLemmas = 0; d_totalLemmas = 0; Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::fmfFullModelCheck() ? 2 : 1; + int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1; for( int e=0; egetNumAssertedQuantifiers(); i++ ){ @@ -238,8 +238,8 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } Debug("inst-fmf-ei") << std::endl; //create a rep set iterator and iterate over the (relevant) domain of the quantifier - RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) ); - if( riter.setQuantifier( d_quantEngine, f ) ){ + RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); + if( riter.setQuantifier( f ) ){ Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; d_quantEngine->getModel()->resetEvaluate(); Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 9facdbc5f..e83014789 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -116,6 +116,9 @@ option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :defau option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques +option fmfBoundInt --fmf-bound-int bool :default false + finite model finding on bounded integer quantification + 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/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 53f67853b..59995a510 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -189,13 +189,13 @@ QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){ for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; if( it->first.getKind()==EQUAL ){ - if( it->first[0].hasAttribute(InstConstantAttribute()) ){ - if( !it->first[1].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(it->first[0]) ){ + if( !quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; d_phase_reqs_equality[ it->first[0] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; } - }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){ + }else if( quantifiers::TermDb::hasInstConstAttr(it->first[1]) ){ d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; d_phase_reqs_equality[ it->first[1] ] = it->second; Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 5c71f6e6f..9f156b656 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -211,10 +211,6 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { if( in.hasAttribute(NestedQuantAttribute()) ){ setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) ); } - if( in.hasAttribute(InstConstantAttribute()) ){ - InstConstantAttribute ica; - ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) ); - } Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; Trace("quantifiers-rewrite") << " to " << std::endl; Trace("quantifiers-rewrite") << ret << std::endl; diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 2b011552c..cf12cf540 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -147,7 +147,7 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ if( n.getKind()==INST_CONSTANT ){ - Node f = n.getAttribute(InstConstantAttribute()); + Node f = TermDb::getInstConstAttr(n); int var = n.getAttribute(InstVarNumAttribute()); range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() ); return false; @@ -177,7 +177,7 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ } } //get the range - if( n.hasAttribute(InstConstantAttribute()) ){ + if( TermDb::hasInstConstAttr(n) ){ if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){ range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() ); }else{ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 417b4ae3a..dc00b5f95 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -74,7 +74,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ //if this is an atomic trigger, consider adding it //Call the children? if( inst::Trigger::isAtomicTrigger( n ) ){ - if( !n.hasAttribute(InstConstantAttribute()) ){ + if( !TermDb::hasInstConstAttr(n) ){ Trace("term-db") << "register term in db " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; Node op = n.getOperator(); @@ -117,7 +117,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } } }else{ - if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){ + if( options::efficientEMatching() && !TermDb::hasInstConstAttr(n)){ //Efficient e-matching must be notified //The term in triggers are not important here Debug("term-db") << "New in this branch term " << n << std::endl; @@ -167,7 +167,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ while( !eqc.isFinished() ){ Node en = (*eqc); computeModelBasisArgAttribute( en ); - if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ + if( en.getKind()==APPLY_UF && !TermDb::hasInstConstAttr(en) ){ if( !en.getAttribute(NoMatchAttribute()) ){ Node op = en.getOperator(); if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ @@ -275,33 +275,75 @@ void TermDb::makeInstantiationConstantsFor( Node f ){ //set the var number attribute InstVarNumAttribute ivna; ic.setAttribute(ivna,i); + InstConstantAttribute ica; + ic.setAttribute(ica,f); + //also set the no-match attribute + NoMatchAttribute nma; + ic.setAttribute(nma,true); } } } -void TermDb::setInstantiationConstantAttr( Node n, Node f ){ - if( !n.hasAttribute(InstConstantAttribute()) ){ - bool setAttr = false; - if( n.getKind()==INST_CONSTANT ){ - setAttr = true; - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - setInstantiationConstantAttr( n[i], f ); - if( n[i].hasAttribute(InstConstantAttribute()) ){ - setAttr = true; - } + +Node TermDb::getInstConstAttr( Node n ) { + if (!n.hasAttribute(InstConstantAttribute()) ){ + Node f; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + f = getInstConstAttr(n[i]); + if( !f.isNull() ){ + break; } } - if( setAttr ){ - InstConstantAttribute ica; - n.setAttribute(ica,f); + InstConstantAttribute ica; + n.setAttribute(ica,f); + if( !f.isNull() ){ //also set the no-match attribute NoMatchAttribute nma; n.setAttribute(nma,true); } } + return n.getAttribute(InstConstantAttribute()); +} + +bool TermDb::hasInstConstAttr( Node n ) { + return !getInstConstAttr(n).isNull(); } +bool TermDb::hasBoundVarAttr( Node n ) { + if( !n.getAttribute(HasBoundVarComputedAttribute()) ){ + bool hasBv = false; + if( n.getKind()==BOUND_VARIABLE ){ + hasBv = true; + }else{ + for (unsigned i=0; i& bvs) { + if (n.getKind()==BOUND_VARIABLE ){ + if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){ + bvs.push_back( n ); + } + }else{ + for( unsigned i=0; i >::const_iterator it = d_inst_constants.find( f ); @@ -347,7 +389,6 @@ Node TermDb::getCounterexampleLiteral( Node f ){ //otherwise, ensure literal Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); d_ce_lit[ f ] = ceLit; - setInstantiationConstantAttr( ceLit, f ); } return d_ce_lit[ f ]; } @@ -361,7 +402,6 @@ Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector & var Node n2 = n.substitute( vars.begin(), vars.end(), inst_constants.begin(), inst_constants.end() ); - setInstantiationConstantAttr( n2, f ); return n2; } diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e5154476a..7b5df2ab8 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -59,6 +59,10 @@ typedef expr::Attribute ModelBasisAttribute; struct ModelBasisArgAttributeId {}; typedef expr::Attribute ModelBasisArgAttribute; +struct HasBoundVarAttributeId {}; +typedef expr::Attribute HasBoundVarAttribute; +struct HasBoundVarComputedAttributeId {}; +typedef expr::Attribute HasBoundVarComputedAttribute; class QuantifiersEngine; @@ -186,9 +190,15 @@ public: Node convertNodeToPattern( Node n, Node f, const std::vector & vars, const std::vector & nvars); - /** set instantiation constant attr */ - void setInstantiationConstantAttr( Node n, Node f ); + static Node getInstConstAttr( Node n ); + static bool hasInstConstAttr( Node n ); +//for bound variables +public: + //does n have bound variables? + static bool hasBoundVarAttr( Node n ); + //get bound variables in n + static void getBoundVars( Node n, std::vector< Node >& bvs); //for skolem private: /** map from universal quantifiers to the list of skolem constants */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 9843cd09e..c68623baa 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -65,7 +65,7 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { void TheoryQuantifiers::preRegisterTerm(TNode n) { Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; - if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){ + if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->registerQuantifier( n ); } } @@ -149,7 +149,7 @@ Node TheoryQuantifiers::getNextDecisionRequest(){ void TheoryQuantifiers::assertUniversal( Node n ){ Assert( n.getKind()==FORALL ); - if( !n.hasAttribute(InstConstantAttribute()) ){ + if( !TermDb::hasInstConstAttr(n) ){ getQuantifiersEngine()->registerQuantifier( n ); getQuantifiersEngine()->assertNode( n ); } @@ -157,7 +157,7 @@ void TheoryQuantifiers::assertUniversal( Node n ){ void TheoryQuantifiers::assertExistential( Node n ){ Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !n[0].hasAttribute(InstConstantAttribute()) ){ + if( !TermDb::hasInstConstAttr(n[0]) ){ if( d_skolemized.find( n )==d_skolemized.end() ){ Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] ); NodeBuilder<> nb(kind::OR); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 1f1667522..fea8ab6d5 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -124,7 +124,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& qe->getTermDatabase()->computeVarContains( temp[i] ); for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; - if( v.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(v)==f ){ if( vars.find( v )==vars.end() ){ varCount++; vars[ v ] = true; @@ -223,7 +223,7 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ } bool Trigger::isUsable( Node n, Node f ){ - if( n.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n)==f ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ if( !isUsable( n[i], f ) ){ @@ -282,8 +282,6 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { int vti = veq[0]==it->first ? 1 : 0; if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){ rtr = veq; - InstConstantAttribute ica; - rtr.setAttribute(ica,veq[vti].getAttribute(InstConstantAttribute()) ); } } } @@ -298,13 +296,11 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) { Trace("relational-trigger") << " polarity : " << pol << std::endl; } Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr; - InstConstantAttribute ica; - rtr2.setAttribute(ica,rtr.getAttribute(InstConstantAttribute()) ); return rtr2; } } } - bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); + bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); Trace("usable") << n << " usable : " << usable << std::endl; if( usable ){ return n; @@ -325,7 +321,7 @@ bool Trigger::isAtomicTrigger( Node n ){ bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){ return false; } } @@ -438,9 +434,9 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff Assert( coeffs.empty() ); NodeBuilder<> t(kind::PLUS); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){ if( n[i].getKind()==INST_CONSTANT ){ - if( n[i].getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){ coeffs[ n[i] ] = Node::null(); }else{ coeffs.clear(); @@ -463,13 +459,13 @@ bool Trigger::isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeff } return true; }else if( n.getKind()==MULT ){ - if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){ - if( !n[1].hasAttribute(InstConstantAttribute()) ){ + if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){ + if( !quantifiers::TermDb::hasInstConstAttr(n[1]) ){ coeffs[ n[0] ] = n[1]; return true; } - }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){ - if( !n[0].hasAttribute(InstConstantAttribute()) ){ + }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){ + if( !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ coeffs[ n[1] ] = n[0]; return true; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ef8169433..89d1ad55a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -61,9 +61,12 @@ d_lemmas_produced_c(u){ if( options::finiteModelFind() ){ d_model_engine = new quantifiers::ModelEngine( c, this ); d_modules.push_back( d_model_engine ); - - d_bint = new quantifiers::BoundedIntegers( c, this ); - d_modules.push_back( d_bint ); + if( options::fmfBoundInt() ){ + d_bint = new quantifiers::BoundedIntegers( c, this ); + d_modules.push_back( d_bint ); + }else{ + d_bint = NULL; + } }else{ d_model_engine = NULL; d_bint = NULL; @@ -256,7 +259,6 @@ void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< No bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ){ Assert( f.getKind()==FORALL ); - Assert( !f.hasAttribute(InstConstantAttribute()) ); Assert( vars.size()==terms.size() ); Node body = getInstantiation( f, vars, terms ); //make the lemma @@ -271,7 +273,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Trace("inst") << "*** Instantiate " << f << " with " << std::endl; uint64_t maxInstLevel = 0; for( int i=0; i<(int)terms.size(); i++ ){ - if( terms[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; for( int i=0; i<(int)terms.size(); i++ ){ Debug("inst") << " " << terms[i] << std::endl; @@ -437,8 +439,6 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ } bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){ - //Assert( !n1.hasAttribute(InstConstantAttribute()) ); - //Assert( !n2.hasAttribute(InstConstantAttribute()) ); //Assert( !areEqual( n1, n2 ) ); //Assert( !areDisequal( n1, n2 ) ); Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL; @@ -468,7 +468,6 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){ bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] ); nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst(preq) ); - d_term_db->setInstantiationConstantAttr( nodes[i], f ); nodeChanged = true; } //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index fe3e39d45..6903adda5 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -95,9 +95,8 @@ void RepSet::toStream(std::ostream& out){ } -RepSetIterator::RepSetIterator( RepSet* rs ) : d_rep_set( rs ){ +RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), d_rep_set( rs ){ d_incomplete = false; - } int RepSetIterator::domainSize( int i ) { @@ -108,25 +107,29 @@ int RepSetIterator::domainSize( int i ) { } } -bool RepSetIterator::setQuantifier( QuantifiersEngine * qe, Node f ){ +bool RepSetIterator::setQuantifier( Node f ){ + Trace("rsi") << "Make rsi for " << f << std::endl; Assert( d_types.empty() ); //store indicies for( size_t i=0; igetBoundedIntegers() ){ - Node l = qe->getBoundedIntegers()->getLowerBoundValue( f, f[0][i] ); - Node u = qe->getBoundedIntegers()->getUpperBoundValue( f, f[0][i] ); - if( !l.isNull() && !u.isNull() ){ - Trace("bound-int-reps") << "Can limit bounds of " << f[0][i] << " to " << l << "..." << u << std::endl; - Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); - Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); - if( ra==NodeManager::currentNM()->mkConst(true) ){ - long rr = range.getConst().getNumerator().getLong()+1; - if (rr<0) { - Trace("bound-int-reps") << "Empty bound range." << std::endl; - //empty - d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); - }else{ - Trace("bound-int-reps") << "Actual bound range is " << rr << std::endl; - d_lower_bounds[i] = l; - d_domain[i].push_back( (int)rr ); - d_enum_type.push_back( ENUM_RANGE ); - } - isSet = true; - }else{ - Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big." << std::endl; - d_incomplete = true; - } + if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ + if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){ + Trace("bound-int-rsi") << "Rep set iterator: variable #" << i << " is bounded integer." << std::endl; + d_enum_type.push_back( ENUM_RANGE ); + isSet = true; }else{ Trace("fmf-incomplete") << "Incomplete because of integer quantification, no bounds found." << std::endl; d_incomplete = true; @@ -197,6 +181,40 @@ bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){ } } } + //must set a variable index order + if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) { + Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; + std::vector< int > varOrder; + for( unsigned i=0; igetBoundedIntegers()->getNumBoundVars(d_owner); i++ ){ + varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i)); + } + for( unsigned i=0; igetBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { + varOrder.push_back(i); + } + } + Trace("bound-int-rsi") << "Variable order : "; + for( unsigned i=0; i indexOrder; + indexOrder.resize(varOrder.size()); + for( unsigned i=0; i& domain ){ } } */ +bool RepSetIterator::resetIndex( int i, bool initial ) { + d_index[i] = 0; + int ii = d_index_order[i]; + 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] ) ){ + 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( 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; + 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(); + d_lower_bounds[ii] = l; + if( ra==NodeManager::currentNM()->mkConst(true) ){ + long rr = range.getConst().getNumerator().getLong()+1; + Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; + d_domain[ii].push_back( (int)rr ); + }else{ + Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl; + d_incomplete = true; + d_domain[ii].push_back( 0 ); + } + } + }else{ + Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl; + } + } + return true; +} + void RepSetIterator::increment2( int counter ){ Assert( !isFinished() ); #ifdef DISABLE_EVAL_SKIP_MULTIPLE counter = (int)d_index.size()-1; #endif //increment d_index - while( counter>=0 && d_index[counter]==(int)(domainSize(counter)-1) ){ + Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl; + while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){ counter--; + if( counter>=0){ + Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl; + } } if( counter==-1 ){ d_index.clear(); }else{ + d_index[counter]++; for( int i=(int)d_index.size()-1; i>counter; i-- ){ - d_index[i] = 0; + if (!resetIndex(i)){ + break; + } } - d_index[counter]++; } } @@ -256,6 +317,7 @@ Node RepSetIterator::getTerm( int i ){ Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() ); return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]]; }else{ + Trace("rsi-debug") << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl; Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index], NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) ); t = Rewriter::rewrite( t ); diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index b92d9d2c6..fc8db420d 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -59,22 +59,26 @@ private: ENUM_DOMAIN_ELEMENTS, ENUM_RANGE, }; - + QuantifiersEngine * d_qe; //initialize function - bool initialize(QuantifiersEngine * qe, Node f); + bool initialize(); //enumeration type? std::vector< int > d_enum_type; //for enum ranges std::map< int, Node > d_lower_bounds; //domain size int domainSize( int i ); + //node this is rep set iterator is for + Node d_owner; + //reset index + bool resetIndex( int i, bool initial = false ); public: - RepSetIterator( RepSet* rs ); + RepSetIterator( QuantifiersEngine * qe, RepSet* rs ); ~RepSetIterator(){} //set that this iterator will be iterating over instantiations for a quantifier - bool setQuantifier( QuantifiersEngine * qe, Node f ); + bool setQuantifier( Node f ); //set that this iterator will be iterating over the domain of a function - bool setFunctionDomain( QuantifiersEngine * qe, Node op ); + bool setFunctionDomain( Node op ); public: //pointer to model RepSet* d_rep_set; diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index a4c111f86..4908e5ec0 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -137,14 +137,13 @@ class DumbPatMatcher: public PatMatcher{ /* The order of the matching is: reset arg1, nextMatch arg1, reset arg2, nextMatch arg2, ... */ ApplyMatcher::ApplyMatcher( Node pat, QuantifiersEngine* qe): d_pattern(pat){ - // Assert( pat.hasAttribute(InstConstantAttribute()) ); //set-up d_variables, d_constants, d_childrens for( size_t i=0; i< d_pattern.getNumChildren(); ++i ){ //EqualityQuery* q = qe->getEqualityQuery(d_pattern[i].getType()); EqualityQuery* q = qe->getEqualityQuery(); Assert( q != NULL ); - if( d_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(d_pattern[i]) ){ if( d_pattern[i].getKind()==INST_CONSTANT ){ //It's a variable d_variables.push_back(make_triple((TNode)d_pattern[i],i,q)); @@ -172,7 +171,7 @@ bool ApplyMatcher::reset(TNode t, InstMatch & m, QuantifiersEngine* qe){ //if t is null Assert( !t.isNull() ); - Assert( !t.hasAttribute(InstConstantAttribute()) ); + Assert( !quantifiers::TermDb::hasInstConstAttr(t) ); Assert( t.getKind()==d_pattern.getKind() ); Assert( (t.getKind()!=APPLY_UF && t.getKind()!=APPLY_CONSTRUCTOR) || t.getOperator()==d_pattern.getOperator() ); @@ -411,7 +410,7 @@ public: size_t numFreeVar(TNode t){ size_t n = 0; for( size_t i=0, size =t.getNumChildren(); i < size; ++i ){ - if( t[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(t[i]) ){ if( t[i].getKind()==INST_CONSTANT ){ //variable ++n; @@ -958,7 +957,7 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){ /** TODO: something simpler to see if the pattern is a good arithmetic pattern */ std::map< Node, Node > d_arith_coeffs; - if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ + if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){ Message() << "(?) Unknown matching pattern is " << pat << std::endl; Unimplemented("pattern not implemented"); return new DumbMatcher(); @@ -983,17 +982,17 @@ Matcher* mkMatcher( Node pat, QuantifiersEngine* qe ){ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){ Debug("inst-match-gen") << "Pattern term is " << pat << std::endl; - Assert( pat.hasAttribute(InstConstantAttribute()) ); + Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); if( pat.getKind()==kind::NOT && pat[0].getKind() == kind::EQUAL){ /* Difference */ return new UfDeqMatcher(pat, qe); } else if (pat.getKind() == kind::EQUAL){ - if( !pat[0].hasAttribute(InstConstantAttribute() )){ - Assert(pat[1].hasAttribute(InstConstantAttribute())); + if( !quantifiers::TermDb::hasInstConstAttr(pat[0])){ + Assert(quantifiers::TermDb::hasInstConstAttr(pat[1])); return new UfCstEqMatcher(pat[1], pat[0], qe); - }else if( !pat[1].hasAttribute(InstConstantAttribute() )){ - Assert(pat[0].hasAttribute(InstConstantAttribute())); + }else if( !quantifiers::TermDb::hasInstConstAttr(pat[1] )){ + Assert(quantifiers::TermDb::hasInstConstAttr(pat[0])); return new UfCstEqMatcher(pat[0], pat[1], qe); }else{ std::vector< Node > pats(pat.begin(),pat.end()); @@ -1009,7 +1008,7 @@ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){ /** TODO: something simpler to see if the pattern is a good arithmetic pattern */ std::map< Node, Node > d_arith_coeffs; - if( !Trigger::getPatternArithmetic( pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ){ + if( !Trigger::getPatternArithmetic( quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ){ Debug("inst-match-gen") << "(?) Unknown matching pattern is " << pat << std::endl; Message() << "(?) Unknown matching pattern is " << pat << std::endl; return new DumbPatMatcher(); @@ -1033,7 +1032,7 @@ PatMatcher* mkPattern( Node pat, QuantifiersEngine* qe ){ ArithMatcher::ArithMatcher(Node pat, QuantifiersEngine* qe): d_pattern(pat){ - if(Trigger::getPatternArithmetic(pat.getAttribute(InstConstantAttribute()), pat, d_arith_coeffs ) ) + if(Trigger::getPatternArithmetic(quantifiers::TermDb::getInstConstAttr(pat), pat, d_arith_coeffs ) ) { Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_pattern << std::endl; Assert(false); diff --git a/src/theory/rewriterules/rr_inst_match.h b/src/theory/rewriterules/rr_inst_match.h index 3ec9438fd..aa89430c1 100644 --- a/src/theory/rewriterules/rr_inst_match.h +++ b/src/theory/rewriterules/rr_inst_match.h @@ -67,7 +67,7 @@ public: /** legal candidate */ static inline bool isLegalCandidate( TNode n ){ return !n.getAttribute(NoMatchAttribute()) && - ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute())) && + ( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(n)) && ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) ); } diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp index 7e35be7ad..13250cf1b 100644 --- a/src/theory/rewriterules/rr_trigger.cpp +++ b/src/theory/rewriterules/rr_trigger.cpp @@ -65,7 +65,7 @@ bool Trigger::getNextMatch(){ int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( baseMatch, - d_nodes[0].getAttribute(InstConstantAttribute()), + quantifiers::TermDb::getInstConstAttr(d_nodes[0]), d_quantEngine); if( addedLemmas>0 ){ Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was "; @@ -91,7 +91,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& qe->getTermDatabase()->computeVarContains( temp[i] ); for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; - if( v.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(v)==f ){ if( vars.find( v )==vars.end() ){ vars[ v ] = true; foundVar = true; @@ -181,7 +181,7 @@ bool Trigger::isUsableTrigger( std::vector< Node >& nodes, Node f ){ } bool Trigger::isUsable( Node n, Node f ){ - if( n.getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n)==f ){ if( !isAtomicTrigger( n ) && n.getKind()!=INST_CONSTANT ){ std::map< Node, Node > coeffs; return getPatternArithmetic( f, n, coeffs ); @@ -201,7 +201,7 @@ bool Trigger::isUsable( Node n, Node f ){ bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + if( n[i].getKind()!=INST_CONSTANT && quantifiers::TermDb::hasInstConstAttr(n[i]) ){ return false; } } @@ -318,9 +318,9 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef Assert( coeffs.empty() ); NodeBuilder<> t(kind::PLUS); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(n[i]) ){ if( n[i].getKind()==INST_CONSTANT ){ - if( n[i].getAttribute(InstConstantAttribute())==f ){ + if( quantifiers::TermDb::getInstConstAttr(n[i])==f ){ coeffs[ n[i] ] = Node::null(); }else{ coeffs.clear(); @@ -343,12 +343,12 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef } return true; }else if( n.getKind()==MULT ){ - if( n[0].getKind()==INST_CONSTANT && n[0].getAttribute(InstConstantAttribute())==f ){ - Assert( !n[1].hasAttribute(InstConstantAttribute()) ); + if( n[0].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[0])==f ){ + Assert( !quantifiers::TermDb::hasInstConstAttr(n[1]) ); coeffs[ n[0] ] = n[1]; return true; - }else if( n[1].getKind()==INST_CONSTANT && n[1].getAttribute(InstConstantAttribute())==f ){ - Assert( !n[0].hasAttribute(InstConstantAttribute()) ); + }else if( n[1].getKind()==INST_CONSTANT && quantifiers::TermDb::getInstConstAttr(n[1])==f ){ + Assert( !quantifiers::TermDb::hasInstConstAttr(n[0]) ); coeffs[ n[1] ] = n[0]; return true; } diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h index f1a37d937..f02f38d0e 100644 --- a/src/theory/rewriterules/rr_trigger.h +++ b/src/theory/rewriterules/rr_trigger.h @@ -94,8 +94,7 @@ public: public: /** is usable trigger */ static inline bool isUsableTrigger( TNode n, TNode f ){ - //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF; - return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f ); + return quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f ); } static inline bool isAtomicTrigger( TNode n ){ return diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index 19cb3e987..a542214b2 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -263,7 +263,7 @@ private: rewriter::Subst & vars); //create inst variable - std::vector createInstVariable( std::vector & vars ); + std::vector createInstVariable( Node r, std::vector & vars ); /** statistics class */ class Statistics { diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp index 589556802..446d30d21 100644 --- a/src/theory/rewriterules/theory_rewriterules_rules.cpp +++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp @@ -151,7 +151,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r) vars.push_back(*v); }; /* Instantiation version */ - std::vector inst_constants = createInstVariable(vars); + std::vector inst_constants = createInstVariable(r,vars); /* Body/Remove_term/Guards/Triggers */ Node body = r[2][1]; TNode new_terms = r[2][1]; @@ -376,7 +376,7 @@ bool TheoryRewriteRules::addRewritePattern(TNode pattern, TNode body, } -std::vector TheoryRewriteRules::createInstVariable( std::vector & vars ){ +std::vector TheoryRewriteRules::createInstVariable( Node r, std::vector & vars ){ std::vector inst_constant; inst_constant.reserve(vars.size()); for( std::vector::const_iterator v = vars.begin(); @@ -384,6 +384,11 @@ std::vector TheoryRewriteRules::createInstVariable( std::vector & va //make instantiation constants Node ic = NodeManager::currentNM()->mkInstConstant( (*v).getType() ); inst_constant.push_back( ic ); + InstConstantAttribute ica; + ic.setAttribute(ica,r); + //also set the no-match attribute + NoMatchAttribute nma; + ic.setAttribute(nma,true); }; return inst_constant; } -- 2.30.2