summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/Makefile.am4
-rw-r--r--src/theory/quantifiers/inst_match_generator.cpp28
-rw-r--r--src/theory/quantifiers/inst_match_generator.h5
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp4
-rw-r--r--src/theory/quantifiers/model_builder.cpp7
-rw-r--r--src/theory/quantifiers/model_builder.h2
-rw-r--r--src/theory/quantifiers/model_engine.cpp9
-rw-r--r--src/theory/quantifiers/options4
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp2
-rwxr-xr-xsrc/theory/quantifiers/rewrite_engine.cpp115
-rwxr-xr-xsrc/theory/quantifiers/rewrite_engine.h51
-rw-r--r--src/theory/quantifiers/term_database.h5
-rw-r--r--src/theory/quantifiers/trigger.cpp6
-rw-r--r--src/theory/quantifiers_engine.cpp16
-rw-r--r--src/theory/quantifiers_engine.h16
-rw-r--r--src/theory/rewriterules/theory_rewriterules_rules.cpp6
16 files changed, 242 insertions, 38 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 60f2ee7f7..0339fbcd8 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -48,7 +48,9 @@ libquantifiers_la_SOURCES = \
bounded_integers.h \
bounded_integers.cpp \
first_order_reasoning.h \
- first_order_reasoning.cpp
+ first_order_reasoning.cpp \
+ rewrite_engine.h \
+ rewrite_engine.cpp
EXTRA_DIST = \
kinds \
diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 87c39f046..50362340b 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -38,10 +38,10 @@ InstMatchGenerator::InstMatchGenerator( Node pat, int matchPolicy ) : d_matchPol
d_next = NULL;
}
-void InstMatchGenerator::setActiveAdd(){
- d_active_add = true;
+void InstMatchGenerator::setActiveAdd(bool val){
+ d_active_add = val;
if( d_next!=NULL ){
- d_next->setActiveAdd();
+ d_next->setActiveAdd(val);
}
}
@@ -310,18 +310,20 @@ bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEn
/** reset instantiation round */
void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
- if( d_match_pattern.isNull() ){
- for( int i=0; i<(int)d_children.size(); i++ ){
- d_children[i]->resetInstantiationRound( qe );
- }
- }else{
+ if( !d_match_pattern.isNull() ){
+ Debug("matching-debug2") << this << " reset instantiation round." << std::endl;
+ d_needsReset = true;
if( d_cg ){
d_cg->resetInstantiationRound();
}
}
+ if( d_next ){
+ d_next->resetInstantiationRound( qe );
+ }
}
void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
+ Debug("matching-debug2") << this << " reset " << eqc << "." << std::endl;
if( !eqc.isNull() ){
d_eq_class = eqc;
}
@@ -329,16 +331,22 @@ void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
//we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
//just look in equivalence class of the RHS
d_cg->reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class );
+ d_needsReset = false;
}
bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+ if( d_needsReset ){
+ Debug("matching") << "Reset not done yet, must do the reset..." << std::endl;
+ reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe );
+ }
m.d_matched = Node::null();
- //Debug("matching") << this << " " << d_pattern << " get next match 2 " << m << " in eq class " << d_eq_class << std::endl;
+ Debug("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
bool success = false;
Node t;
do{
//get the next candidate term t
t = d_cg->getNextCandidate();
+ Debug("matching-debug2") << "Matching candidate : " << t << std::endl;
//if t not null, try to fit it into match m
if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
success = getMatch( f, t, m, qe );
@@ -346,7 +354,7 @@ bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine*
}while( !success && !t.isNull() );
m.d_matched = t;
if( !success ){
- //Debug("matching") << this << " failed, reset " << d_eq_class << std::endl;
+ Debug("matching") << this << " failed, reset " << d_eq_class << std::endl;
//we failed, must reset
reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe );
}
diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 4c954fa81..9f856a56b 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -44,13 +44,14 @@ public:
/** add ground term t, called when t is added to term db */
virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;
/** set active add */
- virtual void setActiveAdd() {}
+ virtual void setActiveAdd( bool val ) {}
};/* class IMGenerator */
class CandidateGenerator;
class InstMatchGenerator : public IMGenerator {
private:
+ bool d_needsReset;
/** candidate generator */
CandidateGenerator* d_cg;
/** policy to use for matching */
@@ -108,7 +109,7 @@ public:
int addTerm( Node f, Node t, QuantifiersEngine* qe );
bool d_active_add;
- void setActiveAdd();
+ void setActiveAdd( bool val );
static InstMatchGenerator* mkInstMatchGenerator( Node pat, QuantifiersEngine* qe );
static InstMatchGenerator* mkInstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe );
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 77df69456..38ee4a57f 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -197,6 +197,7 @@ void InstantiationEngine::check( Theory::Effort e ){
<< d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ //it is not active if we have found the skolemized negation is unsat
if( options::cbqi() && hasAddedCbqiLemma( n ) ){
Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n );
bool active, value;
@@ -226,6 +227,9 @@ void InstantiationEngine::check( Theory::Effort e ){
Debug("quantifiers") << ", ce is asserted";
}
Debug("quantifiers") << std::endl;
+ //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
+ }else if( n.hasAttribute(QRewriteRuleAttribute()) ){
+ d_quant_active[n] = false;
}else{
d_quant_active[n] = true;
quantActive = true;
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 88fb7cd8f..fbf3ce59c 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -39,6 +39,10 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe
d_addedLemmas = 0;
}
+bool QModelBuilder::isQuantifierActive( Node f ) {
+ return !f.hasAttribute(QRewriteRuleAttribute());
+}
+
bool QModelBuilder::optUseModel() {
return options::fmfModelBasedInst();
@@ -355,7 +359,8 @@ QModelBuilderIG::Statistics::~Statistics(){
}
bool QModelBuilderIG::isQuantifierActive( Node f ){
- return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
+ return !f.hasAttribute(QRewriteRuleAttribute()) &&
+ ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
}
bool QModelBuilderIG::isTermActive( Node n ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 715612975..708688c60 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -37,7 +37,7 @@ public:
QModelBuilder( context::Context* c, QuantifiersEngine* qe );
virtual ~QModelBuilder(){}
// is quantifier active?
- virtual bool isQuantifierActive( Node f ) { return true; }
+ virtual bool isQuantifierActive( Node f );
//do exhaustive instantiation
virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) { return false; }
//whether to construct model
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 32deb9e47..0f756dcc0 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -168,14 +168,6 @@ int ModelEngine::checkModel(){
}
}
}
- //full model checking: construct models for all functions
- /*
- if( d_fmc.isActive() ){
- for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) {
- d_fmc.getModel(fm, it->first);
- }
- }
- */
//compute the relevant domain if necessary
//if( optUseRelevantDomain() ){
//}
@@ -227,6 +219,7 @@ int ModelEngine::checkModel(){
int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
int addedLemmas = 0;
+ //first check if the builder can do the exhaustive instantiation
if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){
Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
Debug("inst-fmf-ei") << " Instantiation Constants: ";
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index e83014789..a0e42c425 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -24,8 +24,8 @@ option prenexQuant /--disable-prenex-quant bool :default true
# Whether to variable-eliminate quantifiers.
# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
# forall y. P( c, y )
-option varElimQuant --var-elim-quant bool :default false
- enable variable elimination of quantified formulas
+option varElimQuant /--disable-var-elim-quant bool :default true
+ disable simple variable elimination for quantified formulas
# Whether to CNF quantifier bodies
option cnfQuant --cnf-quant bool :default false
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 9f156b656..b08752169 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -307,7 +307,7 @@ Node QuantifiersRewriter::computeSimpleIteLift( Node body ) {
}
Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
- Trace("var-elim-quant") << "Compute var elimination for " << body << std::endl;
+ Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
QuantPhaseReq qpr( body );
std::vector< Node > vars;
std::vector< Node > subs;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
new file mode 100755
index 000000000..5a35e3808
--- /dev/null
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -0,0 +1,115 @@
+/********************* */
+/*! \file bounded_integers.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Rewrite engine module
+ **
+ ** This class manages rewrite rules for quantifiers
+ **/
+
+#include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/inst_match_generator.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {
+
+}
+
+void RewriteEngine::check( Theory::Effort e ) {
+ if( e==Theory::EFFORT_FULL ){
+ //apply rewrite rules
+ int addedLemmas = 0;
+ for( unsigned i=0; i<d_rr_quant.size(); i++ ) {
+ addedLemmas += checkRewriteRule( d_rr_quant[i] );
+ }
+ Trace("rewrite-engine") << "Rewrite engine generated " << addedLemmas << " lemmas." << std::endl;
+ if (addedLemmas==0) {
+ }else{
+ //otherwise, the search will continue
+ d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
+ }
+ }
+}
+
+int RewriteEngine::checkRewriteRule( Node f ) {
+ Trace("rewrite-engine-inst") << "Check " << f << "..." << std::endl;
+ int addedLemmas = 0;
+ //reset triggers
+ Node rr = f.getAttribute(QRewriteRuleAttribute());
+ if( d_rr_triggers.find(f)==d_rr_triggers.end() ){
+ std::vector< inst::Trigger * > triggers;
+ if( f.getNumChildren()==3 ){
+ for(unsigned i=0; i<f[2].getNumChildren(); i++ ){
+ Node pat = f[2][i];
+ std::vector< Node > nodes;
+ Trace("rewrite-engine-trigger") << "Trigger is : ";
+ for( int j=0; j<(int)pat.getNumChildren(); j++ ){
+ Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f );
+ nodes.push_back( p );
+ Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " ";
+ }
+ Trace("rewrite-engine-trigger") << std::endl;
+ Assert( inst::Trigger::isUsableTrigger( nodes, f ) );
+ inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false );
+ tr->getGenerator()->setActiveAdd(false);
+ triggers.push_back( tr );
+ }
+ }
+ d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() );
+ }
+ for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){
+ Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl;
+ d_rr_triggers[f][i]->resetInstantiationRound();
+ d_rr_triggers[f][i]->reset( Node::null() );
+ bool success;
+ do
+ {
+ InstMatch m;
+ success = d_rr_triggers[f][i]->getNextMatch( f, m );
+ if( success ){
+ //see if instantiation is true in the model
+ bool trueInModel = false;
+
+ if( !trueInModel ){
+ Trace("rewrite-engine-inst") << "Add instantiation : " << m << std::endl;
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
+ Trace("rewrite-engine-inst-debug") << "success" << std::endl;
+ }else{
+ Trace("rewrite-engine-inst-debug") << "failure." << std::endl;
+ }
+ }
+ }
+ }while(success);
+ }
+ Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl;
+ return addedLemmas;
+}
+
+void RewriteEngine::registerQuantifier( Node f ) {
+ if( f.hasAttribute(QRewriteRuleAttribute()) ){
+ Trace("rewrite-engine") << "Register quantifier " << f << std::endl;
+ Node rr = f.getAttribute(QRewriteRuleAttribute());
+ Trace("rewrite-engine") << " rewrite rule is : " << rr << std::endl;
+ d_rr_quant.push_back( f );
+ }
+}
+
+void RewriteEngine::assertNode( Node n ) {
+
+}
+
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
new file mode 100755
index 000000000..5160af602
--- /dev/null
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -0,0 +1,51 @@
+/********************* */
+/*! \file bounded_integers.h
+** \verbatim
+** Original author: Andrew Reynolds
+** This file is part of the CVC4 project.
+** Copyright (c) 2009-2013 New York University and The University of Iowa
+** See the file COPYING in the top-level source directory for licensing
+** information.\endverbatim
+**
+** \brief This class manages integer bounds for quantifiers
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__REWRITE_ENGINE_H
+#define __CVC4__REWRITE_ENGINE_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/trigger.h"
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "context/cdchunk_list.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class RewriteEngine : public QuantifiersModule
+{
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
+ typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+ std::vector< Node > d_rr_quant;
+ /** explicitly provided patterns */
+ std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;
+private:
+ int checkRewriteRule( Node f );
+public:
+ RewriteEngine( context::Context* c, QuantifiersEngine* qe );
+
+ void check( Theory::Effort e );
+ void registerQuantifier( Node f );
+ void assertNode( Node n );
+};
+
+}
+}
+}
+
+#endif \ No newline at end of file
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 7b5df2ab8..fb5964554 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -64,6 +64,11 @@ typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute;
struct HasBoundVarComputedAttributeId {};
typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute;
+//for rewrite rules
+struct QRewriteRuleAttributeId {};
+typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
+
+
class QuantifiersEngine;
namespace inst{
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index fea8ab6d5..b71a1486c 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -44,7 +44,7 @@ d_quantEngine( qe ), d_f( f ){
d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
}else{
d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes[0], qe );
- d_mg->setActiveAdd();
+ d_mg->setActiveAdd(true);
}
}else{
d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption );
@@ -53,7 +53,7 @@ d_quantEngine( qe ), d_f( f ){
}
}else{
d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
- d_mg->setActiveAdd();
+ d_mg->setActiveAdd(true);
}
if( d_nodes.size()==1 ){
if( isSimpleTrigger( d_nodes[0] ) ){
@@ -301,7 +301,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
}
}
bool usable = quantifiers::TermDb::getInstConstAttr(n)==f && isAtomicTrigger( n ) && isUsable( n, f );
- Trace("usable") << n << " usable : " << usable << std::endl;
+ Trace("usable") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==f) << " " << isAtomicTrigger( n ) << " " << isUsable( n, f ) << std::endl;
if( usable ){
return n;
}else{
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c663e1aa2..94bc475d0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -28,6 +28,7 @@
#include "theory/rewriterules/efficient_e_matching.h"
#include "theory/rewriterules/rr_trigger.h"
#include "theory/quantifiers/bounded_integers.h"
+#include "theory/quantifiers/rewrite_engine.h"
using namespace std;
using namespace CVC4;
@@ -62,9 +63,15 @@ d_lemmas_produced_c(u){
}else{
d_inst_engine = NULL;
}
- if( options::finiteModelFind() ){
+ bool reqModel = options::finiteModelFind() || options::rewriteRulesAsAxioms();
+ if( reqModel ){
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
+ }else{
+ d_model_engine = NULL;
+ }
+
+ if( options::finiteModelFind() ){
if( options::fmfBoundInt() ){
d_bint = new quantifiers::BoundedIntegers( c, this );
d_modules.push_back( d_bint );
@@ -72,9 +79,14 @@ d_lemmas_produced_c(u){
d_bint = NULL;
}
}else{
- d_model_engine = NULL;
d_bint = NULL;
}
+ if( options::rewriteRulesAsAxioms() ){
+ d_rr_engine = new quantifiers::RewriteEngine( c, this );
+ d_modules.push_back(d_rr_engine);
+ }else{
+ d_rr_engine = NULL;
+ }
//options
d_optInstCheckDuplicate = true;
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2ff2100b2..40b043752 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -60,11 +60,13 @@ public:
};/* class QuantifiersModule */
namespace quantifiers {
- class InstantiationEngine;
- class ModelEngine;
class TermDb;
class FirstOrderModel;
+ //modules
+ class InstantiationEngine;
+ class ModelEngine;
class BoundedIntegers;
+ class RewriteEngine;
}/* CVC4::theory::quantifiers */
namespace inst {
@@ -88,10 +90,6 @@ private:
TheoryEngine* d_te;
/** vector of modules for quantifiers */
std::vector< QuantifiersModule* > d_modules;
- /** instantiation engine */
- quantifiers::InstantiationEngine* d_inst_engine;
- /** model engine */
- quantifiers::ModelEngine* d_model_engine;
/** equality query class */
EqualityQueryQuantifiersEngine* d_eq_query;
/** for computing relevance of quantifiers */
@@ -100,8 +98,14 @@ private:
std::map< Node, QuantPhaseReq* > d_phase_reqs;
/** efficient e-matcher */
EfficientEMatcher* d_eem;
+ /** instantiation engine */
+ quantifiers::InstantiationEngine* d_inst_engine;
+ /** model engine */
+ quantifiers::ModelEngine* d_model_engine;
/** bounded integers utility */
quantifiers::BoundedIntegers * d_bint;
+ /** rewrite rules utility */
+ quantifiers::RewriteEngine * d_rr_engine;
private:
/** list of all quantifiers seen */
std::vector< Node > d_quants;
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index 446d30d21..7e1d42bb2 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp
@@ -232,7 +232,11 @@ void TheoryRewriteRules::addRewriteRule(const Node r)
NodeBuilder<> patternListB(kind::INST_PATTERN_LIST);
patternListB << static_cast<Node>(patternB);
forallB << static_cast<Node>(patternListB);
- getOutputChannel().lemma((Node) forallB);
+ Node lem = (Node) forallB;
+ lem = Rewriter::rewrite(lem);
+ QRewriteRuleAttribute qra;
+ lem.setAttribute(qra,r);
+ getOutputChannel().lemma(lem);
return;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback