From 38d149261763e5f2f65abb21c2b647f2befa7807 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 20 Feb 2014 09:45:46 -0600 Subject: [PATCH] Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge. --- src/Makefile.am | 15 - src/smt/smt_engine.cpp | 161 +--- src/theory/arith/theory_arith_private.cpp | 4 +- src/theory/quantifiers/bounded_integers.cpp | 1 + .../quantifiers/candidate_generator.cpp | 1 + src/theory/quantifiers/first_order_model.cpp | 1 + .../quantifiers/first_order_reasoning.cpp | 9 +- .../quantifiers/first_order_reasoning.h | 4 + src/theory/quantifiers/full_model_check.cpp | 1 + src/theory/quantifiers/inst_gen.cpp | 1 + .../quantifiers/inst_match_generator.cpp | 1 + .../quantifiers/inst_strategy_e_matching.cpp | 13 +- .../quantifiers/instantiation_engine.cpp | 30 +- src/theory/quantifiers/kinds | 21 + src/theory/quantifiers/model_builder.cpp | 5 +- src/theory/quantifiers/options | 4 + src/theory/quantifiers/options_handlers.h | 3 + src/theory/quantifiers/qinterval_builder.cpp | 2 + .../quantifiers/quant_conflict_find.cpp | 893 +++++++++++------- src/theory/quantifiers/quant_conflict_find.h | 41 +- .../quantifiers/quantifiers_rewriter.cpp | 290 +++++- src/theory/quantifiers/quantifiers_rewriter.h | 10 +- src/theory/quantifiers/relevant_domain.cpp | 3 + src/theory/quantifiers/rewrite_engine.cpp | 300 ++++-- src/theory/quantifiers/rewrite_engine.h | 13 +- src/theory/quantifiers/symmetry_breaking.cpp | 1 + src/theory/quantifiers/term_database.cpp | 50 +- src/theory/quantifiers/term_database.h | 21 +- .../theory_quantifiers_type_rules.h | 86 ++ src/theory/quantifiers_engine.cpp | 61 +- src/theory/quantifiers_engine.h | 32 +- src/theory/rewriterules/kinds | 20 - .../rewriterules/theory_rewriterules.cpp | 570 +---------- src/theory/rewriterules/theory_rewriterules.h | 226 ----- .../theory_rewriterules_type_rules.h | 82 -- src/theory/theory_engine.cpp | 4 +- test/regress/regress0/push-pop/bug326.smt2 | 2 +- .../regress/regress0/rewriterules/Makefile.am | 11 +- .../rewriterules/simulate_rewriting.smt2 | 2 +- 39 files changed, 1310 insertions(+), 1685 deletions(-) diff --git a/src/Makefile.am b/src/Makefile.am index 64e3eb932..450bf063e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -307,23 +307,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/quant_conflict_find.h \ theory/quantifiers/quant_conflict_find.cpp \ theory/quantifiers/options_handlers.h \ - theory/rewriterules/theory_rewriterules_rules.h \ - theory/rewriterules/theory_rewriterules_rules.cpp \ theory/rewriterules/theory_rewriterules.h \ theory/rewriterules/theory_rewriterules.cpp \ - theory/rewriterules/theory_rewriterules_rewriter.h \ - theory/rewriterules/theory_rewriterules_type_rules.h \ - theory/rewriterules/theory_rewriterules_preprocess.h \ - theory/rewriterules/theory_rewriterules_params.h \ - theory/rewriterules/rr_inst_match.h \ - theory/rewriterules/rr_inst_match_impl.h \ - theory/rewriterules/rr_inst_match.cpp \ - theory/rewriterules/rr_trigger.h \ - theory/rewriterules/rr_trigger.cpp \ - theory/rewriterules/rr_candidate_generator.h \ - theory/rewriterules/rr_candidate_generator.cpp \ - theory/rewriterules/efficient_e_matching.h \ - theory/rewriterules/efficient_e_matching.cpp \ theory/arith/theory_arith_type_rules.h \ theory/arith/type_enumerator.h \ theory/arith/arithvar.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 16528e404..8c8b5f840 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -80,8 +80,10 @@ #include "util/sort_inference.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/macros.h" -#include "theory/datatypes/options.h" #include "theory/quantifiers/first_order_reasoning.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/options.h" +#include "theory/datatypes/options.h" #include "theory/strings/theory_strings_preprocess.h" using namespace std; @@ -595,11 +597,6 @@ public: return applySubstitutions(n).toExpr(); } - /** - * Pre-skolemize quantifiers. - */ - Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector& fvs); - /** * Substitute away all AbstractValues in a node. */ @@ -1188,7 +1185,7 @@ void SmtEngine::setLogicInternal() throw() { //instantiate only on last call if( options::fmfInstEngine() ){ Trace("smt") << "setting inst when mode to LAST_CALL" << endl; - options::instWhenMode.set( INST_WHEN_LAST_CALL ); + options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } if ( options::fmfBoundInt() ){ @@ -1776,120 +1773,6 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map ContainsQuantAttribute; - -// check if the given node contains a universal quantifier -static bool containsQuantifiers(Node n) { - if( n.hasAttribute(ContainsQuantAttribute()) ){ - return n.getAttribute(ContainsQuantAttribute())==1; - } else if(n.getKind() == kind::FORALL) { - return true; - } else { - bool cq = false; - for( unsigned i = 0; i < n.getNumChildren(); ++i ){ - if( containsQuantifiers(n[i]) ){ - cq = true; - break; - } - } - ContainsQuantAttribute cqa; - n.setAttribute(cqa, cq ? 1 : 0); - return cq; - } -} - -Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){ - Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; - if( n.getKind()==kind::NOT ){ - Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs ); - return nn.negate(); - }else if( n.getKind()==kind::FORALL ){ - if( polarity ){ - vector< Node > children; - children.push_back( n[0] ); - //add children to current scope - vector< Node > fvss; - fvss.insert( fvss.begin(), fvs.begin(), fvs.end() ); - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - fvss.push_back( n[0][i] ); - } - //process body - children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) ); - if( n.getNumChildren()==3 ){ - children.push_back( n[2] ); - } - //return processed quantifier - return NodeManager::currentNM()->mkNode( kind::FORALL, children ); - }else{ - //process body - Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs ); - //now, substitute skolems for the variables - vector< TypeNode > argTypes; - for( int i=0; i<(int)fvs.size(); i++ ){ - argTypes.push_back( fvs[i].getType() ); - } - //calculate the variables and substitution - vector< Node > vars; - vector< Node > subs; - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - vars.push_back( n[0][i] ); - } - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - //make the new function symbol - if( argTypes.empty() ){ - Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" ); - subs.push_back( s ); - }else{ - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() ); - Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" ); - //DOTHIS: set attribute on op, marking that it should not be selected as trigger - vector< Node > funcArgs; - funcArgs.push_back( op ); - funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); - subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) ); - } - } - //apply substitution - nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - return nn; - } - }else{ - //check if it contains a quantifier as a subterm - //if so, we will write this node - if( containsQuantifiers( n ) ){ - if( n.getType().isBoolean() ){ - if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ - Node nn; - //must remove structure - if( n.getKind()==kind::ITE ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ - nn = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), - NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); - } - return preSkolemizeQuantifiers( nn, polarity, fvs ); - }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ - vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); - } - return NodeManager::currentNM()->mkNode( n.getKind(), children ); - }else{ - //must pull ite's - } - } - } - return n; - } -} - void SmtEnginePrivate::removeITEs() { d_smt.finalOptionsAreSet(); @@ -3156,13 +3039,25 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-strings-pp", d_assertionsToPreprocess); } if( d_smt.d_logic.isQuantified() ){ + //remove rewrite rules + for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) { + if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){ + Node prev = d_assertionsToPreprocess[i]; + Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl; + d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) ); + Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl; + Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; + } + } + dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); if( options::preSkolemQuant() ){ //apply pre-skolemization to existential quantifiers for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { Node prev = d_assertionsToPreprocess[i]; + Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl; vector< Node > fvs; - d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) ); + d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvs ) ); if( prev!=d_assertionsToPreprocess[i] ){ Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; @@ -3174,14 +3069,14 @@ void SmtEnginePrivate::processAssertions() { //quantifiers macro expansion bool success; do{ - QuantifierMacros qm; + quantifiers::QuantifierMacros qm; success = qm.simplify( d_assertionsToPreprocess, true ); }while( success ); } Trace("fo-rsn-enable") << std::endl; if( options::foPropQuant() ){ - FirstOrderPropagation fop; + quantifiers::FirstOrderPropagation fop; fop.simplify( d_assertionsToPreprocess ); } } @@ -3977,28 +3872,26 @@ void SmtEngine::checkModel(bool hardFailure) { Debug("boolean-terms") << "++ got " << n << endl; Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl; - if(Theory::theoryOf(n) != THEORY_REWRITERULES) { + //AJR : FIXME need to ignore quantifiers too? + if( n.getKind() != kind::REWRITE_RULE ){ // In case it's a quantifier (or contains one), look up its value before // simplifying, or the quantifier might be irreparably altered. n = m->getValue(n); - } - - // Simplify the result. - n = d_private->simplify(n); - Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; - - TheoryId thy = Theory::theoryOf(n); - if(thy == THEORY_REWRITERULES) { + } else { // Note this "skip" is done here, rather than above. This is // because (1) the quantifier could in principle simplify to false, // which should be reported, and (2) checking for the quantifier // above, before simplification, doesn't catch buried quantifiers // anyway (those not at the top-level). - Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion" + Notice() << "SmtEngine::checkModel(): -- skipping quantifiers/rewrite-rules assertion" << endl; continue; } + // Simplify the result. + n = d_private->simplify(n); + Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; + // Replace the already-known ITEs (this is important for ground ITEs under quantifiers). n = d_private->d_iteRemover.replace(n); Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d920fc8ca..37dba5e92 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -70,6 +70,8 @@ #include "theory/theory_model.h" #include "theory/arith/options.h" +#include "theory/quantifiers/options.h" + #include "theory/quantifiers/bounded_integers.h" @@ -1597,7 +1599,7 @@ void TheoryArithPrivate::preRegisterTerm(TNode n) { } ConstraintP c = d_constraintDatabase.lookup(n); Assert(c != NullConstraint); - + Debug("arith::preregister") << "setup constraint" << c << endl; Assert(!c->canBePropagated()); c->setPreregistered(); diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index e59874429..bec8ea350 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/term_database.h" using namespace CVC4; using namespace std; diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 1e89bb1ea..1b34bc118 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 8c00c5af4..f3203da4b 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/qinterval_builder.h" +#include "theory/quantifiers/options.h" #define USE_INDEX_ORDERING diff --git a/src/theory/quantifiers/first_order_reasoning.cpp b/src/theory/quantifiers/first_order_reasoning.cpp index a696af3c2..1c87dad7b 100644 --- a/src/theory/quantifiers/first_order_reasoning.cpp +++ b/src/theory/quantifiers/first_order_reasoning.cpp @@ -19,10 +19,11 @@ #include "theory/rewriter.h" using namespace CVC4; -using namespace CVC4::kind; using namespace std; - -namespace CVC4 { +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; +using namespace CVC4::context; void FirstOrderPropagation::collectLits( Node n, std::vector & lits ){ @@ -167,5 +168,3 @@ Node FirstOrderPropagation::simplify( Node n ) { return NodeManager::currentNM()->mkNode( n.getKind(), children ); } } - -} diff --git a/src/theory/quantifiers/first_order_reasoning.h b/src/theory/quantifiers/first_order_reasoning.h index 6bc5c21c1..92898eff5 100644 --- a/src/theory/quantifiers/first_order_reasoning.h +++ b/src/theory/quantifiers/first_order_reasoning.h @@ -25,6 +25,8 @@ #include "expr/type_node.h" namespace CVC4 { +namespace theory { +namespace quantifiers { class FirstOrderPropagation { private: @@ -40,6 +42,8 @@ public: void simplify( std::vector< Node >& assertions ); }; +} +} } #endif diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index d542e878c..6c889781d 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 27b87e6a4..aaa65e630 100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/model_builder.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" //#define CHILD_USE_CONSIDER diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index e1d301c09..13186c7cc 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/candidate_generator.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index dee8192c1..f60e01a7d 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -97,22 +97,11 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){ //extend to literal matching d_quantEngine->getPhaseReqTerms( f, nodes ); //check match option - int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0; + int matchOption = 0; d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW, options::smartTriggers() ) ); } } -/* -InstStrategyUserPatterns::Statistics::Statistics(): - d_instantiations("InstStrategyUserPatterns::Instantiations", 0) -{ - StatisticsRegistry::registerStat(&d_instantiations); -} - -InstStrategyUserPatterns::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_instantiations); -} -*/ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){ //reset triggers diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 99dc29bf8..e5705882a 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -209,7 +209,7 @@ void InstantiationEngine::check( Theory::Effort e ){ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); //it is not active if we have found the skolemized negation is unsat - if( n.hasAttribute(QRewriteRuleAttribute()) ){ + if( TermDb::isRewriteRule( n ) ){ d_quant_active[n] = false; }else if( options::cbqi() && hasAddedCbqiLemma( n ) ){ Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); @@ -292,19 +292,23 @@ void InstantiationEngine::check( Theory::Effort e ){ } void InstantiationEngine::registerQuantifier( Node f ){ - //Notice() << "do cbqi " << f << " ? " << std::endl; - Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); - if( !doCbqi( f ) ){ - d_quantEngine->addTermToDatabase( ceBody, true ); - } + if( !TermDb::isRewriteRule( f ) ){ + //Notice() << "do cbqi " << f << " ? " << std::endl; + if( options::cbqi() ){ + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); + if( !doCbqi( f ) ){ + d_quantEngine->addTermToDatabase( ceBody, true ); + } + } - //take into account user patterns - if( f.getNumChildren()==3 ){ - Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f ); - //add patterns - for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ - //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; - addUserPattern( f, subsPat[i] ); + //take into account user patterns + if( f.getNumChildren()==3 ){ + Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f ); + //add patterns + for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ + //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; + addUserPattern( f, subsPat[i] ); + } } } } diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index ab0e9d934..795bc1ab4 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -48,4 +48,25 @@ typerule BOUND_VAR_LIST ::CVC4::theory::quantifiers::QuantifierBoundVarListTypeR typerule INST_PATTERN ::CVC4::theory::quantifiers::QuantifierInstPatternTypeRule typerule INST_PATTERN_LIST ::CVC4::theory::quantifiers::QuantifierInstPatternListTypeRule +# for rewrite rules +# types... +sort RRHB_TYPE \ + Cardinality::INTEGERS \ + not-well-founded \ + "head and body of the rule type" + +# operators... + +# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE +operator REWRITE_RULE 3 "general rewrite rule" +#HEAD/BODY/TRIGGER +operator RR_REWRITE 2:3 "actual rewrite rule" +operator RR_REDUCTION 2:3 "actual reduction rule" +operator RR_DEDUCTION 2:3 "actual deduction rule" + +typerule REWRITE_RULE ::CVC4::theory::quantifiers::RewriteRuleTypeRule +typerule RR_REWRITE ::CVC4::theory::quantifiers::RRRewriteTypeRule +typerule RR_REDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule +typerule RR_DEDUCTION ::CVC4::theory::quantifiers::RRRedDedTypeRule + endtheory diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 502a34176..50a0084fc 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/inst_gen.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; @@ -39,7 +40,7 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe } bool QModelBuilder::isQuantifierActive( Node f ) { - return !f.hasAttribute(QRewriteRuleAttribute()); + return !TermDb::isRewriteRule( f ); } @@ -381,7 +382,7 @@ QModelBuilderIG::Statistics::~Statistics(){ } bool QModelBuilderIG::isQuantifierActive( Node f ){ - return !f.hasAttribute(QRewriteRuleAttribute()) && + return !TermDb::isRewriteRule( f ) && ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 2967c77c8..7ee416c4e 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -125,5 +125,9 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" when to invoke conflict find mechanism for quantifiers +option quantRewriteRules --rewrite-rules bool :default false + use rewrite rules module +option rrOneInstPerRound --rr-one-inst-per-round bool :default false + add one instance of rewrite rule per round endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 9892009a3..e9c754d4a 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -131,6 +131,9 @@ conflict \n\ partial \n\ + Apply QCF algorithm to instantiate heuristically as well. \n\ \n\ +partial \n\ ++ Apply QCF to instantiate heuristically as well. \n\ +\n\ mc \n\ + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ \n\ diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp index ece519d1c..285834e96 100755 --- a/src/theory/quantifiers/qinterval_builder.cpp +++ b/src/theory/quantifiers/qinterval_builder.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/qinterval_builder.h" +#include "theory/quantifiers/term_database.h" + using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ae5a35a00..79948a063 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -18,6 +18,8 @@ #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" #include "theory/theory_engine.h" +#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" using namespace CVC4; using namespace CVC4::kind; @@ -107,27 +109,16 @@ void QuantInfo::initialize( Node q, Node qn ) { std::vector< int > bvars; d_mg->determineVariableOrder( this, bvars ); } - - //must also contain all variables? - if( d_isPartial ){ - for( unsigned i=0; isetInvalid(); - break; - } - } - } } - Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? ( isPartial() ? "PARTIAL " : "VALID " ) : "INVALID" ) << " : " << q << std::endl; + Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; } void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) { Trace("qcf-qregister-debug2") << "Register : " << n << std::endl; if( n.getKind()==FORALL ){ registerNode( n[1], hasPol, pol, true ); - }else{ - if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){ + }else{ + if( !MatchGen::isHandledBoolConnective( n ) ){ if( n.hasBoundVar() ){ //literals if( n.getKind()==EQUAL ){ @@ -136,11 +127,9 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) } }else if( MatchGen::isHandledUfTerm( n ) ){ flatten( n, beneathQuant ); - }else if( n.getKind()==ITE ){ - if( !n[1].getType().isBoolean() ){ - for( unsigned i=1; i<=2; i++ ){ - flatten( n[i], beneathQuant ); - } + }else if( n.getKind()==ITE ){ + for( unsigned i=1; i<=2; i++ ){ + flatten( n[i], beneathQuant ); } } } @@ -220,6 +209,8 @@ void QuantInfo::reset_round( QuantConflictFind * p ) { for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){ it->second->reset_round( p ); } + //now, reset for matching + d_mg->reset( p, false, this ); } int QuantInfo::getCurrentRepVar( int v ) { @@ -249,6 +240,24 @@ TNode QuantInfo::getCurrentValue( TNode n ) { } } +TNode QuantInfo::getCurrentExpValue( TNode n ) { + int v = getVarNum( n ); + if( v==-1 ){ + return n; + }else{ + if( d_match[v].isNull() ){ + return n; + }else{ + Assert( getVarNum( d_match[v] )!=v ); + if( d_match_term[v].isNull() ){ + return getCurrentValue( d_match[v] ); + }else{ + return d_match_term[v]; + } + } + } +} + bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) { //check disequalities std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v ); @@ -453,109 +462,113 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { return false; } -bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned ) { +bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) { //assign values for variables that were unassigned (usually not necessary, but handles corner cases) - Trace("qcf-check") << std::endl; - std::vector< int > unassigned[2]; - std::vector< TypeNode > unassigned_tn[2]; - for( int i=0; i unassigned[2]; + std::vector< TypeNode > unassigned_tn[2]; + for( int i=0; i eqc_count; - bool doFail = false; - do { - if( doFail ){ - Trace("qcf-check-unassign") << "Failure, try again..." << std::endl; - } - bool invalidMatch = false; - while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){ - invalidMatch = false; - if( !doFail && index==(int)eqc_count.size() ){ - //check if it has now been assigned - if( r==0 ){ - if( !isConstrainedVar( unassigned[r][index] ) ){ - eqc_count.push_back( -1 ); - }else{ - d_var_mg[ unassigned[r][index] ]->reset( p, true, this ); - eqc_count.push_back( 0 ); - } + if( !d_unassigned.empty() ){ + Trace("qcf-check") << "Assign to unassigned..." << std::endl; + do { + if( doFail ){ + Trace("qcf-check-unassign") << "Failure, try again..." << std::endl; + } + bool invalidMatch = false; + while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){ + invalidMatch = false; + if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){ + //check if it has now been assigned + if( d_una_indexreset( p, true, this ); + d_una_eqc_count.push_back( 0 ); } }else{ - if( r==0 ){ - if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){ - Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl; - index++; - }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, this ) ){ - Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl; - index++; + d_una_eqc_count.push_back( 0 ); + } + }else{ + bool failed = false; + if( !doFail ){ + if( d_una_indexgetNextMatch( p, this ) ){ + Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl; + d_una_index++; }else{ - Trace("qcf-check-unassign") << "Failed match with mg at " << index << std::endl; - do{ - if( !doFail ){ - eqc_count.pop_back(); - }else{ - doFail = false; - } - index--; - }while( index>=0 && eqc_count[index]==-1 ); + failed = true; + Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl; } }else{ - Assert( doFail || index==(int)eqc_count.size()-1 ); - if( !doFail && eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){ - int currIndex = eqc_count[index]; - eqc_count[index]++; - Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl; - if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){ - //if( currIndex==0 ){ - // Assert( p->areEqual( p->d_model_basis[unassigned_tn[r][index]], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ); - // d_match_term[unassigned[r][index]] = p->d_model_basis[unassigned_tn[r][index]]; - //}else{ - d_match_term[unassigned[r][index]] = TNode::null(); - //} - Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl; - index++; + Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 ); + if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){ + int currIndex = d_una_eqc_count[d_una_index]; + d_una_eqc_count[d_una_index]++; + Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl; + if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){ + d_match_term[d_unassigned[d_una_index]] = TNode::null(); + Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl; + d_una_index++; }else{ - Trace("qcf-check-unassign") << "Failed match " << index << std::endl; + Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl; invalidMatch = true; } }else{ - Trace("qcf-check-unassign") << "No more matches " << index << std::endl; - if( !doFail ){ - eqc_count.pop_back(); - }else{ - doFail = false; - } - index--; + failed = true; + Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl; } } } + if( doFail || failed ){ + do{ + if( !doFail ){ + d_una_eqc_count.pop_back(); + }else{ + doFail = false; + } + d_una_index--; + }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 ); + } } - success = index>=0; - if( success ){ - doFail = true; - Trace("qcf-check-unassign") << " Try: " << std::endl; - for( unsigned i=0; i " << d_match[ui] << std::endl; - } + } + success = d_una_index>=0; + if( success ){ + doFail = true; + Trace("qcf-check-unassign") << " Try: " << std::endl; + for( unsigned i=0; i " << d_match[ui] << std::endl; } } - }while( success && isMatchSpurious( p ) ); - } + } + }while( success && isMatchSpurious( p ) ); } if( success ){ return true; @@ -568,6 +581,28 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign } } +void QuantInfo::getMatch( std::vector< Node >& terms ){ + for( unsigned i=0; igetCurrentValue( qi->d_match[i] ); + int repVar = getCurrentRepVar( i ); + Node cv; + //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar ); + if( !d_match_term[repVar].isNull() ){ + cv = d_match_term[repVar]; + }else{ + cv = d_match[repVar]; + } + Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl; + terms.push_back( cv ); + } +} + +void QuantInfo::revertMatch( std::vector< int >& assigned ) { + for( unsigned i=0; i "; @@ -583,7 +618,10 @@ void QuantInfo::debugPrintMatch( const char * c ) { } Trace(c) << "}"; } - Trace(c) << std::endl; + if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){ + Trace(c) << ", EXP : " << d_match_term[i]; + } + Trace(c) << std::endl; } } @@ -614,9 +652,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ Trace("qcf-qregister-debug") << " is var #" << v << std::endl; d_qni_var_num[d_qni_size] = v; //qi->addFuncParent( v, f, j ); - if( nn.getKind()==BOUND_VARIABLE && !beneathQuant ){ - qi->d_has_var[nn] = true; - } }else{ Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl; d_qni_gterm[d_qni_size] = nn; @@ -655,7 +690,7 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ d_type_not = !d_type_not; } - if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE || d_n.getKind()==FORALL ){ + if( isHandledBoolConnective( d_n ) ){ //non-literals d_type = typ_formula; bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL; @@ -696,8 +731,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ if( d_n[i].hasBoundVar() ){ if( !qi->isVar( d_n[i] ) ){ Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl; - }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){ - qi->d_has_var[d_n[i]] = true; } Assert( qi->isVar( d_n[i] ) ); }else{ @@ -708,6 +741,8 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ }else if( isHandledUfTerm( d_n ) ){ Assert( qi->isVar( d_n ) ); d_type = typ_pred; + }else if( d_n.getKind()==BOUND_VARIABLE ){ + d_type = typ_bool_var; }else{ Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl; } @@ -737,9 +772,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ Trace("qcf-qregister-debug") << std::endl; //Assert( d_children.size()==d_children_order.size() ); - if( !isValid() && options::qcfMode()>=QCF_PARTIAL ){ - qi->d_isPartial = true; - } } void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) { @@ -829,6 +861,7 @@ void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars void MatchGen::reset_round( QuantConflictFind * p ) { + d_wasSet = false; for( unsigned i=0; id_true : p->d_false ) ){ d_child_counter = 0; } + }else if( d_type==typ_bool_var ){ + //get current value of the variable + TNode n = qi->getCurrentValue( d_n ); + int vn = qi->getCurrentRepVar( qi->getVarNum( n ) ); + if( vn==-1 ){ + //evaluate the value, see if it is compatible + int e = p->evaluate( n ); + if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){ + d_child_counter = 0; + } + }else{ + //unassigned, set match to true/false + d_qni_bound[0] = vn; + qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false ); + d_child_counter = 0; + } + if( d_child_counter==0 ){ + d_qn.push_back( NULL ); + } }else if( d_type==typ_var ){ Assert( isHandledUfTerm( d_n ) ); Node f = getOperator( p, d_n ); @@ -904,6 +960,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { } bool success; if( vn[0]==-1 && vn[1]==-1 ){ + //Trace("qcf-explain") << " reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl; Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl; //just compare values if( d_tgt ){ @@ -931,6 +988,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { success = addc!=-1; //if successful and non-redundant, store that we need to cleanup this if( addc==1 ){ + //Trace("qcf-explain") << " reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl; for( unsigned i=0; i<2; i++ ){ if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){ d_qni_bound[vn[i]] = vn[i]; @@ -962,6 +1020,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { } } d_binding = false; + d_wasSet = true; Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl; } @@ -974,9 +1033,10 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_child_counter = -1; return true; }else{ + d_wasSet = false; return false; } - }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred ){ + }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){ bool success = false; bool terminate = false; do { @@ -1020,8 +1080,8 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { Debug("qcf-match-debug") << " failed." << std::endl; success = false; }else{ - Debug("qcf-match-debug") << " decrement..." << std::endl; --d_binding_it; + Debug("qcf-match-debug") << " decrement..." << std::endl; } }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) ); doReset = false; @@ -1056,6 +1116,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl; std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first ); int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1; + //Trace("qcf-explain") << " cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl; qi->addConstraint( p, it->first, it->second, vn, d_tgt, true ); } } @@ -1085,6 +1146,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { */ } Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl; + d_wasSet = success; return success; }else if( d_type==typ_formula || d_type==typ_ite_var ){ bool success = false; @@ -1096,7 +1158,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { }else{ while( !success && d_child_counter>=0 ){ //transition system based on d_child_counter - if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){ + if( d_n.getKind()==OR || d_n.getKind()==AND ){ if( (d_n.getKind()==AND)==d_tgt ){ //all children must match simultaneously if( getChild( d_child_counter )->getNextMatch( p, qi ) ){ @@ -1181,6 +1243,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { } } } + d_wasSet = success; Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl; return success; } @@ -1189,6 +1252,84 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { return false; } +bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) { + if( d_type==typ_eq ){ + Node n[2]; + for( unsigned i=0; i<2; i++ ){ + Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl; + n[i] = getExplanationTerm( p, qi, d_n[i], exp ); + } + Node eq = n[0].eqNode( n[1] ); + if( !d_tgt_orig ){ + eq = eq.negate(); + } + exp.push_back( eq ); + Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl; + return true; + }else if( d_type==typ_pred ){ + Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl; + Node n = getExplanationTerm( p, qi, d_n, exp ); + if( !d_tgt_orig ){ + n = n.negate(); + } + exp.push_back( n ); + Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl; + return true; + }else if( d_type==typ_formula ){ + Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl; + if( d_n.getKind()==OR || d_n.getKind()==AND ){ + if( (d_n.getKind()==AND)==d_tgt ){ + for( unsigned i=0; igetExplanation( p, qi, exp ) ){ + return false; + } + } + }else{ + return getChild( d_child_counter )->getExplanation( p, qi, exp ); + } + }else if( d_n.getKind()==IFF ){ + for( unsigned i=0; i<2; i++ ){ + if( !getChild( i )->getExplanation( p, qi, exp ) ){ + return false; + } + } + }else if( d_n.getKind()==ITE ){ + for( unsigned i=0; i<3; i++ ){ + bool isActive = ( ( i==0 && d_child_counter!=5 ) || + ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) || + ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) ); + if( isActive ){ + if( !getChild( i )->getExplanation( p, qi, exp ) ){ + return false; + } + } + } + }else{ + return false; + } + return true; + }else{ + return false; + } +} + +Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) { + Node v = qi->getCurrentExpValue( t ); + if( isHandledUfTerm( t ) ){ + for( unsigned i=0; isecond.d_children.empty() ); TNode t = d_qni[d_qni.size()-1]->second.d_children.begin()->first; Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl; + qi->d_match_term[d_qni_var_num[0]] = t; //set the match terms for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){ Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl; - if( it->second<(int)qi->d_q[0].getNumChildren() && it->first>0 ){ //if it is an actual variable, we are interested in knowing the actual term + //if( it->second<(int)qi->d_q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term + if( it->first>0 ){ Assert( !qi->d_match[ it->second ].isNull() ); Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) ); qi->d_match_term[it->second] = t[it->first-1]; } + //} } } } @@ -1322,7 +1466,7 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) { case typ_formula: Trace(c) << "formula";break; case typ_var: Trace(c) << "var";break; case typ_ite_var: Trace(c) << "ite_var";break; - case typ_top: Trace(c) << "top";break; + case typ_bool_var: Trace(c) << "bool_var";break; } }else{ switch( typ ){ @@ -1333,7 +1477,7 @@ void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) { case typ_formula: Debug(c) << "formula";break; case typ_var: Debug(c) << "var";break; case typ_ite_var: Debug(c) << "ite_var";break; - case typ_top: Debug(c) << "top";break; + case typ_bool_var: Debug(c) << "bool_var";break; } } } @@ -1343,18 +1487,37 @@ void MatchGen::setInvalid() { d_children.clear(); } +bool MatchGen::isHandledBoolConnective( TNode n ) { + return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT ); +} + bool MatchGen::isHandledUfTerm( TNode n ) { - return n.getKind()==APPLY_UF;// || n.getKind()==GEQ; + return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT || + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ; } Node MatchGen::getOperator( QuantConflictFind * p, Node n ) { if( isHandledUfTerm( n ) ){ - return n.getOperator(); + return p->getQuantifiersEngine()->getTermDatabase()->getOperator( n ); }else{ return Node::null(); } } +bool MatchGen::isHandled( TNode n ) { + if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){ + if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){ + return false; + } + for( unsigned i=0; iq[0].getNumChildren() ){ - Trace("qcf-qregister") << " with additional constraints : " << std::endl; - for( unsigned j=q[0].getNumChildren(); jq[0].getNumChildren() ){ + Trace("qcf-qregister") << " with additional constraints : " << std::endl; + for( unsigned j=q[0].getNumChildren(); j::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){ - // it->first->d_active.set( true ); - //} + if( !TermDb::isRewriteRule( q ) ){ + Trace("qcf-proc") << "QCF : assertQuantifier : "; + debugPrintQuant("qcf-proc", q); + Trace("qcf-proc") << std::endl; + d_qassert.push_back( q ); + //set the eqRegistries that this depends on to true + //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){ + // it->first->d_active.set( true ); + //} + } } eq::EqualityEngine * QuantConflictFind::getEqualityEngine() { @@ -1518,7 +1699,7 @@ bool QuantConflictFind::areEqual( Node n1, Node n2 ) { return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 ); } bool QuantConflictFind::areDisequal( Node n1, Node n2 ) { - return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false ); + return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false ); } Node QuantConflictFind::getRepresentative( Node n ) { if( getEqualityEngine()->hasTerm( n ) ){ @@ -1677,6 +1858,10 @@ void QuantConflictFind::assertDisequal( Node a, Node b ) { //-------------------------------------------------- check function +void QuantConflictFind::reset_round( Theory::Effort level ) { + d_needs_computeRelEqr = true; +} + /** check */ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-check") << "QCF : check : " << level << std::endl; @@ -1695,7 +1880,6 @@ void QuantConflictFind::check( Theory::Effort level ) { clSet = double(clock())/double(CLOCKS_PER_SEC); Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl; } - Trace("qcf-check") << "Compute relevant equalities..." << std::endl; computeRelevantEqr(); //determine order for quantified formulas @@ -1728,17 +1912,8 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-debug") << std::endl; debugPrint("qcf-debug"); Trace("qcf-debug") << std::endl; - } - short end_e; - if( options::qcfMode()==QCF_CONFLICT_ONLY ){ - end_e = effort_conflict; - }else if( options::qcfMode()==QCF_PROP_EQ ){ - end_e = effort_prop_eq; - }else if( options::qcfMode()==QCF_PARTIAL ){ - end_e = effort_partial; - }else{ - end_e = effort_mc; - } + } + short end_e = getMaxQcfEffort(); for( short e = effort_conflict; e<=end_e; e++ ){ d_effort = e; Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl; @@ -1748,79 +1923,106 @@ void QuantConflictFind::check( Theory::Effort level ) { Assert( d_qinfo.find( q )!=d_qinfo.end() ); if( qi->d_mg->isValid() ){ - if( qi->isPartial()==(e==effort_partial) ){ - Trace("qcf-check") << "Check quantified formula "; - debugPrintQuant("qcf-check", q); - Trace("qcf-check") << " : " << q << "..." << std::endl; - - Trace("qcf-check-debug") << "Reset round..." << std::endl; - qi->reset_round( this ); - //try to make a matches making the body false - Trace("qcf-check-debug") << "Reset..." << std::endl; - qi->d_mg->reset( this, false, qi ); - Trace("qcf-check-debug") << "Get next match..." << std::endl; - while( qi->d_mg->getNextMatch( this, qi ) ){ - - Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl; - qi->debugPrintMatch("qcf-check"); - Trace("qcf-check") << std::endl; - - if( !qi->isMatchSpurious( this ) ){ - std::vector< int > assigned; - if( qi->completeMatch( this, assigned ) ){ - std::vector< Node > terms; - for( unsigned i=0; igetCurrentValue( qi->d_match[i] ); - int repVar = qi->getCurrentRepVar( i ); - Node cv; - //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar ); - if( !qi->d_match_term[repVar].isNull() ){ - cv = qi->d_match_term[repVar]; - }else{ - cv = qi->d_match[repVar]; + Trace("qcf-check") << "Check quantified formula "; + debugPrintQuant("qcf-check", q); + Trace("qcf-check") << " : " << q << "..." << std::endl; + + Trace("qcf-check-debug") << "Reset round..." << std::endl; + qi->reset_round( this ); + //try to make a matches making the body false + Trace("qcf-check-debug") << "Get next match..." << std::endl; + while( qi->d_mg->getNextMatch( this, qi ) ){ + Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-check"); + Trace("qcf-check") << std::endl; + std::vector< int > assigned; + if( !qi->isMatchSpurious( this ) ){ + if( qi->completeMatch( this, assigned ) ){ + /* + if( options::qcfExp() && d_effort==effort_conflict ){ + std::vector< Node > exp; + if( qi->d_mg->getExplanation( this, qi, exp ) ){ + Trace("qcf-check-exp") << "Base explanation is : " << std::endl; + for( unsigned c=0; c " << cv << ", from " << qi->d_match[i] << std::endl; - terms.push_back( cv ); - } - if( Debug.isOn("qcf-check-inst") ){ - //if( e==effort_conflict ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( evaluate( inst )!=1 ); - Assert( evaluate( inst )==-1 || e>effort_conflict ); - //} - } - if( d_quantEngine->addInstantiation( q, terms ) ){ - Trace("qcf-check") << " ... Added instantiation" << std::endl; - ++addedLemmas; - if( e==effort_conflict ){ - d_quant_order.insert( d_quant_order.begin(), q ); - d_conflict.set( true ); - ++(d_statistics.d_conflict_inst); - break; - }else if( e==effort_prop_eq ){ - ++(d_statistics.d_prop_inst); - }else if( e==effort_partial ){ - ++(d_statistics.d_partial_inst); + std::vector< TNode > c_exp; + eq::EqualityEngine* ee = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine() ; + for( unsigned c=0; careDisequal( lit[0], lit[1], true ) ){ + exit( 98 ); + }else if( pol && !ee->areEqual( lit[0], lit[1] ) ){ + exit( 99 ); + } + ee->explainEquality( lit[0], lit[1], pol, c_exp ); + }else{ + if( !ee->areEqual( lit, pol ? d_true : d_false ) ){ + exit( pol ? 96 : 97 ); + } + ee->explainPredicate( lit, pol, c_exp ); + } + } + std::vector< Node > c_lem; + Trace("qcf-check-exp") << "Actual explanation is : " << std::endl; + for( unsigned c=0; cmkNode( OR, c_lem ); + Trace("qcf-conflict") << "QCF conflict : " << conf << std::endl; + d_quantEngine->addLemma( conf, false ); + d_conflict.set( true ); + ++(d_statistics.d_conflict_inst); + ++addedLemmas; + break; } - //clean up assigned - for( unsigned i=0; id_match[ assigned[i] ] = TNode::null(); + } + */ + std::vector< Node > terms; + qi->getMatch( terms ); + if( Debug.isOn("qcf-check-inst") ){ + //if( e==effort_conflict ){ + Node inst = d_quantEngine->getInstantiation( q, terms ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( evaluate( inst )!=1 ); + Assert( evaluate( inst )==-1 || e>effort_conflict ); + //} + } + if( d_quantEngine->addInstantiation( q, terms ) ){ + Trace("qcf-check") << " ... Added instantiation" << std::endl; + ++addedLemmas; + if( e==effort_conflict ){ + d_quant_order.insert( d_quant_order.begin(), q ); + d_conflict.set( true ); + ++(d_statistics.d_conflict_inst); + break; + }else if( e==effort_prop_eq ){ + ++(d_statistics.d_prop_inst); } }else{ - Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; + Trace("qcf-check") << " ... Failed to add instantiation" << std::endl; + //Assert( false ); } + //clean up assigned + qi->revertMatch( assigned ); }else{ - Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl; + Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } - } - if( d_conflict ){ - break; - } + }else{ + Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl; + } + } + if( d_conflict ){ + break; } } } @@ -1845,7 +2047,7 @@ void QuantConflictFind::check( Theory::Effort level ) { bool QuantConflictFind::needsCheck( Theory::Effort level ) { d_performCheck = false; - if( !d_conflict ){ + if( options::quantConflictFind() && !d_conflict ){ if( level==Theory::EFFORT_LAST_CALL ){ d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL; }else if( level==Theory::EFFORT_FULL ){ @@ -1858,131 +2060,133 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) { } void QuantConflictFind::computeRelevantEqr() { - d_uf_terms.clear(); - d_eqc_uf_terms.clear(); - d_eqcs.clear(); - d_model_basis.clear(); - d_arg_reps.clear(); - //double clSet = 0; - //if( Trace.isOn("qcf-opt") ){ - // clSet = double(clock())/double(CLOCKS_PER_SEC); - //} - - //long nTermst = 0; - //long nTerms = 0; - //long nEqc = 0; + if( d_needs_computeRelEqr ){ + d_needs_computeRelEqr = false; + Trace("qcf-check") << "Compute relevant equalities..." << std::endl; + d_uf_terms.clear(); + d_eqc_uf_terms.clear(); + d_eqcs.clear(); + d_model_basis.clear(); + d_arg_reps.clear(); + //double clSet = 0; + //if( Trace.isOn("qcf-opt") ){ + // clSet = double(clock())/double(CLOCKS_PER_SEC); + //} - //which nodes are irrelevant for disequality matches - std::map< TNode, bool > irrelevant_dnode; - //now, store matches - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); - while( !eqcs_i.isFinished() ){ - //nEqc++; - Node r = (*eqcs_i); - TypeNode rtn = r.getType(); - if( options::qcfMode()==QCF_MC ){ - std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn ); - if( itt==d_eqcs.end() ){ - Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn ); - if( !getEqualityEngine()->hasTerm( mb ) ){ - Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl; - Assert( false ); - } - Node mbr = getRepresentative( mb ); - if( mbr!=r ){ - d_eqcs[rtn].push_back( mbr ); + //long nTermst = 0; + //long nTerms = 0; + //long nEqc = 0; + + //which nodes are irrelevant for disequality matches + std::map< TNode, bool > irrelevant_dnode; + //now, store matches + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); + while( !eqcs_i.isFinished() ){ + //nEqc++; + Node r = (*eqcs_i); + TypeNode rtn = r.getType(); + if( options::qcfMode()==QCF_MC ){ + std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn ); + if( itt==d_eqcs.end() ){ + Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn ); + if( !getEqualityEngine()->hasTerm( mb ) ){ + Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl; + Assert( false ); + } + Node mbr = getRepresentative( mb ); + if( mbr!=r ){ + d_eqcs[rtn].push_back( mbr ); + } + d_eqcs[rtn].push_back( r ); + d_model_basis[rtn] = mb; + }else{ + itt->second.push_back( r ); } - d_eqcs[rtn].push_back( r ); - d_model_basis[rtn] = mb; }else{ - itt->second.push_back( r ); - } - }else{ - d_eqcs[rtn].push_back( r ); - } - /* - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); - while( !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - if( n.hasBoundVar() ){ - std::cout << "BAD TERM IN DB : " << n << std::endl; - exit( 199 ); - } - ++eqc_i; - } - */ + d_eqcs[rtn].push_back( r ); + } + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( n.hasBoundVar() ){ + std::cout << "BAD TERM IN DB : " << n << std::endl; + exit( 199 ); + } + ++eqc_i; + } - //if( r.getType().isInteger() ){ - // Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl; - //} - //EqcInfo * eqcir = getEqcInfo( r, false ); - //get relevant nodes that we are disequal from - /* - std::vector< Node > deqc; - if( eqcir ){ - for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){ - if( (*it).second ){ - //Node rd = (*it).first; - //if( rd!=getRepresentative( rd ) ){ - // std::cout << "Bad rep!" << std::endl; - // exit( 0 ); - //} - deqc.push_back( (*it).first ); + //if( r.getType().isInteger() ){ + // Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl; + //} + //EqcInfo * eqcir = getEqcInfo( r, false ); + //get relevant nodes that we are disequal from + /* + std::vector< Node > deqc; + if( eqcir ){ + for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){ + if( (*it).second ){ + //Node rd = (*it).first; + //if( rd!=getRepresentative( rd ) ){ + // std::cout << "Bad rep!" << std::endl; + // exit( 0 ); + //} + deqc.push_back( (*it).first ); + } } } - } - */ - //process disequalities - /* - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); - while( !eqc_i.isFinished() ){ - TNode n = (*eqc_i); - if( n.getKind()!=EQUAL ){ - nTermst++; - //node_to_rep[n] = r; - //if( n.getNumChildren()>0 ){ - // if( n.getKind()!=APPLY_UF ){ - // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl; - // } - //} - if( !n.hasBoundVar() ){ //temporary - - bool isRedundant; - std::map< TNode, std::vector< TNode > >::iterator it_na; - TNode fn; - if( MatchGen::isHandledUfTerm( n ) ){ - Node f = MatchGen::getOperator( this, n ); - computeArgReps( n ); - it_na = d_arg_reps.find( n ); - Assert( it_na!=d_arg_reps.end() ); - Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] ); - isRedundant = (nadd!=n); - d_uf_terms[f].addTerm( n, d_arg_reps[n] ); + */ + //process disequalities + /* + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); + while( !eqc_i.isFinished() ){ + TNode n = (*eqc_i); + if( n.getKind()!=EQUAL ){ + nTermst++; + //node_to_rep[n] = r; + //if( n.getNumChildren()>0 ){ + // if( n.getKind()!=APPLY_UF ){ + // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl; + // } + //} + if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){ //temporary + + bool isRedundant; + std::map< TNode, std::vector< TNode > >::iterator it_na; + TNode fn; + if( MatchGen::isHandledUfTerm( n ) ){ + Node f = MatchGen::getOperator( this, n ); + computeArgReps( n ); + it_na = d_arg_reps.find( n ); + Assert( it_na!=d_arg_reps.end() ); + Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] ); + isRedundant = (nadd!=n); + d_uf_terms[f].addTerm( n, d_arg_reps[n] ); + }else{ + isRedundant = false; + } + nTerms += isRedundant ? 0 : 1; }else{ - isRedundant = false; - } - nTerms += isRedundant ? 0 : 1; - }else{ - if( Debug.isOn("qcf-nground") ){ - Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl; - Assert( false ); + if( Debug.isOn("qcf-nground") ){ + Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl; + Assert( false ); + } } } + ++eqc_i; } - ++eqc_i; + */ + ++eqcs_i; + } + /* + if( Trace.isOn("qcf-opt") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("qcf-opt") << "Compute rel eqc : " << std::endl; + Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl; + Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl; + Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl; } */ - ++eqcs_i; } - /* - if( Trace.isOn("qcf-opt") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("qcf-opt") << "Compute rel eqc : " << std::endl; - Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl; - Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl; - Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl; - } - */ } void QuantConflictFind::computeArgReps( TNode n ) { @@ -2079,20 +2283,17 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo QuantConflictFind::Statistics::Statistics(): d_inst_rounds("QuantConflictFind::Inst_Rounds", 0), d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ), - d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), - d_partial_inst("QuantConflictFind::Instantiations_Partial", 0 ) + d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_conflict_inst); StatisticsRegistry::registerStat(&d_prop_inst); - StatisticsRegistry::registerStat(&d_partial_inst); } QuantConflictFind::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); StatisticsRegistry::unregisterStat(&d_conflict_inst); StatisticsRegistry::unregisterStat(&d_prop_inst); - StatisticsRegistry::unregisterStat(&d_partial_inst); } } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 944cfa584..090af8143 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -83,13 +83,15 @@ public: typ_formula, typ_var, typ_ite_var, - typ_top, + typ_bool_var, }; void debugPrintType( const char * c, short typ, bool isTrace = false ); public: MatchGen() : d_type( typ_invalid ){} MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false ); bool d_tgt; + bool d_tgt_orig; + bool d_wasSet; Node d_n; std::vector< MatchGen > d_children; short d_type; @@ -97,21 +99,32 @@ public: void reset_round( QuantConflictFind * p ); void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ); bool getNextMatch( QuantConflictFind * p, QuantInfo * qi ); + bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ); + Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ); bool isValid() { return d_type!=typ_invalid; } void setInvalid(); // is this term treated as UF application? + static bool isHandledBoolConnective( TNode n ); static bool isHandledUfTerm( TNode n ); static Node getOperator( QuantConflictFind * p, Node n ); + //can this node be handled by the algorithm + static bool isHandled( TNode n ); }; //info for quantifiers class QuantInfo { private: void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false ); - void flatten( Node n, bool beneathQuant ); + void flatten( Node n, bool beneathQuant ); +private: //for completing match + std::vector< int > d_unassigned; + std::vector< TypeNode > d_unassigned_tn; + int d_unassigned_nvar; + int d_una_index; + std::vector< int > d_una_eqc_count; public: - QuantInfo() : d_mg( NULL ), d_isPartial( false ) {} + QuantInfo() : d_mg( NULL ) {} std::vector< TNode > d_vars; std::map< TNode, int > d_var_num; std::map< TNode, bool > d_nbeneathQuant; @@ -120,6 +133,7 @@ public: bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); } int getNumVars() { return (int)d_vars.size(); } TNode getVar( int i ) { return d_vars[i]; } + MatchGen * d_mg; Node d_q; std::map< int, MatchGen * > d_var_mg; @@ -133,20 +147,18 @@ public: std::map< int, std::map< TNode, int > > d_curr_var_deq; int getCurrentRepVar( int v ); TNode getCurrentValue( TNode n ); + TNode getCurrentExpValue( TNode n ); bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false ); int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ); int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ); bool setMatch( QuantConflictFind * p, int v, TNode n ); bool isMatchSpurious( QuantConflictFind * p ); - bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned ); + bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false ); + void revertMatch( std::vector< int >& assigned ); void debugPrintMatch( const char * c ); - bool isConstrainedVar( int v ); -public: - // is partial - bool d_isPartial; - //the variables that this quantified formula has not beneath nested quantifiers - std::map< TNode, bool > d_has_var; - bool isPartial() { return d_isPartial; } + bool isConstrainedVar( int v ); +public: + void getMatch( std::vector< Node >& terms ); }; class QuantConflictFind : public QuantifiersModule @@ -218,6 +230,8 @@ public: effort_mc, }; short d_effort; + void setEffort( int e ) { d_effort = e; } + static short getMaxQcfEffort(); bool areMatchEqual( TNode n1, TNode n2 ); bool areMatchDisequal( TNode n1, TNode n2 ); public: @@ -233,11 +247,15 @@ public: void merge( Node a, Node b ); /** assert disequal */ void assertDisequal( Node a, Node b ); + /** reset round */ + void reset_round( Theory::Effort level ); /** check */ void check( Theory::Effort level ); /** needs check */ bool needsCheck( Theory::Effort level ); private: + bool d_needs_computeRelEqr; +public: void computeRelevantEqr(); private: void debugPrint( const char * c ); @@ -253,7 +271,6 @@ public: IntStat d_inst_rounds; IntStat d_conflict_inst; IntStat d_prop_inst; - IntStat d_partial_inst; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index ac847678d..db61b046f 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4; @@ -90,19 +91,29 @@ void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ } } -void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ){ +void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n ){ if( n.getKind()==BOUND_VARIABLE ){ - if( std::find( args.begin(), args.end(), n )!=args.end() && - std::find( activeArgs.begin(), activeArgs.end(), n )==activeArgs.end() ){ - activeArgs.push_back( n ); + if( std::find( args.begin(), args.end(), n )!=args.end() ){ + activeMap[ n ] = true; } }else{ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeArgs( args, activeArgs, n[i] ); + computeArgs( args, activeMap, n[i] ); } } } +void QuantifiersRewriter::computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ) { + std::map< Node, bool > activeMap; + computeArgs( args, activeMap, n ); + for( unsigned i=0; i& args, Node n ){ if( std::find( args.begin(), args.end(), n )!=args.end() ){ return true; @@ -135,7 +146,6 @@ void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< No } } - RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl; if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){ @@ -164,9 +174,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { } Node n = NodeManager::currentNM()->mkNode( in.getKind(), children ); if( in!=n ){ - if( in.hasAttribute(NestedQuantAttribute()) ){ - setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) ); - } + setAttributes( in, n ); Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl; Trace("quantifiers-pre-rewrite") << " to " << std::endl; Trace("quantifiers-pre-rewrite") << n << std::endl; @@ -178,8 +186,9 @@ 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 ){ + Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl; + Trace("quantifiers-rewrite-debug") << "Attributes : " << in.hasAttribute(NestedQuantAttribute()) << std::endl; + if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){ RewriteStatus status = REWRITE_DONE; Node ret = in; //get the arguments @@ -217,12 +226,13 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { } //print if changed if( in!=ret ){ - if( in.hasAttribute(NestedQuantAttribute()) ){ - setNestedQuantifiers( ret, in.getAttribute(NestedQuantAttribute()) ); - } + setAttributes( in, ret ); Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl; Trace("quantifiers-rewrite") << " to " << std::endl; Trace("quantifiers-rewrite") << ret << std::endl; + Trace("quantifiers-rewrite-debug") << "Attributes : " << ret.hasAttribute(NestedQuantAttribute()) << std::endl; + + } return RewriteResponse( status, ret ); } @@ -409,6 +419,15 @@ Node QuantifiersRewriter::computeClause( Node n ){ } } +void QuantifiersRewriter::setAttributes( Node in, Node n ) { + if( in.hasAttribute(NestedQuantAttribute()) ){ + setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) ); + } + //if( in.hasAttribute(QRewriteRuleAttribute()) ){ + // n.setAttribute(QRewriteRuleAttribute(), in.getAttribute(QRewriteRuleAttribute())); + //} +} + Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){ if( isLiteral( n ) ){ return n; @@ -432,7 +451,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui //compute the free variables Node nt = t; std::vector< Node > activeArgs; - computeArgs( args, activeArgs, nt ); + computeArgVec( args, activeArgs, nt ); std::vector< TypeNode > argTypes; for( int i=0; i<(int)activeArgs.size(); i++ ){ argTypes.push_back( activeArgs[i].getType() ); @@ -581,7 +600,7 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >& //get variables contained in the literal Node n = body[i]; std::vector lit_vars; - computeArgs( vars, lit_vars, n); + computeArgVec( vars, lit_vars, n); //collectVars( n, vars, lit_vars ); if (lit_vars.empty()) { lits.push_back(n); @@ -689,7 +708,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ //return directly - return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) ); + return computeMiniscoping( f, args, n, ipl, f.hasAttribute(NestedQuantAttribute()) ); }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) ); }else if( computeOption==COMPUTE_NNF ){ @@ -735,7 +754,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){ std::vector< Node > activeArgs; - computeArgs( args, activeArgs, body ); + computeArgVec( args, activeArgs, body ); if( activeArgs.empty() ){ return body; }else{ @@ -749,7 +768,7 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node i } } -Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested ){ +Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, Node ipl, bool isNested ){ //Notice() << "rewrite quant " << body << std::endl; if( body.getKind()==FORALL ){ //combine arguments @@ -763,21 +782,21 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo if( body.getKind()==NOT ){ //push not downwards if( body[0].getKind()==NOT ){ - return computeMiniscoping( args, body[0][0], ipl ); + return computeMiniscoping( f, args, body[0][0], ipl ); }else if( body[0].getKind()==AND ){ if( doMiniscopingNoFreeVar() ){ NodeBuilder<> t(kind::OR); for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ t << ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() ); } - return computeMiniscoping( args, t.constructNode(), ipl ); + return computeMiniscoping( f, args, t.constructNode(), ipl ); } }else if( body[0].getKind()==OR ){ if( doMiniscopingAnd() ){ NodeBuilder<> t(kind::AND); for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ Node trm = body[0][i].negate(); - t << computeMiniscoping( args, trm, ipl ); + t << computeMiniscoping( f, args, trm, ipl ); } return t.constructNode(); } @@ -787,7 +806,7 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo //break apart NodeBuilder<> t(kind::AND); for( int i=0; i<(int)body.getNumChildren(); i++ ){ - t << computeMiniscoping( args, body[i], ipl ); + t << computeMiniscoping( f, args, body[i], ipl ); } Node retVal = t; return retVal; @@ -815,7 +834,11 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } } } - return mkForAll( args, body, ipl ); + if( body==f[1] ){ + return f; + }else{ + return mkForAll( args, body, ipl ); + } } Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body, bool isNested ){ @@ -826,7 +849,7 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl; for( size_t i=0; i activeArgs; - computeArgs( args, activeArgs, body[i] ); + computeArgVec( args, activeArgs, body[i] ); for (unsigned j=0; j vars; + vars.reserve(r[0].getNumChildren()); + for( Node::const_iterator v = r[0].begin(); v != r[0].end(); ++v ){ + vars.push_back(*v); + }; + + // Body/Remove_term/Guards/Triggers + Node body = r[2][1]; + TNode new_terms = r[2][1]; + std::vector guards; + std::vector pattern; + Node true_node = NodeManager::currentNM()->mkConst(true); + // shortcut + TNode head = r[2][0]; + switch(rrkind){ + case kind::RR_REWRITE: + // Equality + pattern.push_back( head ); + if( head.getType().isBoolean() ){ + body = head.iffNode(body); + }else{ + body = head.eqNode(body); + } + break; + case kind::RR_REDUCTION: + case kind::RR_DEDUCTION: + // Add head to guards and pattern + switch(head.getKind()){ + case kind::AND: + for( unsigned i = 0; i= 3 ){ + for( unsigned i=0; i forallB(kind::FORALL); + forallB << r[0]; + Node gg = guards.size()==0 ? true_node : ( guards.size()==1 ? guards[0] : NodeManager::currentNM()->mkNode( AND, guards ) ); + gg = NodeManager::currentNM()->mkNode( OR, gg.negate(), body ); + gg = Rewriter::rewrite( gg ); + forallB << gg; + NodeBuilder<> patternB(kind::INST_PATTERN); + patternB.append(pattern); + NodeBuilder<> patternListB(kind::INST_PATTERN_LIST); + //the entire rewrite rule is the first pattern + if( options::quantRewriteRules() ){ + patternListB << NodeManager::currentNM()->mkNode( INST_PATTERN, r ); + } + patternListB << static_cast(patternB); + forallB << static_cast(patternListB); + Node rn = (Node) forallB; + + return rn; +} + +struct ContainsQuantAttributeId {}; +typedef expr::Attribute ContainsQuantAttribute; + +// check if the given node contains a universal quantifier +bool QuantifiersRewriter::containsQuantifiers(Node n) { + if( n.hasAttribute(ContainsQuantAttribute()) ){ + return n.getAttribute(ContainsQuantAttribute())==1; + } else if(n.getKind() == kind::FORALL) { + return true; + } else { + bool cq = false; + for( unsigned i = 0; i < n.getNumChildren(); ++i ){ + if( containsQuantifiers(n[i]) ){ + cq = true; + break; + } + } + ContainsQuantAttribute cqa; + n.setAttribute(cqa, cq ? 1 : 0); + return cq; + } +} + +Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){ + Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl; + if( n.getKind()==kind::NOT ){ + Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs ); + return nn.negate(); + }else if( n.getKind()==kind::FORALL ){ + if( polarity ){ + vector< Node > children; + children.push_back( n[0] ); + //add children to current scope + vector< Node > fvss; + fvss.insert( fvss.begin(), fvs.begin(), fvs.end() ); + for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ + fvss.push_back( n[0][i] ); + } + //process body + children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) ); + if( n.getNumChildren()==3 ){ + children.push_back( n[2] ); + } + //return processed quantifier + return NodeManager::currentNM()->mkNode( kind::FORALL, children ); + }else{ + //process body + Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs ); + //now, substitute skolems for the variables + vector< TypeNode > argTypes; + for( int i=0; i<(int)fvs.size(); i++ ){ + argTypes.push_back( fvs[i].getType() ); + } + //calculate the variables and substitution + vector< Node > vars; + vector< Node > subs; + for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ + vars.push_back( n[0][i] ); + } + for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ + //make the new function symbol + if( argTypes.empty() ){ + Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" ); + subs.push_back( s ); + }else{ + TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() ); + Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" ); + //DOTHIS: set attribute on op, marking that it should not be selected as trigger + vector< Node > funcArgs; + funcArgs.push_back( op ); + funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); + subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) ); + } + } + //apply substitution + nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + return nn; + } + }else{ + //check if it contains a quantifier as a subterm + //if so, we will write this node + if( containsQuantifiers( n ) ){ + if( n.getType().isBoolean() ){ + if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){ + Node nn; + //must remove structure + if( n.getKind()==kind::ITE ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); + }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + nn = NodeManager::currentNM()->mkNode( kind::AND, + NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), + NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); + }else if( n.getKind()==kind::IMPLIES ){ + nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); + } + return preSkolemizeQuantifiers( nn, polarity, fvs ); + }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){ + vector< Node > children; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + //must pull ite's + } + } + } + return n; + } +} diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index e97d84701..4cbdb0cd1 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -38,14 +38,16 @@ public: private: static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, Node ipl ); - static void computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); + static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n ); + static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ); static bool hasArg( std::vector< Node >& args, 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 ); + static void setAttributes( Node in, Node n ); private: static Node computeElimSymbols( Node body ); - static Node computeMiniscoping( std::vector< Node >& args, Node body, Node ipl, bool isNested = false ); + 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 ); @@ -78,6 +80,10 @@ private: static bool doMiniscopingNoFreeVar(); static bool doMiniscopingAnd(); static bool doOperation( Node f, bool isNested, int computeOption ); +public: + static Node rewriteRewriteRule( Node r ); + static bool containsQuantifiers(Node n); + static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector& fvs); public: //static Node rewriteQuants( Node n, bool isNested = false ); //static Node rewriteQuant( Node n, bool isNested = false ); diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 952f3409a..20ab4e55f 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -118,6 +118,7 @@ void RelevantDomain::compute(){ for( unsigned j=0; jaddTerm( n[j] ); + Trace("rel-dom-debug") << "...add ground term " << n[j] << " to rel dom " << op << "[" << j << "]" << std::endl; } } } @@ -188,6 +189,7 @@ void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { }else if( varCount==1 ){ int oCh = varCh==0 ? 1 : 0; bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] ); + Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << std::endl; //the negative occurrence adds the term to the domain if( !hasPol || !pol ){ rds[varCh]->addTerm( n[oCh], ng ); @@ -219,6 +221,7 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { rq->merge( rf ); } }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n ) ){ + Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl; //term to add rf->addTerm( n ); } diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 81de1e11d..59ba40ca7 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -21,6 +21,7 @@ #include "theory/quantifiers/options.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/theory_engine.h" +#include "theory/quantifiers/term_database.h" using namespace CVC4; using namespace std; @@ -37,14 +38,15 @@ struct PrioritySort { RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { - + d_true = NodeManager::currentNM()->mkConst( true ); } double RewriteEngine::getPriority( Node f ) { - Node rr = f.getAttribute(QRewriteRuleAttribute()); + Node rr = TermDb::getRewriteRule( f ); 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 ){ @@ -54,26 +56,31 @@ double RewriteEngine::getPriority( Node f ) { }else{ return 6.0; } + + //return deterministic ? 0.0 : 1.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; igetModel()->isModelSet() ){ + // d_quantEngine->getTheoryEngine()->getModelBuilder()->buildModel( d_quantEngine->getModel(), true ); + // } + //} + if( d_needsSort ){ + d_priority_order.clear(); + 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; iflushLemmas( &d_quantEngine->getOutputChannel() ); @@ -98,85 +106,185 @@ void RewriteEngine::check( Theory::Effort e ) { } } -int RewriteEngine::checkRewriteRule( Node f ) { - Trace("rewrite-engine-inst") << "Check " << f << ", priority = " << getPriority( f ) << "..." << std::endl; +int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { 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 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; iresetInstantiationRound(); - d_rr_triggers[f][i]->reset( Node::null() ); - bool success; - do - { - InstMatch m( f ); - 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); + Trace("rewrite-engine-inst") << "Check " << d_qinfo_n[f] << ", priority = " << getPriority( f ) << ", effort = " << e << "..." << std::endl; + QuantConflictFind * qcf = d_quantEngine->getConflictFind(); + if( qcf ){ + //reset QCF module + qcf->computeRelevantEqr(); + qcf->setEffort( QuantConflictFind::effort_conflict ); + //get the proper quantifiers info + std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f ); + if( it!=d_qinfo.end() ){ + QuantInfo * qi = &it->second; + if( qi->d_mg->isValid() ){ + Node rr = TermDb::getRewriteRule( f ); + Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl; + qi->reset_round( qcf ); + Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl; + while( qi->d_mg->getNextMatch( qcf, qi ) && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ + Trace("rewrite-engine-inst-debug") << " Got match to complete..." << std::endl; + qi->debugPrintMatch( "rewrite-engine-inst-debug" ); + std::vector< int > assigned; + if( !qi->isMatchSpurious( qcf ) ){ + bool doContinue = false; + bool success = true; + int tempAddedLemmas = 0; + while( tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){ + success = qi->completeMatch( qcf, assigned, doContinue ); + doContinue = true; + if( success ){ + Trace("rewrite-engine-inst-debug") << " Construct match..." << std::endl; + std::vector< Node > inst; + qi->getMatch( inst ); + Trace("rewrite-engine-inst-debug") << " Add instantiation..." << std::endl; + for( unsigned i=0; i "; + if( if[0].getNumChildren() ){ + inst.resize( f[0].getNumChildren() ); + } + if( d_quantEngine->addInstantiation( f, inst ) ){ + addedLemmas++; + tempAddedLemmas++; + /* + //remove rewritten terms from consideration + std::vector< Node > to_remove; + switch( rr[2].getKind() ){ + case kind::RR_REWRITE: + to_remove.push_back( rr[2][0] ); + break; + case kind::RR_REDUCTION: + for( unsigned i=0; igetSubstitute( to_remove[j], inst ); + Trace("rewrite-engine-inst-debug") << "Will remove : " << ns << std::endl; + ns.setAttribute(NoMatchAttribute(),true); + } + */ + }else{ + Trace("rewrite-engine-inst-debug") << " - failed." << std::endl; + } + Trace("rewrite-engine-inst-debug") << " Get next completion..." << std::endl; + } + } + //Trace("rewrite-engine-inst-debug") << " Reverted assigned variables : "; + //for( unsigned a=0; arevertMatch( assigned ); + //Assert( assigned.empty() ); + Trace("rewrite-engine-inst-debug") << " - failed to complete." << std::endl; }else{ - Trace("rewrite-engine-inst-debug") << "failure." << std::endl; + Trace("rewrite-engine-inst-debug") << " - match is spurious." << std::endl; } + Trace("rewrite-engine-inst-debug") << " Get next match..." << std::endl; } + }else{ + Trace("rewrite-engine-inst-debug") << "...Invalid qinfo." << std::endl; } - }while(success); + }else{ + Trace("rewrite-engine-inst-debug") << "...No qinfo." << std::endl; + } } - Trace("rewrite-engine-inst") << "Rule " << f << " generated " << addedLemmas << " lemmas." << std::endl; + Trace("rewrite-engine-inst") << "-> 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; + Node rr = TermDb::getRewriteRule( f ); + if( !rr.isNull() ){ + Trace("rr-register") << "Register quantifier " << f << std::endl; + Trace("rr-register") << " 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; + d_rr[f] = rr; + d_needsSort = true; + Trace("rr-register") << " guard is : " << d_rr[f][1] << std::endl; + + QuantConflictFind * qcf = d_quantEngine->getConflictFind(); + if( qcf ){ + std::vector< Node > qcfn_c; + + std::vector< Node > bvl; + for( unsigned i=0; i cc; + //Node head = rr[2][0]; + //if( head!=d_true ){ + //Node head_eq = head.getType().isBoolean() ? head.iffNode( head ) : head.eqNode( head ); + //head_eq = head_eq.negate(); + //cc.push_back( head_eq ); + //Trace("rr-register-debug") << " head eq is " << head_eq << std::endl; + //} + //add patterns + for( unsigned i=1; i nc; + for( unsigned j=0; jmkBoundVar( f[2][i][j].getType() ); + if( f[2][i][j].getType().isBoolean() ){ + if( f[2][i][j].getKind()!=APPLY_UF ){ + nn = f[2][i][j].negate(); + }else{ + nn = f[2][i][j].iffNode( nbv ).negate(); + bvl.push_back( nbv ); + } + //nn = f[2][i][j].negate(); + }else{ + nn = f[2][i][j].eqNode( nbv ).negate(); + bvl.push_back( nbv ); + } + nc.push_back( nn ); + } + if( !nc.empty() ){ + Node n = nc.size()==1 ? nc[0] : NodeManager::currentNM()->mkNode( AND, nc ); + Trace("rr-register-debug") << " pattern is " << n << std::endl; + if( std::find( cc.begin(), cc.end(), n )==cc.end() ){ + cc.push_back( n ); + } + } + } + qcfn_c.push_back( NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvl ) ); + + std::vector< Node > body_c; + //add the guards + if( d_rr[f][1].getKind()==AND ){ + for( unsigned j=0; jmkNode( AND, cc ) ); + //make the body + qcfn_c.push_back( body_c.size()==1 ? body_c[0] : NodeManager::currentNM()->mkNode( OR, body_c ) ); + //make the quantified formula + d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c ); + Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl; + d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] ); + } } } @@ -184,3 +292,13 @@ void RewriteEngine::assertNode( Node n ) { } +Node RewriteEngine::getInstConstNode( Node n, Node q ) { + std::map< Node, Node >::iterator it = d_inst_const_node[q].find( n ); + if( it==d_inst_const_node[q].end() ){ + Node nn = d_quantEngine->getTermDatabase()->getInstConstantNode( n, q ); + d_inst_const_node[q][n] = nn; + return nn; + }else{ + return it->second; + } +} \ No newline at end of file diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index a9a2f9b46..f85803617 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -29,19 +29,28 @@ namespace CVC4 { namespace theory { namespace quantifiers { +class QuantInfo; + class RewriteEngine : public QuantifiersModule { typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; std::vector< Node > d_rr_quant; - std::map< Node, Node > d_rr_guard; + std::vector< Node > d_priority_order; + std::map< Node, Node > d_rr; Node d_true; /** explicitly provided patterns */ std::map< Node, std::vector< inst::Trigger* > > d_rr_triggers; + /** get the quantifer info object */ + std::map< Node, Node > d_qinfo_n; + std::map< Node, QuantInfo > d_qinfo; double getPriority( Node f ); + bool d_needsSort; + std::map< Node, std::map< Node, Node > > d_inst_const_node; + Node getInstConstNode( Node n, Node q ); private: - int checkRewriteRule( Node f ); + int checkRewriteRule( Node f, Theory::Effort e ); public: RewriteEngine( context::Context* c, QuantifiersEngine* qe ); diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp index 0023b05bc..900db62d0 100644 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -21,6 +21,7 @@ #include "theory/theory_engine.h" #include "util/sort_inference.h" #include "theory/uf/theory_uf_strong_solver.h" +#include "theory/uf/theory_uf.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 9a912130f..a9e77d3d2 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -47,19 +47,6 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ } } -void TermDb::addTermEfficient( Node n, std::set< Node >& added){ - static AvailableInTermDb aitdi; - if (inst::Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){ - //Already processed but new in this branch - n.setAttribute(aitdi,true); - added.insert( n ); - for( size_t i=0; i< n.getNumChildren(); i++ ){ - addTermEfficient(n[i],added); - } - } - -} - Node TermDb::getOperator( Node n ) { //return n.getOperator(); @@ -94,10 +81,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ return; } if( d_processed.find( n )==d_processed.end() ){ - ++(d_quantEngine->d_statistics.d_term_in_termdb); d_processed.insert(n); d_type_map[ n.getType() ].push_back( n ); - n.setAttribute(AvailableInTermDb(),true); //if this is an atomic trigger, consider adding it //Call the children? if( inst::Trigger::isAtomicTrigger( n ) ){ @@ -110,22 +95,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ for( size_t i=0; igetEfficientEMatcher(); - if( d_parents[n[i]][op].empty() ){ - //must add parent to equivalence class info - Node nir = d_quantEngine->getEqualityQuery()->getRepresentative( n[i] ); - EqClassInfo* eci_nir = eem->getEquivalenceClassInfo( nir ); - if( eci_nir ){ - eci_nir->d_pfuns[ op ] = true; - } - } - //add to parent structure - if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){ - d_parents[n[i]][op][i].push_back( n ); - Assert(!getParents(n[i],op,i).empty()); - } - } if( options::eagerInstQuant() ){ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){ int addedLemmas = 0; @@ -143,13 +112,6 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ addTerm( n[i], added, withinQuant ); } } - }else{ - if( options::efficientEMatching() && !TermDb::hasInstConstAttr(n)){ - //Efficient e-matching must be notified - //The term in triggers are not important here - Debug("term-db") << "New in this branch term " << n << std::endl; - addTermEfficient(n,added); - } } } @@ -647,3 +609,15 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ d_op_triggers[op].push_back( tr ); } } + +bool TermDb::isRewriteRule( Node q ) { + return !getRewriteRule( q ).isNull(); +} + +Node TermDb::getRewriteRule( Node q ) { + if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){ + return q[2][0][0]; + }else{ + return Node::null(); + } +} diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 66b45be2f..b3db6d266 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -44,15 +44,6 @@ typedef expr::Attribute InstLevelAttribute; struct InstVarNumAttributeId {}; typedef expr::Attribute InstVarNumAttribute; -// Attribute that tell if a node have been asserted in this branch -struct AvailableInTermDbId {}; -/** use the special for boolean flag */ -typedef expr::Attribute AvailableInTermDb; - struct ModelBasisAttributeId {}; typedef expr::Attribute ModelBasisAttribute; //for APPLY_UF terms, 1 : term has direct child with model basis attribute, @@ -60,10 +51,6 @@ typedef expr::Attribute ModelBasisAttribute; struct ModelBasisArgAttributeId {}; typedef expr::Attribute ModelBasisArgAttribute; -//for rewrite rules -struct QRewriteRuleAttributeId {}; -typedef expr::Attribute QRewriteRuleAttribute; - //for bounded integers struct BoundIntLitAttributeId {}; typedef expr::Attribute BoundIntLitAttribute; @@ -128,9 +115,6 @@ public: void reset( Theory::Effort effort ); /** get operation */ Node getOperator( Node n ); -private: - /** for efficient e-matching */ - void addTermEfficient( Node n, std::set< Node >& added); public: /** parent structure (for efficient E-matching): n -> op -> index -> L @@ -252,6 +236,11 @@ public: int isInstanceOf( Node n1, Node n2 ); /** filter all nodes that have instances */ void filterInstances( std::vector< Node >& nodes ); +public: + /** is quantifier treated as a rewrite rule? */ + static bool isRewriteRule( Node q ); + /** get the rewrite rule associated with the quanfied formula */ + static Node getRewriteRule( Node q ); };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index b13d8601e..93bd2c012 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -104,6 +104,92 @@ struct QuantifierInstPatternListTypeRule { } };/* struct QuantifierInstPatternListTypeRule */ + +class RewriteRuleTypeRule { +public: + + /** + * Compute the type for (and optionally typecheck) a term belonging + * to the theory of rewriterules. + * + * @param nodeManager the NodeManager in use + * @param n the node to compute the type of + * @param check if true, the node's type should be checked as well + * as computed. + */ + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, + bool check) + throw(TypeCheckingExceptionPrivate) { + Debug("typecheck-r") << "type check for rr " << n << std::endl; + Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 ); + if( check ){ + if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ + throw TypeCheckingExceptionPrivate(n[0], + "first argument of rewrite rule is not bound var list"); + } + if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ + throw TypeCheckingExceptionPrivate(n[1], + "guard of rewrite rule is not an actual guard"); + } + if( n[2].getType(check) != + TypeNode(nodeManager->mkTypeConst(RRHB_TYPE))){ + throw TypeCheckingExceptionPrivate(n[2], + "not a correct rewrite rule"); + } + } + return nodeManager->booleanType(); + } +};/* class RewriteRuleTypeRule */ + + +class RRRewriteTypeRule { +public: + + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::RR_REWRITE ); + if( check ){ + if( n[0].getType(check)!=n[1].getType(check) ){ + throw TypeCheckingExceptionPrivate(n, + "terms of rewrite rule are not equal"); + } + if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ + throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); + } + if( n[0].getKind()!=kind::APPLY_UF ){ + throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation"); + } + } + return TypeNode(nodeManager->mkTypeConst(RRHB_TYPE)); + } +};/* struct QuantifierReductionRuleRule */ + +class RRRedDedTypeRule { +public: + + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::RR_REDUCTION || + n.getKind() == kind::RR_DEDUCTION ); + if( check ){ + if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){ + throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean"); + } + if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ + throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean"); + } + if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ + throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); + } + if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst(true) ){ + throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); + } + } + return TypeNode(nodeManager->mkTypeConst(RRHB_TYPE)); + } +};/* struct QuantifierReductionRuleRule */ + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 41f53740a..02423e54d 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -25,13 +25,14 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" -#include "theory/rewriterules/efficient_e_matching.h" -#include "theory/rewriterules/rr_trigger.h" +//#include "theory/rewriterules/efficient_e_matching.h" +//#include "theory/rewriterules/rr_trigger.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/uf/options.h" +#include "theory/uf/theory_uf.h" using namespace std; using namespace CVC4; @@ -46,8 +47,8 @@ d_lemmas_produced_c(u){ 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_rr_tr_trie = new rrinst::TriggerTrie; + //d_eem = new EfficientEMatcher( this ); d_hasAddedLemma = false; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; @@ -74,7 +75,7 @@ d_lemmas_produced_c(u){ } //add quantifiers modules - if( options::quantConflictFind() ){ + if( options::quantConflictFind() || options::quantRewriteRules() ){ d_qcf = new quantifiers::QuantConflictFind( this, c); d_modules.push_back( d_qcf ); }else{ @@ -100,7 +101,7 @@ d_lemmas_produced_c(u){ d_model_engine = NULL; d_bint = NULL; } - if( options::rewriteRulesAsAxioms() ){ + if( options::quantRewriteRules() ){ d_rr_engine = new quantifiers::RewriteEngine( c, this ); d_modules.push_back(d_rr_engine); }else{ @@ -129,10 +130,6 @@ EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } -//Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ -// return d_te->theoryOf( id )->getInstantiator(); -//} - context::Context* QuantifiersEngine::getSatContext(){ return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext(); } @@ -176,6 +173,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_rel_dom ){ d_rel_dom->reset(); } + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->reset_round( e ); + } if( e==Theory::EFFORT_LAST_CALL ){ //if effort is last call, try to minimize model first if( options::finiteModelFind() ){ @@ -216,7 +216,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ void QuantifiersEngine::registerQuantifier( Node f ){ if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){ - Trace("quant") << "Register quantifier : " << f << std::endl; + Trace("quant") << "QuantifiersEngine : Register quantifier "; + if( d_term_db->isRewriteRule( f ) ){ + Trace("quant") << " (rewrite rule)"; + } + Trace("quant") << " : " << f << std::endl; d_quants.push_back( f ); ++(d_statistics.d_num_quant); @@ -277,9 +281,6 @@ Node QuantifiersEngine::getNextDecisionRequest(){ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ std::set< Node > added; getTermDatabase()->addTerm( n, added, withinQuant ); - if( options::efficientEMatching() ){ - d_eem->newTerms( added ); - } //added contains also the Node that just have been asserted in this branch if( d_quant_rel ){ for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ @@ -361,7 +362,7 @@ void QuantifiersEngine::setInstantiationLevelAttr( Node n, uint64_t level ){ } } -Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){ +Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){ if( n.getKind()==INST_CONSTANT ){ Debug("check-inst") << "Substitute inst constant : " << n << std::endl; return terms[n.getAttribute(InstVarNumAttribute())]; @@ -377,7 +378,7 @@ Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){ } bool changed = false; for( unsigned i=0; i& vars, std }else{ //do optimized version Node icb = d_term_db->getInstConstantBody( f ); - body = doSubstitute( icb, terms ); + body = getSubstitute( icb, terms ); if( Debug.isOn("check-inst") ){ Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); if( body!=body2 ){ @@ -612,15 +613,7 @@ QuantifiersEngine::Statistics::Statistics(): d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), - d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0), - d_term_in_termdb("QuantifiersEngine::Term_in_TermDb", 0), - d_num_mono_candidates("QuantifiersEngine::NumMonoCandidates", 0), - d_num_mono_candidates_new_term("QuantifiersEngine::NumMonoCandidatesNewTerm", 0), - d_num_multi_candidates("QuantifiersEngine::NumMultiCandidates", 0), - d_mono_candidates_cache_hit("QuantifiersEngine::MonoCandidatesCacheHit", 0), - d_mono_candidates_cache_miss("QuantifiersEngine::MonoCandidatesCacheMiss", 0), - d_multi_candidates_cache_hit("QuantifiersEngine::MultiCandidatesCacheHit", 0), - d_multi_candidates_cache_miss("QuantifiersEngine::MultiCandidatesCacheMiss", 0) + d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0) { StatisticsRegistry::registerStat(&d_num_quant); StatisticsRegistry::registerStat(&d_instantiation_rounds); @@ -634,14 +627,6 @@ QuantifiersEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_simple_triggers); StatisticsRegistry::registerStat(&d_multi_triggers); StatisticsRegistry::registerStat(&d_multi_trigger_instantiations); - StatisticsRegistry::registerStat(&d_term_in_termdb); - StatisticsRegistry::registerStat(&d_num_mono_candidates); - StatisticsRegistry::registerStat(&d_num_mono_candidates_new_term); - StatisticsRegistry::registerStat(&d_num_multi_candidates); - StatisticsRegistry::registerStat(&d_mono_candidates_cache_hit); - StatisticsRegistry::registerStat(&d_mono_candidates_cache_miss); - StatisticsRegistry::registerStat(&d_multi_candidates_cache_hit); - StatisticsRegistry::registerStat(&d_multi_candidates_cache_miss); } QuantifiersEngine::Statistics::~Statistics(){ @@ -657,14 +642,6 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_simple_triggers); StatisticsRegistry::unregisterStat(&d_multi_triggers); StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations); - StatisticsRegistry::unregisterStat(&d_term_in_termdb); - StatisticsRegistry::unregisterStat(&d_num_mono_candidates); - StatisticsRegistry::unregisterStat(&d_num_mono_candidates_new_term); - StatisticsRegistry::unregisterStat(&d_num_multi_candidates); - StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_hit); - StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_miss); - StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_hit); - StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss); } eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index fbc501aec..858093543 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -20,8 +20,8 @@ #include "theory/theory.h" #include "util/hash.h" #include "theory/quantifiers/inst_match.h" -#include "theory/rewriterules/rr_inst_match.h" #include "theory/quantifiers/quant_util.h" +#include "expr/attribute.h" #include "util/statistics_registry.h" @@ -49,6 +49,8 @@ public: virtual void finishInit() {} /* whether this module needs to check this round */ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; } + /* reset at a round */ + virtual void reset_round( Theory::Effort e ){} /* Call during quantifier engine's check */ virtual void check( Theory::Effort e ) = 0; /* Called for new quantifiers */ @@ -75,11 +77,7 @@ namespace inst { class TriggerTrie; }/* CVC4::theory::inst */ -namespace rrinst { - class TriggerTrie; -}/* CVC4::theory::inst */ - -class EfficientEMatcher; +//class EfficientEMatcher; class EqualityQueryQuantifiersEngine; class QuantifiersEngine { @@ -102,8 +100,6 @@ private: quantifiers::RelevantDomain* d_rel_dom; /** phase requirements for each quantifier for each instantiation literal */ std::map< Node, QuantPhaseReq* > d_phase_reqs; - /** efficient e-matcher */ - EfficientEMatcher* d_eem; /** instantiation engine */ quantifiers::InstantiationEngine* d_inst_engine; /** model engine */ @@ -131,8 +127,6 @@ 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; /** statistics for debugging */ @@ -144,8 +138,6 @@ private: public: QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); - /** get instantiator for id */ - //Instantiator* getInstantiator( theory::TheoryId id ); /** get theory engine */ TheoryEngine* getTheoryEngine() { return d_te; } /** get equality query object for the given type. The default is the @@ -171,8 +163,6 @@ public: QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } /** get phase requirement terms */ void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); - /** get efficient e-matching utility */ - EfficientEMatcher* getEfficientEMatcher() { return d_eem; } /** get bounded integers utility */ quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; } /** Conflict find mechanism for quantifiers */ @@ -199,8 +189,6 @@ private: bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); /** set instantiation level attr */ void setInstantiationLevelAttr( Node n, uint64_t level ); - /** do substitution */ - Node doSubstitute( Node n, std::vector< Node >& terms ); public: /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms ); @@ -208,6 +196,8 @@ public: Node getInstantiation( Node f, InstMatch& m ); /** get instantiation */ Node getInstantiation( Node f, std::vector< Node >& terms ); + /** do substitution */ + Node getSubstitute( Node n, std::vector< Node >& terms ); /** exist instantiation ? */ bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ); /** add lemma lem */ @@ -238,8 +228,6 @@ 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 ); /** get the master equality engine */ @@ -260,14 +248,6 @@ public: IntStat d_simple_triggers; IntStat d_multi_triggers; IntStat d_multi_trigger_instantiations; - IntStat d_term_in_termdb; - IntStat d_num_mono_candidates; - IntStat d_num_mono_candidates_new_term; - IntStat d_num_multi_candidates; - IntStat d_mono_candidates_cache_hit; - IntStat d_mono_candidates_cache_miss; - IntStat d_multi_candidates_cache_hit; - IntStat d_multi_candidates_cache_miss; Statistics(); ~Statistics(); };/* class QuantifiersEngine::Statistics */ diff --git a/src/theory/rewriterules/kinds b/src/theory/rewriterules/kinds index 490c8f100..4ea0ecd43 100644 --- a/src/theory/rewriterules/kinds +++ b/src/theory/rewriterules/kinds @@ -14,24 +14,4 @@ properties check # constants... -# types... -sort RRHB_TYPE \ - Cardinality::INTEGERS \ - not-well-founded \ - "head and body of the rule type" - -# operators... - -# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE -operator REWRITE_RULE 3 "general rewrite rule" -#HEAD/BODY/TRIGGER -operator RR_REWRITE 2:3 "actual rewrite rule" -operator RR_REDUCTION 2:3 "actual reduction rule" -operator RR_DEDUCTION 2:3 "actual deduction rule" - -typerule REWRITE_RULE ::CVC4::theory::rewriterules::RewriteRuleTypeRule -typerule RR_REWRITE ::CVC4::theory::rewriterules::RRRewriteTypeRule -typerule RR_REDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule -typerule RR_DEDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule - endtheory diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 7fe625da1..37187e684 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -16,12 +16,7 @@ **/ #include "theory/rewriterules/theory_rewriterules.h" -#include "theory/rewriterules/theory_rewriterules_rules.h" -#include "theory/rewriterules/theory_rewriterules_params.h" - -#include "theory/rewriterules/theory_rewriterules_preprocess.h" #include "theory/rewriter.h" -#include "theory/rewriterules/options.h" using namespace std; @@ -38,159 +33,26 @@ namespace theory { namespace rewriterules { -inline std::ostream& operator <<(std::ostream& stream, const RuleInst& ri) { - ri.toStream(stream); - return stream; -} - -static const RuleInst* RULEINST_TRUE = (RuleInst*) 1; -static const RuleInst* RULEINST_FALSE = (RuleInst*) 2; - - /** Rule an instantiation with the given match */ -RuleInst::RuleInst(TheoryRewriteRules & re, const RewriteRule * r, - std::vector & inst_subst, - Node matched): - rule(r), d_matched(matched) -{ - Assert(r != NULL); - Assert(!r->directrr || !d_matched.isNull()); - subst.swap(inst_subst); -}; - -Node RuleInst::substNode(const TheoryRewriteRules & re, TNode r, - TCache cache ) const { - Assert(this != RULEINST_TRUE && this != RULEINST_FALSE); - return r.substitute (rule->free_vars.begin(),rule->free_vars.end(), - subst.begin(),subst.end(),cache); -}; -size_t RuleInst::findGuard(TheoryRewriteRules & re, size_t start)const{ - TCache cache; - Assert(this != RULEINST_TRUE && this != RULEINST_FALSE); - while (start < (rule->guards).size()){ - Node g = substNode(re,rule->guards[start],cache); - switch(re.addWatchIfDontKnow(g,this,start)){ - case ATRUE: - Debug("rewriterules::guards") << g << "is true" << std::endl; - ++start; - continue; - case AFALSE: - Debug("rewriterules::guards") << g << "is false" << std::endl; - return -1; - case ADONTKNOW: - Debug("rewriterules::guards") << g << "is unknown" << std::endl; - return start; - } - } - /** All the guards are verified */ - re.propagateRule(this,cache); - return start; -}; - -bool RuleInst::alreadyRewritten(TheoryRewriteRules & re) const{ - Assert(this != RULEINST_TRUE && this != RULEINST_FALSE); - static NoMatchAttribute rewrittenNodeAttribute; - TCache cache; - for(std::vector::const_iterator - iter = rule->to_remove.begin(); - iter != rule->to_remove.end(); ++iter){ - if (substNode(re,*iter,cache).getAttribute(rewrittenNodeAttribute)) - return true; - }; - return false; -} - -void RuleInst::toStream(std::ostream& out) const{ - if(this == RULEINST_TRUE){ out << "TRUE"; return;}; - if(this == RULEINST_FALSE){ out << "FALSE"; return;}; - out << "(" << *rule << ") "; - for(std::vector::const_iterator - iter = subst.begin(); iter != subst.end(); ++iter){ - out << *iter << " "; - }; -} - - -void Guarded::nextGuard(TheoryRewriteRules & re)const{ - Assert(inst != RULEINST_TRUE && inst != RULEINST_FALSE); - if(simulateRewritting && inst->alreadyRewritten(re)) return; - inst->findGuard(re,d_guard+1); -}; - -/** start indicate the first guard which is not true */ -Guarded::Guarded(const RuleInst* ri, const size_t start) : - d_guard(start),inst(ri) {}; -Guarded::Guarded(const Guarded & g) : - d_guard(g.d_guard),inst(g.inst) {}; -Guarded::Guarded() : - //dumb value - d_guard(-1),inst(RULEINST_TRUE) {}; - TheoryRewriteRules::TheoryRewriteRules(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo), - d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0), - d_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false) + Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo) { - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); -} - -void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r, - rrinst::InstMatch & im, - bool delay){ - ++r->nb_matched; - ++d_statistics.d_match_found; - if(rewrite_instantiation) im.applyRewrite(); - if(representative_instantiation) - im.makeRepresentative( getQuantifiersEngine() ); - if(!cache_match || !r->inCache(*this,im)){ - ++r->nb_applied; - ++d_statistics.d_cache_miss; - std::vector subst; - //AJR: replaced computeTermVec with this - for( size_t i=0; iinst_vars.size(); i++ ){ - Node n = im.getValue( r->inst_vars[i] ); - Assert( !n.isNull() ); - subst.push_back( n ); - } - RuleInst * ri = new RuleInst(*this,r,subst, - r->directrr ? im.d_matched : Node::null()); - Debug("rewriterules::matching") << "One matching found" - << (delay? "(delayed)":"") - << ":" << *ri << std::endl; - // Find the first non verified guard, don't save the rule if the - // rule can already be fired In fact I save it otherwise strange - // things append. - Assert(ri->rule != NULL); - if(delay) d_ruleinsts_to_add.push_back(ri); - else{ - if(simulateRewritting && ri->alreadyRewritten(*this)) return; - if(ri->findGuard(*this, 0) != (r->guards).size()) - d_ruleinsts.push_back(ri); - else delete(ri); - }; - }else{ - ++d_statistics.d_cache_hit; - }; } void TheoryRewriteRules::check(Effort level) { CodeTimer codeTimer(d_theoryTime); - Assert(d_ruleinsts_to_add.empty()); - while(!done()) { // Get all the assertions // TODO: Test that it have already been ppAsserted //if we are here and ppAssert has not been done // that means that ppAssert is off so we need to assert now - if(!d_ppAssert_on) addRewriteRule(get()); - else get(); + Assertion assertion = get(); // Assertion assertion = get(); // TNode fact = assertion.assertion; @@ -199,442 +61,18 @@ void TheoryRewriteRules::check(Effort level) { // Unhandled(getValuation().getDecisionLevel()); // addRewriteRule(fact); - }; - - Debug("rewriterules::check") << "RewriteRules::Check start " << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl; - - /** Test each rewrite rule */ - for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid) { - RewriteRule * r = d_rules[rid]; - if (level!=EFFORT_FULL && r->d_split) continue; - Debug("rewriterules::check") << "RewriteRules::Check rule: " << *r << std::endl; - Trigger & tr = r->trigger; - //reset instantiation round for trigger (set up match production) - tr.resetInstantiationRound(); - - /** Test the possible matching one by one */ - while(tr.getNextMatch()){ - rrinst::InstMatch im = tr.getInstMatch(); - addMatchRuleTrigger(r, im, true); - } - } - - const bool do_notification = d_checkLevel == 0 || level==EFFORT_FULL; - bool polldone = false; - - if(level==EFFORT_FULL) ++d_statistics.d_full_check; - else ++d_statistics.d_check; - - GuardedMap::const_iterator p = d_guardeds.begin(); - do{ - - - //dequeue instantiated rules - for(; !d_ruleinsts_to_add.empty();){ - RuleInst * ri = d_ruleinsts_to_add.back(); d_ruleinsts_to_add.pop_back(); - if(simulateRewritting && ri->alreadyRewritten(*this)) continue; - if(ri->findGuard(*this, 0) != ri->rule->guards.size()) - d_ruleinsts.push_back(ri); - else delete(ri); - }; - - if(do_notification) - /** Temporary way. Poll value */ - for (; p != d_guardeds.end(); ++p){ - TNode g = (*p).first; - const GList * const l = (*p).second; - const Guarded & glast = l->back(); - // Notice() << "Polled?:" << g << std::endl; - if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) continue; - // Notice() << "Polled!:" << g << "->" << (glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) << std::endl; - bool value; - if(getValuation().hasSatValue(g,value)){ - if(value) polldone = true; //One guard is true so pass n check - Debug("rewriterules::guards") << "Poll value:" << g - << " is " << (value ? "true" : "false") << std::endl; - notification(g,value); - //const Guarded & glast2 = (*l)[l->size()-1]; - // Notice() << "Polled!!:" << g << "->" << (glast2.inst == RULEINST_TRUE||glast2.inst == RULEINST_FALSE) << std::endl; - }; - }; - - }while(!d_ruleinsts_to_add.empty() || - (p != d_guardeds.end() && do_notification)); - - if(polldone) d_checkLevel = checkSlowdown; - else d_checkLevel = d_checkLevel > 0 ? (d_checkLevel - 1) : 0; - - /** Narrowing by splitting on the guards */ - /** Perhaps only when no notification? */ - if(narrowing_full_effort && level==EFFORT_FULL){ - for (GuardedMap::const_iterator p = d_guardeds.begin(); - p != d_guardeds.end(); ++p){ - TNode g = (*p).first; - const GList * const l = (*p).second; - const Guarded & glast = (*l)[l->size()-1]; - if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) - continue; - // If it has a value it should already has been notified - bool value CVC4_UNUSED; - Assert(!getValuation().hasSatValue(g,value)); - Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl; - /** Can split on already rewritten instrule... but... */ - getOutputChannel().split(g); } - } - - Assert(d_ruleinsts_to_add.empty()); - Debug("rewriterules::check") << "RewriteRules::Check done " << d_checkLevel << std::endl; - -}; - -void TheoryRewriteRules::registerQuantifier( Node n ){}; - -Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector & pattern ) { - // Debug("rewriterules") << "createTrigger:"; - getQuantifiersEngine()->registerPattern(pattern); - return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern, - options::efficientEMatching()? - Trigger::MATCH_GEN_EFFICIENT_E_MATCH : - Trigger::MATCH_GEN_DEFAULT, - true, - Trigger::TR_MAKE_NEW, - false); - // options::smartMultiTriggers()); -}; - -bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested, - GList * const lpropa) { - Assert(ltested->size() > 0); - const Guarded & glast = (*ltested)[ltested->size()-1]; - if(glast.inst == RULEINST_TRUE || glast.inst == RULEINST_FALSE){ - notification(lpropa,glast.inst == RULEINST_TRUE); - return true; - }; - return false; -}; - -void TheoryRewriteRules::notification(GList * const lpropa, bool b){ - if (b){ - for(size_t ig = 0; - ig != lpropa->size(); ++ig) { - (*lpropa)[ig].nextGuard(*this); - }; - lpropa->push_back(Guarded(RULEINST_TRUE,0)); - }else{ - lpropa->push_back(Guarded(RULEINST_FALSE,0)); - }; - Assert(lpropa->back().inst == RULEINST_TRUE || - lpropa->back().inst == RULEINST_FALSE); }; - - -Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri, - const size_t gid){ - /** Currently create a node with a literal */ - Node g = getValuation().ensureLiteral(g0); - GuardedMap::iterator l_i = d_guardeds.find(g); - GList* l; - if( l_i == d_guardeds.end() ) { - /** Normally Not watched so IDONTNOW but since we poll, we can poll now */ - bool value; - if(getValuation().hasSatValue(g,value)){ - if(value) return ATRUE; - else return AFALSE; - }; - //Not watched so IDONTNOW - l = new(getSatContext()->getCMM()) - GList(true, getSatContext());//, - //ContextMemoryAllocator(getContext()->getCMM())); - d_guardeds.insert(g ,l);//.insertDataFromContextMemory(g, l); - /* TODO Add register propagation */ - } else { - l = (*l_i).second; - Assert(l->size() > 0); - const Guarded & glast = (*l)[l->size()-1]; - if(glast.inst == RULEINST_TRUE) return ATRUE; - if(glast.inst == RULEINST_FALSE) return AFALSE; - - }; - /** I DONT KNOW because not watched or because not true nor false */ - l->push_back(Guarded(ri,gid)); - return ADONTKNOW; -}; - -void TheoryRewriteRules::notification(Node g, bool b){ - GuardedMap::const_iterator l = d_guardeds.find(g); - /** Should be a propagated node already known */ - Assert(l != d_guardeds.end()); - notification((*l).second,b); -} - - -void TheoryRewriteRules::notifyEq(TNode lhs, TNode rhs) { - GuardedMap::const_iterator ilhs = d_guardeds.find(lhs); - GuardedMap::const_iterator irhs = d_guardeds.find(rhs); - /** Should be a propagated node already known */ - Assert(ilhs != d_guardeds.end()); - if( irhs == d_guardeds.end() ) { - /** Not watched so points to the list directly */ - d_guardeds.insertDataFromContextMemory(rhs, (*ilhs).second); - } else { - GList * const llhs = (*ilhs).second; - GList * const lrhs = (*irhs).second; - if(!(notifyIfKnown(llhs,lrhs) || notifyIfKnown(lrhs,llhs))){ - /** If none of the two is known */ - for(GList::const_iterator g = llhs->begin(); g != llhs->end(); ++g){ - lrhs->push_back(*g); - }; - }; - }; -}; - - -Node TheoryRewriteRules::normalizeConjunction(NodeBuilder<> & conjunction){ - Assert(conjunction.getKind() == kind::AND); - switch(conjunction.getNumChildren()){ - case 0: - return d_true; - case 1: - return conjunction[0]; - default: - return conjunction; - } - -} - -void explainInstantiation(const RuleInst *inst, TNode substHead, NodeBuilder<> & conjunction ){ - TypeNode booleanType = NodeManager::currentNM()->booleanType(); - // if the rule is directly applied by the rewriter, - // we should take care to use the representative that can't be directly rewritable: - // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't - // add the constraint car(cons(x,l) = x because it is rewritten to x = x. - // But we should say cons(a) = x - Assert(!inst->d_matched.isNull()); - Assert( inst->d_matched.getKind() == kind::APPLY_UF); - Assert( substHead.getKind() == kind::APPLY_UF ); - Assert( inst->d_matched.getOperator() == substHead.getOperator() ); - Assert(conjunction.getKind() == kind::AND); - // replace the left hand side by the term really matched - NodeBuilder<2> nb; - for(size_t i = 0, - iend = inst->d_matched.getNumChildren(); i < iend; ++i){ - nb.clear( inst->d_matched[i].getType(false) == booleanType ? - kind::IFF : kind::EQUAL ); - nb << inst->d_matched[i] << substHead[i]; - conjunction << static_cast(nb); - } -} - -Node skolemizeBody( Node f ){ - /*TODO skolemize the subformula of s with constant or skolemize - directly in the body of the rewrite rule with an uninterpreted - function. - */ - if ( f.getKind()!=EXISTS ) return f; - std::vector< Node > vars; - std::vector< Node > csts; - for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - csts.push_back( NodeManager::currentNM()->mkSkolem( "skolem_$$", f[0][i].getType(), "is from skolemizing the body of a rewrite rule" ) ); - vars.push_back( f[0][i] ); - } - return f[ 1 ].substitute( vars.begin(), vars.end(), - csts.begin(), csts.end() ); -} - - -void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){ - // Debug("rewriterules") << "A rewrite rules is verified. Add lemma:"; - Debug("rewriterules::propagate") << "propagateRule" << *inst << std::endl; - const RewriteRule * rule = inst->rule; - ++rule->nb_applied; - // Can be more something else than an equality in fact (eg. propagation rule) - Node equality = skolemizeBody(inst->substNode(*this,rule->body,cache)); - if(propagate_as_lemma){ - Node lemma = equality; - if(rule->directrr){ - NodeBuilder<> conjunction(kind::AND); - explainInstantiation(inst, - rule->guards.size() > 0? - inst->substNode(*this,rule->guards[0],cache) : equality[0], - conjunction); - Debug("rewriterules-directrr") << "lemma:" << lemma << " :: " << inst->d_matched; - //rewrite rule - TypeNode booleanType = NodeManager::currentNM()->booleanType(); - if(equality[1].getType(false) == booleanType) - equality = inst->d_matched.iffNode(equality[1]); - else equality = inst->d_matched.eqNode(equality[1]); - lemma = normalizeConjunction(conjunction).impNode(equality); - Debug("rewriterules-directrr") << " -> " << lemma << std::endl; - } - else if(rule->guards.size() > 0){ - // We can use implication for reduction rules since the head is known - // to be true - NodeBuilder<> conjunction(kind::AND); - substGuards(inst,cache,conjunction); - lemma = normalizeConjunction(conjunction).impNode(equality); - } - Debug("rewriterules::propagate") << "propagated " << lemma << std::endl; - getOutputChannel().lemma(lemma); - }else{ - Node lemma_lit = equality; - if(rule->directrr && rule->guards.size() == 0) - lemma_lit = inst->d_matched.eqNode(equality[1]); // rewrite rules - lemma_lit = getValuation().ensureLiteral(lemma_lit); - ExplanationMap::const_iterator p = d_explanations.find(lemma_lit); - if(p!=d_explanations.end()) return; //Already propagated - bool value; - if(getValuation().hasSatValue(lemma_lit,value)){ - /* Already assigned */ - if (!value){ - NodeBuilder<> conflict(kind::AND); - - if(rule->directrr){ - explainInstantiation(inst, - rule->guards.size() > 0? - inst->substNode(*this,rule->guards[0],cache) : equality[0], - conflict); - if(rule->guards.size() > 0){ - //reduction rule - Assert(rule->guards.size() == 1); - conflict << inst->d_matched; //this one will be two times - } - } - substGuards(inst,cache,conflict); - conflict << lemma_lit; - getOutputChannel().conflict(normalizeConjunction(conflict)); - }; - }else{ - getOutputChannel().propagate(lemma_lit); - d_explanations.insert(lemma_lit, *inst); - }; - }; - - if(simulateRewritting){ - static NoMatchAttribute rewrittenNodeAttribute; - // Tag the rewritted terms - // for(std::vector::iterator i = rule->to_remove.begin(); - // i == rule->to_remove.end(); ++i){ - // (*i).setAttribute(rewrittenNodeAttribute,true); - // }; - for(size_t i = 0; i < rule->to_remove.size(); ++i){ - Node rewritten = inst->substNode(*this,rule->to_remove[i],cache); - Debug("rewriterules::simulateRewriting") << "tag " << rewritten << " as rewritten" << std::endl; - rewritten.setAttribute(rewrittenNodeAttribute,true); - }; - - }; - - if ( compute_opt && !rule->body_match.empty() ){ - - uf::TheoryUF* uf = static_cast(getQuantifiersEngine()->getTheoryEngine()->theoryOf( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast(uf->getEqualityEngine()); - - //Verify that this instantiation can't immediately fire another rule - for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin(); - p != rule->body_match.end(); ++p){ - RewriteRule * r = (*p).second; - // Use trigger2 since we can be in check - ApplyMatcher * tr = r->trigger_for_body_match; - Assert(tr != NULL); - tr->resetInstantiationRound(getQuantifiersEngine()); - rrinst::InstMatch im; - TNode m = inst->substNode(*this,(*p).first, cache); - Assert( m.getKind() == kind::APPLY_UF ); - ee->addTerm(m); - if( tr->reset(m,im,getQuantifiersEngine()) ){ - im.d_matched = m; - Debug("rewriterules::matching") << "SimulatedRewrite: " << std::endl; - addMatchRuleTrigger(r, im); - } - } - - } -}; - -void TheoryRewriteRules::substGuards(const RuleInst *inst, - TCache cache, - NodeBuilder<> & conjunction){ - const RewriteRule * r = inst->rule; - /** Guards */ /* TODO remove the duplicate with a set like in uf? */ - for(std::vector::const_iterator p = r->guards.begin(); - p != r->guards.end(); ++p) { - Assert(!p->isNull()); - conjunction << inst->substNode(*this,*p,cache); - }; -} - Node TheoryRewriteRules::explain(TNode n){ - ExplanationMap::const_iterator p = d_explanations.find(n); - Assert(p!=d_explanations.end(),"I forget the explanation..."); - RuleInst inst = (*p).second; - const RewriteRule * rule = inst.rule; - TCache cache; - NodeBuilder<> explanation(kind::AND); - if(rule->directrr){ - explainInstantiation(&inst, - rule->guards.size() > 0? - inst.substNode(*this,rule->guards[0],cache): - inst.substNode(*this,rule->body[0] ,cache), - explanation); - if(rule->guards.size() > 0){ - //reduction rule - Assert(rule->guards.size() == 1); - explanation << inst.d_matched; //this one will be two times - } - }; - substGuards(&inst, cache ,explanation); - return normalizeConjunction(explanation); -} - -void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){ + return Node::null(); } -Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - //TODO: here add only to the rewriterules database for ppRewrite, - //and not for the general one. Otherwise rewriting that occur latter - //on this rewriterules will be lost. But if the rewriting of the - //body is not done in "in", will it be done latter after - //substitution? Perhaps we should add the rewriterules to the - //database for ppRewrite also after the subtitution at the levvel of check - - // addRewriteRule(in); - // d_ppAssert_on = true; - return PP_ASSERT_STATUS_UNSOLVED; -} - -TheoryRewriteRules::Statistics::Statistics(): - d_num_rewriterules("TheoryRewriteRules::Num_RewriteRules", 0), - d_check("TheoryRewriteRules::Check", 0), - d_full_check("TheoryRewriteRules::FullCheck", 0), - d_poll("TheoryRewriteRules::Poll", 0), - d_match_found("TheoryRewriteRules::MatchFound", 0), - d_cache_hit("TheoryRewriteRules::CacheHit", 0), - d_cache_miss("TheoryRewriteRules::CacheMiss", 0) -{ - StatisticsRegistry::registerStat(&d_num_rewriterules); - StatisticsRegistry::registerStat(&d_check); - StatisticsRegistry::registerStat(&d_full_check); - StatisticsRegistry::registerStat(&d_poll); - StatisticsRegistry::registerStat(&d_match_found); - StatisticsRegistry::registerStat(&d_cache_hit); - StatisticsRegistry::registerStat(&d_cache_miss); -} +void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){ -TheoryRewriteRules::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_num_rewriterules); - StatisticsRegistry::unregisterStat(&d_check); - StatisticsRegistry::unregisterStat(&d_full_check); - StatisticsRegistry::unregisterStat(&d_poll); - StatisticsRegistry::unregisterStat(&d_match_found); - StatisticsRegistry::unregisterStat(&d_cache_hit); - StatisticsRegistry::unregisterStat(&d_cache_miss); } - }/* CVC4::theory::rewriterules namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index 2cefe7f07..85cd9a85c 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -25,173 +25,17 @@ #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "context/context_mm.h" -#include "theory/rewriterules/rr_inst_match_impl.h" -#include "theory/rewriterules/rr_trigger.h" -#include "theory/rewriterules/rr_inst_match.h" #include "util/statistics_registry.h" -#include "theory/rewriterules/theory_rewriterules_preprocess.h" namespace CVC4 { namespace theory { namespace rewriterules { -using namespace CVC4::theory::rrinst; -typedef CVC4::theory::rrinst::Trigger Trigger; - -typedef std::hash_map TCache; - - enum Answer {ATRUE, AFALSE, ADONTKNOW}; - - class TheoryRewriteRules; /** forward */ - - class RewriteRule{ - public: - // constant - const size_t id; //for debugging - const bool d_split; - mutable Trigger trigger; - std::vector guards; - mutable std::vector to_remove; /** terms to remove */ - const Node body; - const TNode new_terms; /** new terms included in the body */ - std::vector free_vars; /* free variable in the rule */ - std::vector inst_vars; /* corresponding vars in the triggers */ - /* After instantiating the body new match can appear (TNode - because is a subterm of a body on the assicaited rewrite - rule) */ - typedef context::CDList< std::pair > BodyMatch; - mutable BodyMatch body_match; - mutable ApplyMatcher * trigger_for_body_match; // used because we can be matching - // trigger when we need new match. - // So currently we use another - // trigger for that. - - //context dependent - typedef InstMatchTrie2 CacheNode; - mutable CacheNode d_cache; - - const bool directrr; - - RewriteRule(TheoryRewriteRules & re, - Trigger & tr, ApplyMatcher * tr2, - std::vector & g, Node b, TNode nt, - std::vector & fv,std::vector & iv, - std::vector & to_r, bool drr); - RewriteRule(const RewriteRule & r) CVC4_UNUSED; - RewriteRule& operator=(const RewriteRule &) CVC4_UNUSED; - ~RewriteRule(); - - bool noGuard()const throw () { return guards.size() == 0; }; - bool inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const; - - void toStream(std::ostream& out) const; - - /* statistics */ - mutable size_t nb_matched; - mutable size_t nb_applied; - mutable size_t nb_propagated; - - }; - - class RuleInst{ - public: - /** The rule has at least one guard */ - const RewriteRule* rule; - - /** the substitution */ - std::vector subst; - - /** the term matched (not null if mono-pattern and direct-rr) */ - Node d_matched; - - /** Rule an instantiation with the given match */ - RuleInst(TheoryRewriteRules & re, const RewriteRule* r, - std::vector & inst_subst, - Node matched); - RuleInst():rule(NULL){} // Dumb - - Node substNode(const TheoryRewriteRules & re, TNode r, TCache cache) const; - size_t findGuard(TheoryRewriteRules & re, size_t start)const; - - void toStream(std::ostream& out) const; - - bool alreadyRewritten(TheoryRewriteRules & re) const; - }; - -/** A pair? */ - class Guarded { - public: - /** The backtracking is done somewhere else */ - const size_t d_guard; /* the id of the guard */ - - /** The shared instantiation data */ - const RuleInst* inst; - - void nextGuard(TheoryRewriteRules & re)const; - - /** start indicate the first guard which is not true */ - Guarded(const RuleInst* ri, const size_t start); - Guarded(const Guarded & g); - /** Should be ssigned by a good garded after */ - Guarded(); - - ~Guarded(){}; - void destroy(){}; - }; - -template -class CleanUpPointer{ -public: - inline void operator()(T** e){ - delete(*e); - }; -}; class TheoryRewriteRules : public Theory { private: KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::rewriterules::theoryTime"); - - /** list of all rewrite rules */ - /* std::vector< Node > d_rules; */ - // typedef std::vector< std::pair > Rules; - typedef context::CDList< RewriteRule *, - CleanUpPointer, - std::allocator< RewriteRule * > > Rules; - Rules d_rules; - typedef context::CDList< RuleInst *, - CleanUpPointer, - std::allocator< RuleInst * > > RuleInsts; - RuleInsts d_ruleinsts; - - /** The GList* will lead too memory leaks since that doesn't use - CDChunckList */ - typedef context::CDList< Guarded > GList; - typedef context::CDHashMap GuardedMap; - GuardedMap d_guardeds; - - /* In order to not monopolize, the system slow down himself: If a - guard stored in d_guardeds become true or false, it waits - checkSlowdown(=10) checks before checking again if some guard take a - value. At FULL_EFFORT regardless of d_checkLevel it check the - guards - */ - context::CDO d_checkLevel; - - /** explanation */ - typedef context::CDHashMap ExplanationMap; - ExplanationMap d_explanations; - - /** new instantiation must be cleared at each conflict used only - inside check */ - typedef std::vector< RuleInst* > QRuleInsts; - QRuleInsts d_ruleinsts_to_add; - bool d_ppAssert_on; //Indicate if a ppAssert have been done - public: - /** true and false for predicate */ - Node d_true; - Node d_false; - /** Constructs a new instance of TheoryRewriteRules w.r.t. the provided context.*/ TheoryRewriteRules(context::Context* c, @@ -209,76 +53,6 @@ private: return "THEORY_REWRITERULES"; } - Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); - - bool ppDontRewriteSubterm(TNode atom) { return true; } - - - private: - void registerQuantifier( Node n ); - - public: - /* TODO modify when notification will be available */ - void notification( Node n, bool b); - - Trigger createTrigger( TNode n, std::vector & pattern ); - - /** return if the guard (already substituted) is known true or false - or unknown. In the last case it add the Guarded(rid,gid) to the watch - list of this guard */ - Answer addWatchIfDontKnow(Node g, const RuleInst* r, const size_t gid); - - /** An instantiation of a rule is fired (all guards true) we - propagate the body. That can be done by theory propagation if - possible or by lemmas. - */ - void propagateRule(const RuleInst * r, TCache cache); - - /** Auxiliary functions */ -private: - /** A guard is verify, notify the Guarded */ - void notification(GList * const lpropa, bool b); - /* If two guards becomes equals we should notify if one of them is - already true */ - bool notifyIfKnown(const GList * const ltested, GList * const lpropa); - - void substGuards(const RuleInst * inst, - TCache cache, - NodeBuilder<> & conjunction); - - void addRewriteRule(const Node r); - void computeMatchBody ( const RewriteRule * r, size_t start = 0); - void addMatchRuleTrigger(const RewriteRule* r, - rrinst::InstMatch & im, bool delay = true); - - Node normalizeConjunction(NodeBuilder<> & conjunction); - - /* rewrite pattern */ - typedef std::hash_map< Node, rewriter::RRPpRewrite*, NodeHashFunction > RegisterRRPpRewrite; - RegisterRRPpRewrite d_registeredRRPpRewrite; - - bool addRewritePattern(TNode pattern, TNode body, - rewriter::Subst & pvars, - rewriter::Subst & vars); - - //create inst variable - std::vector createInstVariable( Node r, std::vector & vars ); - - /** statistics class */ - class Statistics { - public: - IntStat d_num_rewriterules; - IntStat d_check; - IntStat d_full_check; - IntStat d_poll; - IntStat d_match_found; - IntStat d_cache_hit; - IntStat d_cache_miss; - Statistics(); - ~Statistics(); - }; - Statistics d_statistics; - };/* class TheoryRewriteRules */ }/* CVC4::theory::rewriterules namespace */ diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h index fa6bb2227..28b10f91f 100644 --- a/src/theory/rewriterules/theory_rewriterules_type_rules.h +++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h @@ -26,89 +26,7 @@ namespace CVC4 { namespace theory { namespace rewriterules { -class RewriteRuleTypeRule { -public: - /** - * Compute the type for (and optionally typecheck) a term belonging - * to the theory of rewriterules. - * - * @param nodeManager the NodeManager in use - * @param n the node to compute the type of - * @param check if true, the node's type should be checked as well - * as computed. - */ - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, - bool check) - throw(TypeCheckingExceptionPrivate) { - Debug("typecheck-r") << "type check for rr " << n << std::endl; - Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 ); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){ - throw TypeCheckingExceptionPrivate(n[0], - "first argument of rewrite rule is not bound var list"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n[1], - "guard of rewrite rule is not an actual guard"); - } - if( n[2].getType(check) != - TypeNode(nodeManager->mkTypeConst(RRHB_TYPE))){ - throw TypeCheckingExceptionPrivate(n[2], - "not a correct rewrite rule"); - } - } - return nodeManager->booleanType(); - } -};/* class RewriteRuleTypeRule */ - - -class RRRewriteTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { - Assert(n.getKind() == kind::RR_REWRITE ); - if( check ){ - if( n[0].getType(check)!=n[1].getType(check) ){ - throw TypeCheckingExceptionPrivate(n, - "terms of rewrite rule are not equal"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n[0].getKind()!=kind::APPLY_UF ){ - throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation"); - } - } - return TypeNode(nodeManager->mkTypeConst(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ - -class RRRedDedTypeRule { -public: - - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw(TypeCheckingExceptionPrivate) { - Assert(n.getKind() == kind::RR_REDUCTION || - n.getKind() == kind::RR_DEDUCTION ); - if( check ){ - if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean"); - } - if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){ - throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean"); - } - if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){ - throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list"); - } - if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst(true) ){ - throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); - } - } - return TypeNode(nodeManager->mkTypeConst(RRHB_TYPE)); - } -};/* struct QuantifierReductionRuleRule */ }/* CVC4::theory::rewriterules namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 80d1152da..45c9402ab 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,7 +52,7 @@ #include "theory/uf/equality_engine.h" -#include "theory/rewriterules/efficient_e_matching.h" +//#include "theory/rewriterules/efficient_e_matching.h" #include "proof/proof_manager.h" @@ -95,7 +95,7 @@ void TheoryEngine::eqNotifyNewClass(TNode t){ void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){ //TODO: add notification to efficient E-matching if( d_logicInfo.isQuantified() ){ - d_quantEngine->getEfficientEMatcher()->merge( t1, t2 ); + //d_quantEngine->getEfficientEMatcher()->merge( t1, t2 ); if( options::quantConflictFind() ){ d_quantEngine->getConflictFind()->merge( t1, t2 ); } diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2 index 8fe88e9f5..51d60e920 100644 --- a/test/regress/regress0/push-pop/bug326.smt2 +++ b/test/regress/regress0/push-pop/bug326.smt2 @@ -31,7 +31,7 @@ (check-sat) (pop) -; EXPECT: sat +; EXPECT: unknown (push);;sat (assert (and (not (R e1 e3)) (R e4 e1))) (check-sat) diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index b7eac2535..5aba7dcec 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -1,4 +1,4 @@ -CVC4_REGRESSION_ARGS ?= --efficient-e-matching +CVC4_REGRESSION_ARGS ?= --rewrite-rules export CVC4_REGRESSION_ARGS # don't override a BINARY imported from a personal.mk @@ -23,10 +23,11 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \ - datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \ - set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \ - reachability_back_to_the_future.smt2 native_arrays.smt2 -# reachability_bbttf_eT_arrays.smt2 + datatypes.smt2 datatypes_sat.smt2 reachability_back_to_the_future.smt2 \ + relation.smt2 simulate_rewriting.smt2 \ + native_arrays.smt2 + +# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 index d1d88a549..838c0cd16 100644 --- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 +++ b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 @@ -1,6 +1,6 @@ ;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba (set-logic AUFLIA) -(set-info :status sat) +(set-info :status unsat) (declare-sort elt1 0) (declare-sort elt2 0) -- 2.30.2