From 66ee6c6472264be842f4e80a7106399d7f51d28a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Jun 2013 15:31:28 -0500 Subject: [PATCH] Make --var-elim-quant true by default. Add rewrite engine to quantifiers module. --- src/theory/quantifiers/Makefile.am | 4 +- .../quantifiers/inst_match_generator.cpp | 28 +++-- src/theory/quantifiers/inst_match_generator.h | 5 +- .../quantifiers/instantiation_engine.cpp | 4 + src/theory/quantifiers/model_builder.cpp | 7 +- src/theory/quantifiers/model_builder.h | 2 +- src/theory/quantifiers/model_engine.cpp | 9 +- src/theory/quantifiers/options | 4 +- .../quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers/rewrite_engine.cpp | 115 ++++++++++++++++++ src/theory/quantifiers/rewrite_engine.h | 51 ++++++++ src/theory/quantifiers/term_database.h | 5 + src/theory/quantifiers/trigger.cpp | 6 +- src/theory/quantifiers_engine.cpp | 16 ++- src/theory/quantifiers_engine.h | 16 ++- .../theory_rewriterules_rules.cpp | 6 +- 16 files changed, 242 insertions(+), 38 deletions(-) create mode 100755 src/theory/quantifiers/rewrite_engine.cpp create mode 100755 src/theory/quantifiers/rewrite_engine.h 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; iflushLemmas( &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 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; iresetInstantiationRound(); + 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 NodeBoolMap; + typedef context::CDHashMap NodeIntMap; + typedef context::CDHashMap 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 HasBoundVarAttribute; struct HasBoundVarComputedAttributeId {}; typedef expr::Attribute HasBoundVarComputedAttribute; +//for rewrite rules +struct QRewriteRuleAttributeId {}; +typedef expr::Attribute 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(patternB); forallB << static_cast(patternListB); - getOutputChannel().lemma((Node) forallB); + Node lem = (Node) forallB; + lem = Rewriter::rewrite(lem); + QRewriteRuleAttribute qra; + lem.setAttribute(qra,r); + getOutputChannel().lemma(lem); return; } -- 2.30.2