From 8a672c060d2b3946c542c82bd6ca8f89892216ee Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Nov 2012 22:58:53 +0000 Subject: [PATCH] replaced all static member data from rewrite rule triggers, added infrastructure for recognizing quantifier macros --- src/smt/smt_engine.cpp | 40 +++-- src/theory/arith/theory_arith.cpp | 2 +- src/theory/quantifiers/Makefile.am | 4 +- src/theory/quantifiers/macros.cpp | 128 +++++++++++++ src/theory/quantifiers/macros.h | 51 ++++++ src/theory/quantifiers/options | 4 + src/theory/quantifiers/term_database.cpp | 71 ++++++++ src/theory/quantifiers/term_database.h | 9 + src/theory/quantifiers/trigger.cpp | 76 +------- src/theory/quantifiers/trigger.h | 4 - src/theory/quantifiers_engine.cpp | 2 + src/theory/quantifiers_engine.h | 8 + src/theory/rewriterules/rr_trigger.cpp | 217 +++++------------------ src/theory/rewriterules/rr_trigger.h | 67 +++---- 14 files changed, 367 insertions(+), 316 deletions(-) create mode 100755 src/theory/quantifiers/macros.cpp create mode 100755 src/theory/quantifiers/macros.h diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e1c30c6c7..16de7957a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -65,6 +65,7 @@ #include "prop/options.h" #include "theory/arrays/options.h" #include "util/sort_inference.h" +#include "theory/quantifiers/macros.h" using namespace std; using namespace CVC4; @@ -1131,32 +1132,32 @@ void SmtEngine::defineFunction(Expr func, Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) { - NodeManager* nm = d_smt.d_nodeManager; + NodeManager* nm = d_smt.d_nodeManager; if (k == kind::BITVECTOR_UDIV) { if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) { // lazily create the function symbols std::ostringstream os; - os << "BVUDivByZero_" << width; + os << "BVUDivByZero_" << width; Node divByZero = nm->mkSkolem(os.str(), nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME); - d_BVDivByZero[width] = divByZero; + d_BVDivByZero[width] = divByZero; } - return d_BVDivByZero[width]; + return d_BVDivByZero[width]; } else if (k == kind::BITVECTOR_UREM) { if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) { std::ostringstream os; - os << "BVURemByZero_" << width; + os << "BVURemByZero_" << width; Node divByZero = nm->mkSkolem(os.str(), nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)), "partial bvurem", NodeManager::SKOLEM_EXACT_NAME); d_BVRemByZero[width] = divByZero; } - return d_BVRemByZero[width]; - } + return d_BVRemByZero[width]; + } - Unreachable(); + Unreachable(); } @@ -1164,15 +1165,15 @@ Node SmtEnginePrivate::expandBVDivByZero(TNode n) { // we only deal wioth the unsigned division operators as the signed ones should have been // expanded in terms of the unsigned operators NodeManager* nm = d_smt.d_nodeManager; - unsigned width = n.getType().getBitVectorSize(); + unsigned width = n.getType().getBitVectorSize(); Node divByZero = getBVDivByZero(n.getKind(), width); TNode num = n[0], den = n[1]; - Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0)))); + Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0)))); Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num); Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL, num, den); - Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); - return node; + Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + return node; } @@ -1205,12 +1206,12 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map + +#include "theory/quantifiers/macros.h" + +using namespace CVC4; +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; +using namespace CVC4::context; + +void QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ + //first, collect macro definitions + for( size_t i=0; i args; + for( size_t j=0; j& args, Node f ){ + if( n.getKind()==NOT ){ + process( n[0], !pol, args, f ); + }else if( n.getKind()==AND || n.getKind()==OR || n.getKind()==IMPLIES ){ + //bool favorPol = (n.getKind()==AND)==pol; + //conditional? + }else if( n.getKind()==ITE ){ + //can not do anything + }else{ + //literal case + //only care about literals in form of (basis, definition) + if( isMacroKind( n, pol ) ){ + for( int i=0; i<2; i++ ){ + int j = i==0 ? 1 : 0; + //check if n[i] is the basis for a macro + if( n[i].getKind()==APPLY_UF ){ + //make sure it doesn't occur in the potential definition + if( !containsOp( n[j], n[i].getOperator() ) ){ + //bool usable = true; + //for( size_j a=0; a children; + bool childChanged = false; + for( size_t i=0; i vars; + for( size_t i = 0; imkNode( n.getKind(), children ); + }else{ + return n; + } +#else + return n; +#endif +} diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h new file mode 100755 index 000000000..d93070481 --- /dev/null +++ b/src/theory/quantifiers/macros.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \file macros.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Pre-process step for detecting quantifier macro definitions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_MACROS_H +#define __CVC4__QUANTIFIERS_MACROS_H + +#include +#include +#include +#include +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class QuantifierMacros{ +private: + void process( Node n, bool pol, std::vector< Node >& args, Node f ); + bool containsOp( Node n, Node op ); + bool isMacroKind( Node n, bool pol ); + //map from operators to macro definition ( basis, definition ) + std::map< Node, std::pair< Node, Node > > d_macro_defs; +private: + Node simplify( Node n ); +public: + QuantifierMacros(){} + ~QuantifierMacros(){} + + void simplify( std::vector< Node >& assertions, bool doRewrite = false ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 2c36520e4..24d0c4047 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -37,6 +37,10 @@ option cnfQuant --cnf-quant bool :default false option preSkolemQuant --pre-skolem-quant bool :default false apply skolemization eagerly to bodies of quantified formulas +# Whether to perform quantifier macro expansion +option macrosQuant --macros-quant bool :default false + perform quantifiers macro expansions + # Whether to use smart triggers option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index b55e8abdf..2c2ee0bfe 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -468,6 +468,77 @@ void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContain } } +/** is n1 an instance of n2 or vice versa? */ +int TermDb::isInstanceOf( Node n1, Node n2 ){ + if( n1==n2 ){ + return 1; + }else if( n1.getKind()==n2.getKind() ){ + if( n1.getKind()==APPLY_UF ){ + if( n1.getOperator()==n2.getOperator() ){ + int result = 0; + for( int i=0; i<(int)n1.getNumChildren(); i++ ){ + if( n1[i]!=n2[i] ){ + int cResult = isInstanceOf( n1[i], n2[i] ); + if( cResult==0 ){ + return 0; + }else if( cResult!=result ){ + if( result!=0 ){ + return 0; + }else{ + result = cResult; + } + } + } + } + return result; + } + } + return 0; + }else if( n2.getKind()==INST_CONSTANT ){ + computeVarContains( n1 ); + //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ + // return 1; + //} + if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){ + return 1; + } + }else if( n1.getKind()==INST_CONSTANT ){ + computeVarContains( n2 ); + //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ + // return -1; + //} + if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){ + return 1; + } + } + return 0; +} + +void TermDb::filterInstances( std::vector< Node >& nodes ){ + std::vector< bool > active; + active.resize( nodes.size(), true ); + for( int i=0; i<(int)nodes.size(); i++ ){ + for( int j=i+1; j<(int)nodes.size(); j++ ){ + if( active[i] && active[j] ){ + int result = isInstanceOf( nodes[i], nodes[j] ); + if( result==1 ){ + active[j] = false; + }else if( result==-1 ){ + active[i] = false; + } + } + } + } + std::vector< Node > temp; + for( int i=0; i<(int)nodes.size(); i++ ){ + if( active[i] ){ + temp.push_back( nodes[i] ); + } + } + nodes.clear(); + nodes.insert( nodes.begin(), temp.begin(), temp.end() ); +} + void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ d_op_triggers[op].push_back( tr ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 2bae5a043..a1f1de1dc 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -65,6 +65,10 @@ class QuantifiersEngine; namespace inst{ class Trigger; } +namespace rrinst{ + class Trigger; +} + namespace quantifiers { @@ -82,6 +86,7 @@ public: class TermDb { friend class ::CVC4::theory::QuantifiersEngine; friend class ::CVC4::theory::inst::Trigger; + friend class ::CVC4::theory::rrinst::Trigger; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -218,6 +223,10 @@ public: void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); /** register trigger (for eager quantifier instantiation) */ void registerTrigger( inst::Trigger* tr, Node op ); + /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ + int isInstanceOf( Node n1, Node n2 ); + /** filter all nodes that have instances */ + void filterInstances( std::vector< Node >& nodes ); };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 67b2e6bd8..a9c5e8b96 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -250,32 +250,6 @@ bool Trigger::isSimpleTrigger( Node n ){ } } -/** filter all nodes that have instances */ -void Trigger::filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes ){ - std::vector< bool > active; - active.resize( nodes.size(), true ); - for( int i=0; i<(int)nodes.size(); i++ ){ - for( int j=i+1; j<(int)nodes.size(); j++ ){ - if( active[i] && active[j] ){ - int result = isInstanceOf( qe, nodes[i], nodes[j] ); - if( result==1 ){ - active[j] = false; - }else if( result==-1 ){ - active[i] = false; - } - } - } - } - std::vector< Node > temp; - for( int i=0; i<(int)nodes.size(); i++ ){ - if( active[i] ){ - temp.push_back( nodes[i] ); - } - } - nodes.clear(); - nodes.insert( nodes.begin(), temp.begin(), temp.end() ); -} - bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ if( patMap.find( n )==patMap.end() ){ @@ -345,7 +319,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto collectPatTerms( qe, f, n, patTerms2, TS_ALL, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); - filterInstances( qe, temp ); + qe->getTermDatabase()->filterInstances( temp ); if( temp.size()!=patTerms2.size() ){ Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl; Debug("trigger-filter-instance") << "Old: "; @@ -378,54 +352,6 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } -/** is n1 an instance of n2 or vice versa? */ -int Trigger::isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 ){ - if( n1==n2 ){ - return 1; - }else if( n1.getKind()==n2.getKind() ){ - if( n1.getKind()==APPLY_UF ){ - if( n1.getOperator()==n2.getOperator() ){ - int result = 0; - for( int i=0; i<(int)n1.getNumChildren(); i++ ){ - if( n1[i]!=n2[i] ){ - int cResult = isInstanceOf( qe, n1[i], n2[i] ); - if( cResult==0 ){ - return 0; - }else if( cResult!=result ){ - if( result!=0 ){ - return 0; - }else{ - result = cResult; - } - } - } - } - return result; - } - } - return 0; - }else if( n2.getKind()==INST_CONSTANT ){ - qe->getTermDatabase()->computeVarContains( n1 ); - //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ - // return 1; - //} - if( qe->getTermDatabase()->d_var_contains[ n1 ].size()==1 && - qe->getTermDatabase()->d_var_contains[ n1 ][ 0 ]==n2 ){ - return 1; - } - }else if( n1.getKind()==INST_CONSTANT ){ - qe->getTermDatabase()->computeVarContains( n2 ); - //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ - // return -1; - //} - if( qe->getTermDatabase()->d_var_contains[ n2 ].size()==1 && - qe->getTermDatabase()->d_var_contains[ n2 ][ 0 ]==n1 ){ - return 1; - } - } - return 0; -} - bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ if( n.getKind()==PLUS ){ Assert( coeffs.empty() ); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 267debb02..6fcd316f4 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -108,10 +108,6 @@ public: static bool isUsableTrigger( Node n, Node f ); static bool isAtomicTrigger( Node n ); static bool isSimpleTrigger( Node n ); - /** filter all nodes that have instances */ - static void filterInstances( QuantifiersEngine* qe, std::vector< Node >& nodes ); - /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - static int isInstanceOf( QuantifiersEngine* qe, Node n1, Node n2 ); /** get pattern arithmetic */ static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3f6ba8a0f..b4e046506 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/rewriterules/efficient_e_matching.h" +#include "theory/rewriterules/rr_trigger.h" using namespace std; using namespace CVC4; @@ -40,6 +41,7 @@ d_quant_rel( false ){ //currently do not care about relevance d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); d_tr_trie = new inst::TriggerTrie; + d_rr_tr_trie = new rrinst::TriggerTrie; d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 8fc6253ac..20972a6a1 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -68,6 +68,10 @@ namespace inst { class TriggerTrie; }/* CVC4::theory::inst */ +namespace rrinst { + class TriggerTrie; +}/* CVC4::theory::inst */ + class EfficientEMatcher; class EqualityQueryQuantifiersEngine; @@ -108,6 +112,8 @@ private: quantifiers::TermDb* d_term_db; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; + /** all triggers for rewrite rules will be stored in this trie */ + rrinst::TriggerTrie* d_rr_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; private: @@ -193,6 +199,8 @@ public: quantifiers::TermDb* getTermDatabase() { return d_term_db; } /** get trigger database */ inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; } + /** get rewrite trigger database */ + rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false ); public: diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp index 545c47bcd..ad77f0bcb 100644 --- a/src/theory/rewriterules/rr_trigger.cpp +++ b/src/theory/rewriterules/rr_trigger.cpp @@ -26,43 +26,9 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::rrinst; -//#define NESTED_PATTERN_SELECTION - -Trigger* Trigger::TrTrie::getTrigger2( std::vector< Node >& nodes ){ - if( nodes.empty() ){ - return d_tr; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )!=d_children.end() ){ - return d_children[n]->getTrigger2( nodes ); - }else{ - return NULL; - } - } -} -void Trigger::TrTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ - if( nodes.empty() ){ - d_tr = t; - }else{ - Node n = nodes.back(); - nodes.pop_back(); - if( d_children.find( n )==d_children.end() ){ - d_children[n] = new TrTrie; - } - d_children[n]->addTrigger2( nodes, t ); - } -} - -/** trigger static members */ -std::map< Node, std::vector< Node > > Trigger::d_var_contains; -int Trigger::trCount = 0; -Trigger::TrTrie Trigger::d_tr_trie; - /** trigger class constructor */ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) : d_quantEngine( qe ), d_f( f ){ - trCount++; d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); Debug("trigger") << "Trigger for " << f << ": " << d_nodes << std::endl; if(matchOption == MATCH_GEN_DEFAULT) d_mg = mkPatterns( d_nodes, qe ); @@ -80,24 +46,6 @@ d_quantEngine( qe ), d_f( f ){ ++(qe->d_statistics.d_multi_triggers); } } -void Trigger::computeVarContains( Node n ) { - if( d_var_contains.find( n )==d_var_contains.end() ){ - d_var_contains[n].clear(); - computeVarContains2( n, n ); - } -} - -void Trigger::computeVarContains2( Node n, Node parent ){ - if( n.getKind()==INST_CONSTANT ){ - if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){ - d_var_contains[parent].push_back( n ); - } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeVarContains2( n[i], parent ); - } - } -} void Trigger::resetInstantiationRound(){ d_mg->resetInstantiationRound( d_quantEngine ); @@ -141,9 +89,9 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& std::map< Node, std::vector< Node > > patterns; for( int i=0; i<(int)temp.size(); i++ ){ bool foundVar = false; - computeVarContains( temp[i] ); - for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ - Node v = d_var_contains[ temp[i] ][j]; + qe->getTermDatabase()->computeVarContains( temp[i] ); + for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ + Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; if( v.getAttribute(InstConstantAttribute())==f ){ if( vars.find( v )==vars.end() ){ vars[ v ] = true; @@ -153,8 +101,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } if( foundVar ){ trNodes.push_back( temp[i] ); - for( int j=0; j<(int)d_var_contains[ temp[i] ].size(); j++ ){ - Node v = d_var_contains[ temp[i] ][j]; + for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ + Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; patterns[ v ].push_back( temp[i] ); } } @@ -163,8 +111,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& for( int i=0; i<(int)trNodes.size(); i++ ){ bool keepPattern = false; Node n = trNodes[i]; - for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ - Node v = d_var_contains[ n ][j]; + for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ + Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; if( patterns[v].size()==1 ){ keepPattern = true; break; @@ -172,8 +120,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } if( !keepPattern ){ //remove from pattern vector - for( int j=0; j<(int)d_var_contains[ n ].size(); j++ ){ - Node v = d_var_contains[ n ][j]; + for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ + Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; for( int k=0; k<(int)patterns[v].size(); k++ ){ if( patterns[v][k]==n ){ patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 ); @@ -194,7 +142,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& if( trOption==TR_MAKE_NEW ){ //static int trNew = 0; //static int trOld = 0; - //Trigger* t = d_tr_trie.getTrigger( trNodes ); + //Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes ); //if( t ){ // trOld++; //}else{ @@ -204,7 +152,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& // std::cout << "Trigger new old = " << trNew << " " << trOld << std::endl; //} }else{ - Trigger* t = d_tr_trie.getTrigger( trNodes ); + Trigger* t = qe->getRRTriggerDatabase()->getTrigger( trNodes ); if( t ){ if( trOption==TR_GET_OLD ){ //just return old trigger @@ -215,7 +163,7 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } } Trigger* t = new Trigger( qe, f, trNodes, matchOption, smartTriggers ); - d_tr_trie.addTrigger( trNodes, t ); + qe->getRRTriggerDatabase()->addTrigger( trNodes, t ); return t; } Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, int matchOption, bool keepAll, int trOption, bool smartTriggers ){ @@ -264,32 +212,6 @@ bool Trigger::isSimpleTrigger( Node n ){ } } -/** filter all nodes that have instances */ -void Trigger::filterInstances( std::vector< Node >& nodes ){ - std::vector< bool > active; - active.resize( nodes.size(), true ); - for( int i=0; i<(int)nodes.size(); i++ ){ - for( int j=i+1; j<(int)nodes.size(); j++ ){ - if( active[i] && active[j] ){ - int result = isInstanceOf( nodes[i], nodes[j] ); - if( result==1 ){ - active[j] = false; - }else if( result==-1 ){ - active[i] = false; - } - } - } - } - std::vector< Node > temp; - for( int i=0; i<(int)nodes.size(); i++ ){ - if( active[i] ){ - temp.push_back( nodes[i] ); - } - } - nodes.clear(); - nodes.insert( nodes.begin(), temp.begin(), temp.end() ); -} - bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){ if( patMap.find( n )==patMap.end() ){ @@ -359,7 +281,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto collectPatTerms( qe, f, n, patTerms2, TS_ALL, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); - filterInstances( temp ); + qe->getTermDatabase()->filterInstances( temp ); if( temp.size()!=patTerms2.size() ){ Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl; Debug("trigger-filter-instance") << "Old: "; @@ -392,91 +314,6 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } -/** is n1 an instance of n2 or vice versa? */ -int Trigger::isInstanceOf( Node n1, Node n2 ){ - if( n1==n2 ){ - return 1; - }else if( n1.getKind()==n2.getKind() ){ - if( n1.getKind()==APPLY_UF ){ - if( n1.getOperator()==n2.getOperator() ){ - int result = 0; - for( int i=0; i<(int)n1.getNumChildren(); i++ ){ - if( n1[i]!=n2[i] ){ - int cResult = isInstanceOf( n1[i], n2[i] ); - if( cResult==0 ){ - return 0; - }else if( cResult!=result ){ - if( result!=0 ){ - return 0; - }else{ - result = cResult; - } - } - } - } - return result; - } - } - return 0; - }else if( n2.getKind()==INST_CONSTANT ){ - computeVarContains( n1 ); - //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ - // return 1; - //} - if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){ - return 1; - } - }else if( n1.getKind()==INST_CONSTANT ){ - computeVarContains( n2 ); - //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ - // return -1; - //} - if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){ - return 1; - } - } - return 0; -} - -bool Trigger::isVariableSubsume( Node n1, Node n2 ){ - if( n1==n2 ){ - return true; - }else{ - //std::cout << "is variable subsume ? " << n1 << " " << n2 << std::endl; - computeVarContains( n1 ); - computeVarContains( n2 ); - for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){ - if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){ - //std::cout << "no" << std::endl; - return false; - } - } - //std::cout << "yes" << std::endl; - return true; - } -} - -void Trigger::getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ){ - for( int i=0; i<(int)pats.size(); i++ ){ - computeVarContains( pats[i] ); - varContains[ pats[i] ].clear(); - for( int j=0; j<(int)d_var_contains[pats[i]].size(); j++ ){ - if( d_var_contains[pats[i]][j].getAttribute(InstConstantAttribute())==f ){ - varContains[ pats[i] ].push_back( d_var_contains[pats[i]][j] ); - } - } - } -} - -void Trigger::getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ){ - computeVarContains( n ); - for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ - if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){ - varContains.push_back( d_var_contains[n][j] ); - } - } -} - bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ){ if( n.getKind()==PLUS ){ Assert( coeffs.empty() ); @@ -519,3 +356,31 @@ bool Trigger::getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coef } return false; } + + + +Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){ + if( nodes.empty() ){ + return d_tr; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )!=d_children.end() ){ + return d_children[n]->getTrigger2( nodes ); + }else{ + return NULL; + } + } +} +void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){ + if( nodes.empty() ){ + d_tr = t; + }else{ + Node n = nodes.back(); + nodes.pop_back(); + if( d_children.find( n )==d_children.end() ){ + d_children[n] = new TriggerTrie; + } + d_children[n]->addTrigger2( nodes, t ); + } +} diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h index 99e7bf3d3..7be5d1507 100644 --- a/src/theory/rewriterules/rr_trigger.h +++ b/src/theory/rewriterules/rr_trigger.h @@ -25,13 +25,6 @@ namespace rrinst { //a collect of nodes representing a trigger class Trigger { -public: - static int trCount; -private: - /** computation of variable contains */ - static std::map< Node, std::vector< Node > > d_var_contains; - static void computeVarContains( Node n ); - static void computeVarContains2( Node n, Node parent ); private: /** the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -39,32 +32,6 @@ private: Node d_f; /** match generators */ PatsMatcher * d_mg; -private: - /** a trie of triggers */ - class TrTrie - { - private: - Trigger* getTrigger2( std::vector< Node >& nodes ); - void addTrigger2( std::vector< Node >& nodes, Trigger* t ); - public: - TrTrie() : d_tr( NULL ){} - Trigger* d_tr; - std::map< Node, TrTrie* > d_children; - Trigger* getTrigger( std::vector< Node >& nodes ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return getTrigger2( temp ); - } - void addTrigger( std::vector< Node >& nodes, Trigger* t ){ - std::vector< Node > temp; - temp.insert( temp.begin(), nodes.begin(), nodes.end() ); - std::sort( temp.begin(), temp.end() ); - return addTrigger2( temp, t ); - } - }; - /** all triggers will be stored in this trie */ - static TrTrie d_tr_trie; private: /** trigger constructor */ Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes, int matchOption = 0, bool smartTriggers = false ); @@ -138,15 +105,6 @@ public: } static bool isUsableTrigger( std::vector< Node >& nodes, Node f ); static bool isSimpleTrigger( Node n ); - /** filter all nodes that have instances */ - static void filterInstances( std::vector< Node >& nodes ); - /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - static int isInstanceOf( Node n1, Node n2 ); - /** variables subsume, return true if n1 contains all free variables in n2 */ - static bool isVariableSubsume( Node n1, Node n2 ); - /** get var contains */ - static void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); - static void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); /** get pattern arithmetic */ static bool getPatternArithmetic( Node f, Node n, std::map< Node, Node >& coeffs ); @@ -165,6 +123,31 @@ inline std::ostream& operator<<(std::ostream& out, const Trigger & tr) { return out; } +/** a trie of triggers */ +class TriggerTrie +{ +private: + Trigger* getTrigger2( std::vector< Node >& nodes ); + void addTrigger2( std::vector< Node >& nodes, Trigger* t ); +public: + TriggerTrie() : d_tr( NULL ){} + Trigger* d_tr; + std::map< Node, TriggerTrie* > d_children; + Trigger* getTrigger( std::vector< Node >& nodes ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return getTrigger2( temp ); + } + void addTrigger( std::vector< Node >& nodes, Trigger* t ){ + std::vector< Node > temp; + temp.insert( temp.begin(), nodes.begin(), nodes.end() ); + std::sort( temp.begin(), temp.end() ); + return addTrigger2( temp, t ); + } +}; + + }/* CVC4::theory::rrinst namespace */ }/* CVC4::theory namespace */ -- 2.30.2