summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriterules')
-rw-r--r--src/theory/rewriterules/rr_inst_match.cpp23
-rw-r--r--src/theory/rewriterules/rr_inst_match.h2
-rw-r--r--src/theory/rewriterules/rr_trigger.cpp20
-rw-r--r--src/theory/rewriterules/rr_trigger.h3
-rw-r--r--src/theory/rewriterules/theory_rewriterules.h2
-rw-r--r--src/theory/rewriterules/theory_rewriterules_rules.cpp9
6 files changed, 31 insertions, 28 deletions
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback