diff options
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]<d_curr_range ){
- Trace("bound-integers-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;
+ Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << d_lit_to_range[nlit] << std::endl;
d_curr_range = d_lit_to_range[nlit];
}
//set the range
@@ -76,11 +77,11 @@ void BoundedIntegers::RangeModel::assertNode(Node n) { void BoundedIntegers::RangeModel::allocateRange() {
d_curr_max++;
int newBound = d_curr_max;
- Trace("bound-integers-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
+ Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
//TODO: newBound should be chosen in a smarter way
Node ltr = NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) );
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; i<f[0].getNumChildren(); i++) {
+ numMap[f[0][i]] = i;
if( f[0][i].getType().isInteger() ){
hasIntType = true;
- break;
}
}
if( hasIntType ){
@@ -233,24 +235,56 @@ void BoundedIntegers::registerQuantifier( Node f ) { if( !isBound(f,v) ){
if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){
d_set[f].push_back(v);
+ d_set_nums[f].push_back(numMap[v]);
success = true;
}
}
}
}while( success );
- Trace("bound-integers") << "Bounds are : " << std::endl;
+ Trace("bound-int") << "Bounds are : " << std::endl;
for( unsigned i=0; i<d_set[f].size(); i++) {
Node v = d_set[f][i];
Node r = NodeManager::currentNM()->mkNode( 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; i<d_set[f].size(); i++) {
Node v = d_set[f][i];
Node r = d_range[f][v];
+ if( quantifiers::TermDb::hasBoundVarAttr(r) ){
+ //introduce a new bound
+ Node new_range = NodeManager::currentNM()->mkSkolem( "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; j<bvs.size(); j++) {
+ Node l = NodeManager::currentNM()->mkNode( 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; i<d_lit_to_ranges[nlit].size(); i++) {
Node r = d_lit_to_ranges[nlit][i];
- Trace("bound-integers-assert") << " ...this is a bounding literal for " << r << std::endl;
+ Trace("bound-int-assert") << " ...this is a bounding literal for " << r << std::endl;
d_rms[r]->assertNode( 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; i<d_ranges.size(); i++) {
Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();
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; i<d_set[f].size(); i++) {
+ if( d_set[f][i]!=v ){
+ Trace("bound-int-rsi") << "Look up the value for " << d_set[f][i] << " " << rsi->d_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<Node, bool, NodeHashFunction> 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;
@@ -73,6 +78,25 @@ private: //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:
BoundedIntegers( context::Context* c, QuantifiersEngine* qe );
@@ -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<Node> inst ) {
+Node Def::evaluate( FullModelChecker * m, std::vector<Node>& 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<Node> inst ) { }
}
-int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst ) {
+int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst ) {
return d_et.getGeneralizationIndex(m, inst);
}
@@ -163,7 +163,7 @@ void Def::simplify(FullModelChecker * m) { d_et.reset();
for (unsigned i=0; i<d_status.size(); i++) {
if( d_status[i]!=status_redundant ){
- addEntry(m, d_cond[i], d_value[i]);
+ addEntry(m, cond[i], value[i]);
}
}
d_status.clear();
@@ -435,108 +435,112 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {
Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
- if (effort==0) {
- //register the quantifier
- if (d_quant_cond.find(f)==d_quant_cond.end()) {
- std::vector< TypeNode > types;
- for(unsigned i=0; i<f[0].getNumChildren(); i++){
- types.push_back(f[0][i].getType());
- d_quant_var_id[f][f[0][i]] = i;
- }
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( 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<d_quant_models[f].d_cond.size(); i++) {
- if( d_quant_models[f].d_value[i]!=d_true) {
- Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
- bool hasStar = false;
- std::vector< Node > inst;
- for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
- if (isStar(d_quant_models[f].d_cond[i][j])) {
- hasStar = true;
- inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
- }else{
- inst.push_back(d_quant_models[f].d_cond[i][j]);
- }
+ if (!options::fmfModelBasedInst()) {
+ return false;
+ }else{
+ if (effort==0) {
+ //register the quantifier
+ if (d_quant_cond.find(f)==d_quant_cond.end()) {
+ std::vector< TypeNode > types;
+ for(unsigned i=0; i<f[0].getNumChildren(); i++){
+ types.push_back(f[0][i].getType());
+ d_quant_var_id[f][f[0][i]] = i;
}
- bool addInst = true;
- if( hasStar ){
- //try obvious (specified by inst)
- Node ev = d_quant_models[f].evaluate(this, inst);
- if (ev==d_true) {
- addInst = false;
- }
- }else{
- //for debugging
- if (Trace.isOn("fmc-test-inst")) {
- Node ev = d_quant_models[f].evaluate(this, inst);
- if( ev==d_true ){
- std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
- exit(0);
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( 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<d_quant_models[f].d_cond.size(); i++) {
+ if( d_quant_models[f].d_value[i]!=d_true) {
+ Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;
+ bool hasStar = false;
+ std::vector< Node > inst;
+ for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
+ if (isStar(d_quant_models[f].d_cond[i][j])) {
+ hasStar = true;
+ inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
}else{
- Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
+ inst.push_back(d_quant_models[f].d_cond[i][j]);
}
}
- }
- if( addInst ){
- InstMatch m;
- for( unsigned j=0; j<inst.size(); j++) {
- m.set( d_qe, f, j, inst[j] );
+ bool addInst = true;
+ if( hasStar ){
+ //try obvious (specified by inst)
+ Node ev = d_quant_models[f].evaluate(this, inst);
+ if (ev==d_true) {
+ addInst = false;
+ }
+ }else{
+ //for debugging
+ if (Trace.isOn("fmc-test-inst")) {
+ Node ev = d_quant_models[f].evaluate(this, inst);
+ if( ev==d_true ){
+ std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
+ exit(0);
+ }else{
+ Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;
+ }
+ }
}
- if( d_qe->addInstantiation( f, m ) ){
- lemmas++;
+ if( addInst ){
+ InstMatch m;
+ for( unsigned j=0; j<inst.size(); j++) {
+ m.set( d_qe, f, j, inst[j] );
+ }
+ if( d_qe->addInstantiation( 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; i<c.getNumChildren(); i++) {
TypeNode tn = c[i].getType();
@@ -996,4 +1000,20 @@ Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const cha }
curr = Rewriter::rewrite( curr );
return NodeManager::currentNM()->mkNode(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; i<args.size(); i++) {
+ args[i] = getRepresentative(fm, args[i]);
+ }
+ if( n.getKind()==VARIABLE ){
+ Node r = getRepresentative(fm, n);
+ return r;
+ }else if( n.getKind()==APPLY_UF ){
+ getModel(fm, n.getOperator());
+ return d_models[n.getOperator()]->evaluate(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<Node> inst );
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );
+ Node evaluate( FullModelChecker * m, std::vector<Node>& inst );
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& 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<n.getNumChildren(); i++ ){ - if( n[i].getKind()!=INST_CONSTANT && n[i].hasAttribute(InstConstantAttribute()) ){ + if( n[i].getKind()!=INST_CONSTANT && TermDb::hasInstConstAttr(n[i]) ){ d_children.push_back( InstGenProcess( n[i] ) ); d_children_index.push_back( i ); d_children_map[ i ] = count; diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index d4988f223..d55f72a88 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -143,7 +143,7 @@ void InstMatch::set(TNode var, TNode n){ if (Trace.isOn("inst-match-warn")) { // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){ - Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl; + Trace("inst-match-warn") << quantifiers::TermDb::getInstConstAttr(var) << std::endl; Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ; } } diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 105575c49..87c39f046 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -32,7 +32,7 @@ namespace inst { InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPolicy( matchPolicy ){ d_active_add = false; - Assert( pat.hasAttribute(InstConstantAttribute()) ); + Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); d_pattern = pat; d_match_pattern = pat; d_next = NULL; @@ -53,9 +53,9 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat d_match_pattern = d_pattern[0]; } if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ - if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) || + if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) || d_match_pattern[0].getKind()==INST_CONSTANT ){ - Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) ); + Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) ); Node mp = d_match_pattern[1]; //swap sides Node pat = d_pattern; @@ -67,9 +67,9 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern; d_match_pattern = mp; - }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) || + }else if( !quantifiers::TermDb::hasInstConstAttr(d_match_pattern[1]) || d_match_pattern[1].getKind()==INST_CONSTANT ){ - Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) ); + Assert( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[0]) ); if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching d_match_pattern = d_match_pattern[0]; }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){ @@ -79,7 +79,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat } int childMatchPolicy = MATCH_GEN_DEFAULT; for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ if( d_match_pattern[i].getKind()!=INST_CONSTANT && !Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ InstMatchGenerator * cimg = new InstMatchGenerator( d_match_pattern[i], childMatchPolicy ); d_children.push_back( cimg ); @@ -127,7 +127,7 @@ void InstMatchGenerator::initialize( QuantifiersEngine* qe, std::vector< InstMat d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() ); }else{ d_cg = new CandidateGeneratorQueue; - if( !Trigger::isArithmeticTrigger( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){ + if( !Trigger::isArithmeticTrigger( quantifiers::TermDb::getInstConstAttr(d_match_pattern), d_match_pattern, d_arith_coeffs ) ){ Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; //Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl; d_matchPolicy = MATCH_GEN_INTERNAL_ERROR; @@ -161,12 +161,12 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi InstMatch prev( &m ); //if t is null Assert( !t.isNull() ); - Assert( !t.hasAttribute(InstConstantAttribute()) ); + Assert( !quantifiers::TermDb::hasInstConstAttr(t) ); Assert( t.getKind()==d_match_pattern.getKind() ); Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() ); //first, check if ground arguments are not equal, or a match is in conflict for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){ - if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){ + if( quantifiers::TermDb::hasInstConstAttr(d_match_pattern[i]) ){ if( d_match_pattern[i].getKind()==INST_CONSTANT || Trigger::isBooleanTermTrigger( d_match_pattern[i] ) ){ Node vv = d_match_pattern[i]; Node tt = t[i]; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index dbdf95613..a5031a061 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -143,8 +143,8 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){ void InstStrategySimplex::addTermToRow( ArithVar x, Node n, Node& f, NodeBuilder<>& 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<possibleCons.size(); j++ ) { - if( possibleCons[j] ){ - tIndex = j; - break; - } - } - } - Assert( tIndex!=-1 ); - Node cons = Node::fromExpr( dt[ tIndex ].getConstructor() ); - Debug("quant-datatypes-debug") << n << " cons is " << cons << std::endl; - std::vector< Node > 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; i<n.getNumChildren(); i++) { + Node nc = getCurrentModelValue( fm, n[i] ); + if (nc.isNull()) { + return Node::null(); + }else{ + children.push_back( nc ); + } + } + if( n.getKind()==APPLY_UF ){ + return getCurrentUfModelValue( fm, n, children, partial ); + }else{ + Node nn = NodeManager::currentNM()->mkNode( 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<riter.getNumTerms(); i++ ){ @@ -410,7 +444,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ // constant definitions. bool isConst = true; std::vector< Node > 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<d_quant_selection_lit_candidates[f].size(); i++ ){ bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT; Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i]; - Assert( lit.hasAttribute(InstConstantAttribute()) ); + Assert( TermDb::hasInstConstAttr(lit) ); std::vector< Node > 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; e<e_max; e++) { if (addedLemmas==0) { for( int i=0; i<fm->getNumAssertedQuantifiers(); 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<n.getNumChildren(); i++) { + if( hasBoundVarAttr(n[i]) ){ + hasBv = true; + break; + } + } + } + HasBoundVarAttribute hbva; + n.setAttribute(hbva, hasBv); + HasBoundVarComputedAttribute hbvca; + n.setAttribute(hbvca, true); + Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl; + } + return n.getAttribute(HasBoundVarAttribute()); +} + +void TermDb::getBoundVars( Node n, std::vector< Node >& 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<n.getNumChildren(); i++) { + getBoundVars(n[i], bvs); + } + } +} + + /** get the i^th instantiation constant of f */ Node TermDb::getInstantiationConstant( Node f, int i ) const { std::map< Node, std::vector< Node > >::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<Node> & 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<ModelBasisAttributeId, bool> ModelBasisAttribute; struct ModelBasisArgAttributeId {}; typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute; +struct HasBoundVarAttributeId {}; +typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute; +struct HasBoundVarComputedAttributeId {}; +typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute; class QuantifiersEngine; @@ -186,9 +190,15 @@ public: Node convertNodeToPattern( Node n, Node f, const std::vector<Node> & vars, const std::vector<Node> & 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<bool>(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; i<f[0].getNumChildren(); i++ ){ d_types.push_back( f[0][i].getType() ); } - return initialize(qe, f); + d_owner = f; + return initialize(); } -bool RepSetIterator::setFunctionDomain( QuantifiersEngine * qe, Node op ){ +bool RepSetIterator::setFunctionDomain( Node op ){ + Trace("rsi") << "Make rsi for " << op << std::endl; Assert( d_types.empty() ); TypeNode tn = op.getType(); for( size_t i=0; i<tn.getNumChildren()-1; i++ ){ d_types.push_back( tn[i] ); } - return initialize(qe, Node::null()); + d_owner = op; + return initialize(); } -bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){ +bool RepSetIterator::initialize(){ for( size_t i=0; i<d_types.size(); i++ ){ d_index.push_back( 0 ); //store default index order @@ -144,30 +147,11 @@ bool RepSetIterator::initialize(QuantifiersEngine * qe, Node f){ } }else if( tn.isInteger() ){ //check if it is bound - if( !f.isNull() && qe && qe->getBoundedIntegers() ){ - 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<Rational>().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; i<d_qe->getBoundedIntegers()->getNumBoundVars(d_owner); i++ ){ + varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i)); + } + for( unsigned i=0; i<d_owner[0].getNumChildren(); i++) { + if( !d_qe->getBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { + varOrder.push_back(i); + } + } + Trace("bound-int-rsi") << "Variable order : "; + for( unsigned i=0; i<varOrder.size(); i++) { + Trace("bound-int-rsi") << varOrder[i] << " "; + } + Trace("bound-int-rsi") << std::endl; + std::vector< int > indexOrder; + indexOrder.resize(varOrder.size()); + for( unsigned i=0; i<varOrder.size(); i++){ + indexOrder[varOrder[i]] = i; + } + Trace("bound-int-rsi") << "Will use index order : "; + for( unsigned i=0; i<indexOrder.size(); i++) { + Trace("bound-int-rsi") << indexOrder[i] << " "; + } + Trace("bound-int-rsi") << std::endl; + setIndexOrder(indexOrder); + } + for (unsigned i=0; i<d_index.size(); i++) { + if (!resetIndex(i, true)){ + break; + } + } return true; } @@ -220,22 +238,65 @@ void RepSetIterator::setDomain( std::vector< RepDomain >& 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<Rational>().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<Node> createInstVariable( std::vector<Node> & vars ); + std::vector<Node> createInstVariable( Node r, std::vector<Node> & 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<Node> inst_constants = createInstVariable(vars); + std::vector<Node> 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<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & vars ){ +std::vector<Node> TheoryRewriteRules::createInstVariable( Node r, std::vector<Node> & vars ){ std::vector<Node> inst_constant; inst_constant.reserve(vars.size()); for( std::vector<Node>::const_iterator v = vars.begin(); @@ -384,6 +384,11 @@ std::vector<Node> TheoryRewriteRules::createInstVariable( std::vector<Node> & 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; } |