diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 88 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 4 |
5 files changed, 69 insertions, 51 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d25e516fe..dabaa2188 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -185,51 +185,55 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ + RewriteStatus status = REWRITE_DONE; + Node ret = in; //get the arguments std::vector< Node > args; for( int i=0; i<(int)in[0].getNumChildren(); i++ ){ args.push_back( in[0][i] ); } - //get the body - Node body = in[1]; - if( in.getKind()==EXISTS ){ - body = body.getKind()==NOT ? body[0] : body.notNode(); - } //get the instantiation pattern list Node ipl; if( in.getNumChildren()==3 ){ ipl = in[2]; } - bool isNested = in.hasAttribute(NestedQuantAttribute()); - //compute miniscoping first - Node n = body;//computeNNF( body ); TODO: compute NNF here (current bad idea since arithmetic rewrites equalities) - if( body!=n ){ - Notice() << "NNF " << body << " -> " << n << std::endl; - } - n = computeMiniscoping( args, n, ipl, isNested ); - if( in.getKind()==kind::EXISTS ){ - n = n.getKind()==NOT ? n[0] : n.notNode(); + //get the body + if( in.getKind()==EXISTS ){ + std::vector< Node > children; + children.push_back( in[0] ); + children.push_back( in[1].negate() ); + if( in.getNumChildren()==3 ){ + children.push_back( in[2] ); + } + ret = NodeManager::currentNM()->mkNode( FORALL, children ); + ret = ret.negate(); + status = REWRITE_AGAIN_FULL; + }else{ + bool isNested = in.hasAttribute(NestedQuantAttribute()); + for( int op=0; op<COMPUTE_LAST; op++ ){ + if( doOperation( in, isNested, op ) ){ + ret = computeOperation( in, op ); + if( ret!=in ){ + status = REWRITE_AGAIN_FULL; + break; + } + } + } } - //compute other rewrite options for each produced quantifier - n = rewriteQuants( n, isNested, true ); //print if changed - if( in!=n ){ + if( in!=ret ){ if( in.hasAttribute(NestedQuantAttribute()) ){ - setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) ); + setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) ); } - Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; - Trace("quantifiers-rewrite") << " to " << std::endl; - Trace("quantifiers-rewrite") << n << std::endl; if( in.hasAttribute(InstConstantAttribute()) ){ InstConstantAttribute ica; - n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) ); + ret.setAttribute(ica,in.getAttribute(InstConstantAttribute()) ); } - - // This is required if substitute in computePrenex() is used. - return RewriteResponse(REWRITE_AGAIN_FULL, n ); - }else{ - return RewriteResponse(REWRITE_DONE, n ); + Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; + Trace("quantifiers-rewrite") << " to " << std::endl; + Trace("quantifiers-rewrite") << ret << std::endl; } + return RewriteResponse( status, ret ); } return RewriteResponse(REWRITE_DONE, in); } @@ -542,7 +546,10 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ if( f.getNumChildren()==3 ){ ipl = f[2]; } - if( computeOption==COMPUTE_NNF ){ + if( computeOption==COMPUTE_MINISCOPING ){ + //return directly + return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) ); + }else if( computeOption==COMPUTE_NNF ){ n = computeNNF( n ); }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){ n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX ); @@ -663,25 +670,25 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } return mkForAll( args, body, ipl ); } - -Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested, bool duringRewrite ){ +/* +Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested ){ if( n.getKind()==FORALL ){ - return rewriteQuant( n, isNested, duringRewrite ); + return rewriteQuant( n, isNested ); }else if( isLiteral( n ) ){ return n; }else{ NodeBuilder<> tt(n.getKind()); for( int i=0; i<(int)n.getNumChildren(); i++ ){ - tt << rewriteQuants( n[i], isNested, duringRewrite ); + tt << rewriteQuants( n[i], isNested ); } return tt.constructNode(); } } -Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrite ){ +Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested ){ Node prev = n; for( int op=0; op<COMPUTE_LAST; op++ ){ - if( doOperation( n, isNested, op, duringRewrite ) ){ + if( doOperation( n, isNested, op ) ){ Node prev2 = n; n = computeOperation( n, op ); if( prev2!=n ){ @@ -695,9 +702,10 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit return n; }else{ //rewrite again until fix point is reached - return rewriteQuant( n, isNested, duringRewrite ); + return rewriteQuant( n, isNested ); } } +*/ bool QuantifiersRewriter::doMiniscopingNoFreeVar(){ return options::miniscopeQuantFreeVar(); @@ -715,17 +723,19 @@ bool QuantifiersRewriter::doMiniscopingAnd(){ } } -bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption, bool duringRewrite ){ - if( computeOption==COMPUTE_NNF ){ +bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){ + if( computeOption==COMPUTE_MINISCOPING ){ + return true; + }else if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) }else if( computeOption==COMPUTE_PRE_SKOLEM ){ - return false;//options::preSkolemQuant() && !duringRewrite; + return false;//options::preSkolemQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant(); }else if( computeOption==COMPUTE_CNF ){ - return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind(); + return false;//return options::cnfQuant() ; }else{ return false; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 636e00774..00301c610 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -51,7 +51,8 @@ private: static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq ); private: enum{ - COMPUTE_NNF = 0, + COMPUTE_MINISCOPING = 0, + COMPUTE_NNF, COMPUTE_PRE_SKOLEM, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, @@ -69,10 +70,10 @@ private: /** options */ static bool doMiniscopingNoFreeVar(); static bool doMiniscopingAnd(); - static bool doOperation( Node f, bool isNested, int computeOption, bool duringRewrite = true ); + static bool doOperation( Node f, bool isNested, int computeOption ); public: - static Node rewriteQuants( Node n, bool isNested = false, bool duringRewrite = true ); - static Node rewriteQuant( Node n, bool isNested = false, bool duringRewrite = true ); + //static Node rewriteQuants( Node n, bool isNested = false ); + //static Node rewriteQuant( Node n, bool isNested = false ); };/* class QuantifiersRewriter */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 591270ab0..b55e8abdf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" -#include "theory/uf/theory_uf_instantiator.h" +#include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/options.h" @@ -80,7 +80,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ d_op_map[op].push_back( n ); added.insert( n ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ + for( size_t i=0; i<n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant ); if( options::efficientEMatching() ){ EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher(); @@ -100,10 +100,9 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } if( options::eagerInstQuant() ){ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF ); int addedLemmas = 0; - for( int i=0; i<(int)ith->d_op_triggers[op].size(); i++ ){ - addedLemmas += ith->d_op_triggers[op][i]->addTerm( n ); + for( size_t i=0; i<d_op_triggers[op].size(); i++ ){ + addedLemmas += d_op_triggers[op][i]->addTerm( n ); } //Message() << "Terms, added lemmas: " << addedLemmas << std::endl; d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel() ); @@ -468,3 +467,9 @@ void TermDb::getVarContainsNode( Node f, Node n, std::vector< Node >& varContain } } } + +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 5060ac1a7..2bae5a043 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -205,6 +205,8 @@ private: void computeVarContains2( Node n, Node parent ); /** var contains */ std::map< TNode, std::vector< TNode > > d_var_contains; + /** triggers for each operator */ + std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; public: /** compute var contains */ void computeVarContains( Node n ); @@ -214,6 +216,8 @@ public: void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); + /** register trigger (for eager quantifier instantiation) */ + void registerTrigger( inst::Trigger* tr, Node op ); };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index ae08fe863..67b2e6bd8 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -67,10 +67,8 @@ d_quantEngine( qe ), d_f( f ){ } //Notice() << "Trigger : " << (*this) << " for " << f << std::endl; if( options::eagerInstQuant() ){ - Theory* th_uf = qe->getTheoryEngine()->theoryOf( theory::THEORY_UF ); - uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator(); for( int i=0; i<(int)d_nodes.size(); i++ ){ - ith->registerTrigger( this, d_nodes[i].getOperator() ); + qe->getTermDatabase()->registerTrigger( this, d_nodes[i].getOperator() ); } } } |