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 \
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);
}
}
/** 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;
}
//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 );
}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 );
}
/** 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 */
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 );
<< 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;
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;
d_addedLemmas = 0;
}
+bool QModelBuilder::isQuantifierActive( Node f ) {
+ return !f.hasAttribute(QRewriteRuleAttribute());
+}
+
bool QModelBuilder::optUseModel() {
return options::fmfModelBasedInst();
}
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 ){
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
}
}
}
- //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() ){
//}
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: ";
# 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
}
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;
--- /dev/null
+/********************* */\r
+/*! \file bounded_integers.cpp\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Rewrite engine module\r
+ **\r
+ ** This class manages rewrite rules for quantifiers\r
+ **/\r
+\r
+#include "theory/quantifiers/rewrite_engine.h"\r
+#include "theory/quantifiers/quant_util.h"\r
+#include "theory/quantifiers/first_order_model.h"\r
+#include "theory/quantifiers/model_engine.h"\r
+#include "theory/quantifiers/options.h"\r
+#include "theory/quantifiers/inst_match_generator.h"\r
+\r
+using namespace CVC4;\r
+using namespace std;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+using namespace CVC4::kind;\r
+\r
+RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) {\r
+\r
+}\r
+\r
+void RewriteEngine::check( Theory::Effort e ) {\r
+ if( e==Theory::EFFORT_FULL ){\r
+ //apply rewrite rules\r
+ int addedLemmas = 0;\r
+ for( unsigned i=0; i<d_rr_quant.size(); i++ ) {\r
+ addedLemmas += checkRewriteRule( d_rr_quant[i] );\r
+ }\r
+ Trace("rewrite-engine") << "Rewrite engine generated " << addedLemmas << " lemmas." << std::endl;\r
+ if (addedLemmas==0) {\r
+ }else{\r
+ //otherwise, the search will continue\r
+ d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );\r
+ }\r
+ }\r
+}\r
+\r
+int RewriteEngine::checkRewriteRule( Node f ) {\r
+ Trace("rewrite-engine-inst") << "Check " << f << "..." << std::endl;\r
+ int addedLemmas = 0;\r
+ //reset triggers\r
+ Node rr = f.getAttribute(QRewriteRuleAttribute());\r
+ if( d_rr_triggers.find(f)==d_rr_triggers.end() ){\r
+ std::vector< inst::Trigger * > triggers;\r
+ if( f.getNumChildren()==3 ){\r
+ for(unsigned i=0; i<f[2].getNumChildren(); i++ ){\r
+ Node pat = f[2][i];\r
+ std::vector< Node > nodes;\r
+ Trace("rewrite-engine-trigger") << "Trigger is : ";\r
+ for( int j=0; j<(int)pat.getNumChildren(); j++ ){\r
+ Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f );\r
+ nodes.push_back( p );\r
+ Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " ";\r
+ }\r
+ Trace("rewrite-engine-trigger") << std::endl;\r
+ Assert( inst::Trigger::isUsableTrigger( nodes, f ) );\r
+ inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false );\r
+ tr->getGenerator()->setActiveAdd(false);\r
+ triggers.push_back( tr );\r
+ }\r
+ }\r
+ d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() );\r
+ }\r
+ for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){\r
+ Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl;\r
+ d_rr_triggers[f][i]->resetInstantiationRound();\r
+ d_rr_triggers[f][i]->reset( Node::null() );\r
+ bool success;\r
+ do\r
+ {\r
+ InstMatch m;\r
+ success = d_rr_triggers[f][i]->getNextMatch( f, m );\r
+ if( success ){\r
+ //see if instantiation is true in the model\r
+ bool trueInModel = false;\r
+\r
+ if( !trueInModel ){\r
+ Trace("rewrite-engine-inst") << "Add instantiation : " << m << std::endl;\r
+ if( d_quantEngine->addInstantiation( f, m ) ){\r
+ addedLemmas++;\r
+ Trace("rewrite-engine-inst-debug") << "success" << std::endl;\r
+ }else{\r
+ Trace("rewrite-engine-inst-debug") << "failure." << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }while(success);\r
+ }\r
+ Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl;\r
+ return addedLemmas;\r
+}\r
+\r
+void RewriteEngine::registerQuantifier( Node f ) {\r
+ if( f.hasAttribute(QRewriteRuleAttribute()) ){\r
+ Trace("rewrite-engine") << "Register quantifier " << f << std::endl;\r
+ Node rr = f.getAttribute(QRewriteRuleAttribute());\r
+ Trace("rewrite-engine") << " rewrite rule is : " << rr << std::endl;\r
+ d_rr_quant.push_back( f );\r
+ }\r
+}\r
+\r
+void RewriteEngine::assertNode( Node n ) {\r
+\r
+}\r
+\r
--- /dev/null
+/********************* */\r
+/*! \file bounded_integers.h\r
+** \verbatim\r
+** Original author: Andrew Reynolds\r
+** This file is part of the CVC4 project.\r
+** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+** See the file COPYING in the top-level source directory for licensing\r
+** information.\endverbatim\r
+**\r
+** \brief This class manages integer bounds for quantifiers\r
+**/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__REWRITE_ENGINE_H\r
+#define __CVC4__REWRITE_ENGINE_H\r
+\r
+#include "theory/quantifiers_engine.h"\r
+#include "theory/quantifiers/trigger.h"\r
+\r
+#include "context/context.h"\r
+#include "context/context_mm.h"\r
+#include "context/cdchunk_list.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+\r
+class RewriteEngine : public QuantifiersModule\r
+{\r
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;\r
+ typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;\r
+ typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;\r
+ std::vector< Node > d_rr_quant;\r
+ /** explicitly provided patterns */\r
+ std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers;\r
+private:\r
+ int checkRewriteRule( Node f );\r
+public:\r
+ RewriteEngine( context::Context* c, QuantifiersEngine* qe );\r
+\r
+ void check( Theory::Effort e );\r
+ void registerQuantifier( Node f );\r
+ void assertNode( Node n );\r
+};\r
+\r
+}\r
+}\r
+}\r
+\r
+#endif
\ No newline at end of file
struct HasBoundVarComputedAttributeId {};
typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute;
+//for rewrite rules
+struct QRewriteRuleAttributeId {};
+typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
+
+
class QuantifiersEngine;
namespace inst{
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 );
}
}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] ) ){
}
}
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{
#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;
}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 );
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;
};/* 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 {
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 */
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;
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;
}
projects / cvc5.git / commitdiff