diff options
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.cpp')
-rwxr-xr-x | src/theory/quantifiers/rewrite_engine.cpp | 184 |
1 files changed, 184 insertions, 0 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp new file mode 100755 index 000000000..107a99014 --- /dev/null +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -0,0 +1,184 @@ +/********************* */ +/*! \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" +#include "theory/theory_engine.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +struct PrioritySort { + std::vector< double > d_priority; + bool operator() (int i,int j) { + return d_priority[i] < d_priority[j]; + } +}; + + +RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { + +} + +double RewriteEngine::getPriority( Node f ) { + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rrr = rr[2]; + Trace("rr-priority") << "Get priority : " << rrr << " " << rrr.getKind() << std::endl; + bool deterministic = rrr[1].getKind()!=OR; + if( rrr.getKind()==RR_REWRITE ){ + return deterministic ? 0.0 : 3.0; + }else if( rrr.getKind()==RR_DEDUCTION ){ + return deterministic ? 1.0 : 4.0; + }else if( rrr.getKind()==RR_REDUCTION ){ + return deterministic ? 2.0 : 5.0; + }else{ + return 6.0; + } +} + +void RewriteEngine::check( Theory::Effort e ) { + if( e==Theory::EFFORT_LAST_CALL ){ + if( !d_quantEngine->getModel()->isModelSet() ){ + d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true ); + } + if( d_true.isNull() ){ + d_true = NodeManager::currentNM()->mkConst( true ); + } + std::vector< Node > priority_order; + PrioritySort ps; + std::vector< int > indicies; + for( int i=0; i<(int)d_rr_quant.size(); i++ ){ + ps.d_priority.push_back( getPriority( d_rr_quant[i] ) ); + indicies.push_back( i ); + } + std::sort( indicies.begin(), indicies.end(), ps ); + for( unsigned i=0; i<indicies.size(); i++ ){ + priority_order.push_back( d_rr_quant[indicies[i]] ); + } + + //apply rewrite rules + int addedLemmas = 0; + //per priority level + int index = 0; + bool success = true; + while( success && index<(int)priority_order.size() ) { + addedLemmas += checkRewriteRule( priority_order[index] ); + index++; + if( index<(int)priority_order.size() ){ + success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] ); + } + } + + Trace("inst-engine") << "Rewrite engine added " << 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 << ", priority = " << getPriority( 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 + Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rrg = rr[1]; + std::vector< Node > vars; + std::vector< Node > terms; + d_quantEngine->computeTermVector( f, m, vars, terms ); + Trace("rewrite-engine-inst-debug") << "Instantiation : " << m << std::endl; + Node inst = d_rr_guard[f]; + inst = inst.substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + Trace("rewrite-engine-inst-debug") << "Try instantiation, guard : " << inst << std::endl; + FirstOrderModel * fm = d_quantEngine->getModel(); + Node v = fm->getValue( inst ); + Trace("rewrite-engine-inst-debug") << "Evaluated to " << v << std::endl; + if( v==d_true ){ + Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl; + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; + Trace("rewrite-engine-inst-debug") << "success" << std::endl; + //set the no-match attribute (the term is rewritten and can be ignored) + //Trace("rewrite-engine-inst-debug") << "We matched on : " << m.d_matched << std::endl; + //if( !m.d_matched.isNull() ){ + // NoMatchAttribute nma; + // m.d_matched.setAttribute(nma,true); + //} + }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 ); + d_rr_guard[f] = rr[1]; + Trace("rewrite-engine") << " guard is : " << d_rr_guard[f] << std::endl; + } +} + +void RewriteEngine::assertNode( Node n ) { + +} + |