diff options
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.cpp')
-rwxr-xr-x | src/theory/quantifiers/rewrite_engine.cpp | 368 |
1 files changed, 184 insertions, 184 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index e278de9e1..107a99014 100755 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -1,184 +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 ) {
-
-}
-
+/********************* */ +/*! \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 ) { + +} + |