From d8da3b13bc9df7750723cf3da38edc8cb6f67d3d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 16 Nov 2014 16:38:50 +0100 Subject: [PATCH] Add term db mode. Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches. Minor cleanup. --- src/theory/datatypes/theory_datatypes.cpp | 1 + .../quantifiers/inst_strategy_e_matching.cpp | 2 +- src/theory/quantifiers/modes.h | 7 + src/theory/quantifiers/options | 4 + src/theory/quantifiers/options_handlers.h | 24 +++ src/theory/quantifiers/quant_util.cpp | 1 + .../quantifiers/quantifiers_rewriter.cpp | 144 +++++++++++++----- src/theory/quantifiers/quantifiers_rewriter.h | 5 +- src/theory/quantifiers/term_database.cpp | 76 ++++----- src/theory/theory_engine.h | 5 + 10 files changed, 189 insertions(+), 80 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a05c7010b..453f8eb7f 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1110,6 +1110,7 @@ void TheoryDatatypes::computeCareGraph(){ TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES); Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl; EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); + Trace("dt-cg") << "...eq status is " << eqStatus << std::endl; if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ somePairIsDisequal = true; break; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 02536eb99..8a0ec3c09 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -173,7 +173,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) if( gen ){ generateTriggers( f, effort, e, status ); if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){ - Trace("no-trigger") << "Could not find trigger for " << f << std::endl; + Trace("trigger-warn") << "Could not find trigger for " << f << std::endl; } } diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 80dbb783e..5e692ace1 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -132,6 +132,13 @@ typedef enum { CEGQI_FAIR_NONE, } CegqiFairMode; +typedef enum { + /** consider all terms in master equality engine */ + TERM_DB_ALL, + /** consider only relevant terms */ + TERM_DB_RELEVANT, +} TermDbMode; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 97a43a96d..f4f1bcd86 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -29,6 +29,8 @@ option varElimQuant /--disable-var-elim-quant bool :default true option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers +option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true + split variables occurring as conditions of ITE in quantifiers option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true disable simple ite lifting for quantified formulas @@ -57,6 +59,8 @@ option macrosQuant --macros-quant bool :default false option foPropQuant --fo-prop-quant bool :default false perform first-order propagation on quantifiers +option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h" + which ground terms to consider for instantiation # Whether to use smart triggers option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e00879303..08fcf319d 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -188,6 +188,16 @@ none \n\ + Do not enforce fairness. \n\ \n\ "; +static const std::string termDbModeHelp = "\ +Modes for term database, supported by --term-db-mode:\n\ +\n\ +all \n\ ++ Consider all terms in the system.\n\ +\n\ +relevant \n\ ++ Consider only terms connected to current assertions. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { @@ -380,6 +390,20 @@ inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optar } } +inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "all" ) { + return TERM_DB_ALL; + } else if(optarg == "relevant") { + return TERM_DB_RELEVANT; + } else if(optarg == "help") { + puts(termDbModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --term-db-mode: `") + + optarg + "'. Try --term-db-mode help."); + } +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b39d7fff6..62a87bb99 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -241,6 +241,7 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int } void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { + Assert( n.getKind()!=IMPLIES && n.getKind()!=XOR ); newHasPol = hasPol; newPol = pol; if( n.getKind()==NOT ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 0d338f283..0ed175393 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -131,7 +131,7 @@ bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){ if( std::find( args.begin(), args.end(), n )!=args.end() ){ return true; }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ + for( unsigned i=0; i& args, Node n ){ } } +bool QuantifiersRewriter::hasArg1( Node a, Node n ) { + if( n==a ){ + return true; + }else{ + for( unsigned i=0; i processed; setNestedQuantifiers2( n, q, processed ); @@ -335,43 +348,88 @@ Node QuantifiersRewriter::computeNNF( Node body ){ } } -Node QuantifiersRewriter::computeSimpleIteLift( Node body ) { - if( body.getKind()==EQUAL ){ - for( size_t i=0; i<2; i++ ){ - if( body[i].getKind()==ITE ){ - Node no = i==0 ? body[1] : body[0]; - bool doRewrite = false; - std::vector< Node > children; - children.push_back( body[i][0] ); - for( size_t j=1; j<=2; j++ ){ - //check if it rewrites to a constant - Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); - nn = Rewriter::rewrite( nn ); - children.push_back( nn ); - if( nn.isConst() ){ - doRewrite = true; +Node QuantifiersRewriter::computeProcessIte( Node body, bool hasPol, bool pol ) { + if( body.getType().isBoolean() ){ + if( body.getKind()==EQUAL && options::simpleIteLiftQuant() ){ + for( size_t i=0; i<2; i++ ){ + if( body[i].getKind()==ITE ){ + Node no = i==0 ? body[1] : body[0]; + bool doRewrite = false; + std::vector< Node > children; + children.push_back( body[i][0] ); + for( size_t j=1; j<=2; j++ ){ + //check if it rewrites to a constant + Node nn = NodeManager::currentNM()->mkNode( EQUAL, no, body[i][j] ); + nn = Rewriter::rewrite( nn ); + children.push_back( nn ); + if( nn.isConst() ){ + doRewrite = true; + } + } + if( doRewrite ){ + return NodeManager::currentNM()->mkNode( ITE, children ); } } - if( doRewrite ){ - return NodeManager::currentNM()->mkNode( ITE, children ); + } + }else if( body.getKind()==ITE && hasPol && options::iteCondVarSplitQuant() ){ + for( unsigned r=0; r<2; r++ ){ + //check if there is a variable elimination + Node b = r==0 ? body[0] : body[0].negate(); + QuantPhaseReq qpr( b ); + std::vector< Node > vars; + std::vector< Node > subs; + Trace("ite-var-split-quant") << "phase req " << body[0] << " #: " << qpr.d_phase_reqs.size() << std::endl; + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ + Trace("ite-var-split-quant") << "phase req " << it->first << " -> " << it->second << std::endl; + if( it->second ){ + if( it->first.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + if( it->first[i].getKind()==BOUND_VARIABLE ){ + unsigned j = i==0 ? 1 : 0; + if( !hasArg1( it->first[i], it->first[j] ) ){ + vars.push_back( it->first[i] ); + subs.push_back( it->first[j] ); + break; + } + } + } + } + } + } + if( !vars.empty() ){ + //bool cpol = (r==1); + Node pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ); + //pos = pos.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + //pos = Rewriter::rewrite( pos ); + Node neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] ); + //Trace("ite-var-split-quant") << "Split ITE " << body << " into : " << std::endl; + //Trace("ite-var-split-quant") << " " << pos << std::endl; + //Trace("ite-var-split-quant") << " " << neg << std::endl; + return NodeManager::currentNM()->mkNode( AND, pos, neg ); } } } - }else if( body.getKind()!=APPLY_UF && body.getType()==NodeManager::currentNM()->booleanType() ){ - bool changed = false; - std::vector< Node > children; - for( size_t i=0; imkNode( body.getKind(), children ); + if( body.getKind()!=EQUAL && body.getKind()!=APPLY_UF ){ + bool changed = false; + std::vector< Node > children; + for( size_t i=0; imkNode( body.getKind(), children ); + } } } return body; } + + Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl; QuantPhaseReq qpr( body ); @@ -385,9 +443,7 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& int j = i==0 ? 1 : 0; std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), it->first[i] ); if( ita!=args.end() ){ - std::vector< Node > temp; - temp.push_back( it->first[i] ); - if( !hasArg( temp, it->first[j] ) ){ + if( !hasArg1( it->first[i], it->first[j] ) ){ vars.push_back( it->first[i] ); subs.push_back( it->first[j] ); args.erase( ita ); @@ -607,18 +663,22 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b }else{ return body; } - }else if( body.getKind()==ITE || body.getKind()==XOR || body.getKind()==IFF ){ - return body; }else{ Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; std::vector< Node > newChildren; for( int i=0; i<(int)body.getNumChildren(); i++ ){ - bool newPol = body.getKind()==NOT ? !pol : pol; - Node n = computePrenex( body[i], args, newPol ); - newChildren.push_back( n ); - if( n!=body[i] ){ - childrenChanged = true; + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); + if( newHasPol ){ + Node n = computePrenex( body[i], args, newPol ); + newChildren.push_back( n ); + if( n!=body[i] ){ + childrenChanged = true; + } + }else{ + newChildren.push_back( body[i] ); } } if( childrenChanged ){ @@ -959,8 +1019,8 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption return options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_NNF ){ return options::nnfQuant(); - }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ - return options::simpleIteLiftQuant(); + }else if( computeOption==COMPUTE_PROCESS_ITE ){ + return options::iteCondVarSplitQuant() || options::simpleIteLiftQuant(); }else if( computeOption==COMPUTE_PRENEX ){ return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ @@ -997,8 +1057,8 @@ Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOp return computeAggressiveMiniscoping( args, n, isNested ); }else if( computeOption==COMPUTE_NNF ){ n = computeNNF( n ); - }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){ - n = computeSimpleIteLift( n ); + }else if( computeOption==COMPUTE_PROCESS_ITE ){ + n = computeProcessIte( n, true, true ); }else if( computeOption==COMPUTE_PRENEX ){ n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 901a47f79..badf97c46 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -42,6 +42,7 @@ private: static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl ); static bool hasArg( std::vector< Node >& args, Node n ); + static bool hasArg1( Node a, Node n ); static void setNestedQuantifiers( Node n, Node q ); static void setNestedQuantifiers2( Node n, Node q, std::vector< Node >& processed ); static Node computeClause( Node n ); @@ -51,7 +52,7 @@ private: static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested = false ); static Node computeNNF( Node body ); - static Node computeSimpleIteLift( Node body ); + static Node computeProcessIte( Node body, bool hasPol, bool pol ); static Node computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); @@ -62,7 +63,7 @@ private: COMPUTE_MINISCOPING, COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, - COMPUTE_SIMPLE_ITE_LIFT, + COMPUTE_PROCESS_ITE, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 4979a3dfd..9e7d14b9a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -316,10 +316,16 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return false; } -bool TermDb::hasTermCurrent( Node n ) { +bool TermDb::hasTermCurrent( Node n ) { //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); - //return d_has_map.find( n )!=d_has_map.end(); - return true; + if( options::termDbMode()==TERM_DB_ALL ){ + return true; + }else if( options::termDbMode()==TERM_DB_RELEVANT ){ + return d_has_map.find( n )!=d_has_map.end(); + }else{ + Assert( false ); + return false; + } } void TermDb::setHasTerm( Node n ) { @@ -348,44 +354,44 @@ void TermDb::reset( Theory::Effort effort ){ d_func_map_eqc_trie.clear(); //compute has map - /* - d_has_map.clear(); - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ - TNode r = (*eqcs_i); - bool addedFirst = false; - Node first; - //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); - while( !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - if( first.isNull() ){ - first = n; - }else{ - if( !addedFirst ){ - addedFirst = true; - setHasTerm( first ); + if( options::termDbMode()==TERM_DB_RELEVANT ){ + d_has_map.clear(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + TNode r = (*eqcs_i); + bool addedFirst = false; + Node first; + //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( first.isNull() ){ + first = n; + }else{ + if( !addedFirst ){ + addedFirst = true; + setHasTerm( first ); + } + setHasTerm( n ); } - setHasTerm( n ); + ++eqc_i; } - ++eqc_i; + ++eqcs_i; } - ++eqcs_i; - } - for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { - Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId]; - if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) { - context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - Trace("ajr-temp") << "Set has term " << (*it).assertion << std::endl; - setHasTerm( (*it).assertion ); + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId]; + if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) { + context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + Trace("ajr-temp") << "Set has term " << (*it).assertion << std::endl; + setHasTerm( (*it).assertion ); + } } } } - */ - - + + //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ d_op_nonred_count[ it->first ] = 0; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e589e8f87..136c0409f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -83,6 +83,10 @@ namespace theory { class EqualityEngine; }/* CVC4::theory::eq namespace */ + namespace quantifiers { + class TermDb; + } + class EntailmentCheckParameters; class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ @@ -101,6 +105,7 @@ class TheoryEngine { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; + friend class theory::quantifiers::TermDb; /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; -- 2.30.2