diff options
Diffstat (limited to 'src')
36 files changed, 1302 insertions, 1678 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; @@ -596,11 +598,6 @@ public: } /** - * Pre-skolemize quantifiers. - */ - Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs); - - /** * Substitute away all AbstractValues in a node. */ Node substituteAbstractValues(TNode n) { @@ -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<Node, Node, NodeHashF return result.top(); } - -struct ContainsQuantAttributeId {}; -typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> 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<Node> & 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: @@ -41,5 +43,7 @@ public: }; } +} +} #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; i<q[0].getNumChildren(); i++ ){
- if( d_has_var.find( q[0][i] )==d_has_var.end() ){
- d_isPartial = false;
- d_mg->setInvalid();
- 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<getNumVars(); i++ ){
- if( d_match[i].isNull() ){
- //Assert( i<(int)q[0].getNumChildren() );
- int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
- unassigned[rindex].push_back( i );
- unassigned_tn[rindex].push_back( getVar( i ).getType() );
- assigned.push_back( i );
+ bool doFail = false;
+ bool success = true;
+ if( doContinue ){
+ doFail = true;
+ success = false;
+ }else{
+ d_unassigned.clear();
+ d_unassigned_tn.clear();
+ std::vector< int > unassigned[2];
+ std::vector< TypeNode > unassigned_tn[2];
+ for( int i=0; i<getNumVars(); i++ ){
+ if( d_match[i].isNull() ){
+ int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
+ unassigned[rindex].push_back( i );
+ unassigned_tn[rindex].push_back( getVar( i ).getType() );
+ assigned.push_back( i );
+ }
+ }
+ d_unassigned_nvar = unassigned[0].size();
+ for( unsigned i=0; i<2; i++ ){
+ d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
+ d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
}
+ d_una_eqc_count.clear();
+ d_una_index = 0;
}
- bool success = true;
- for( unsigned r=0; r<2; r++ ){
- if( success && !unassigned[r].empty() ){
- Trace("qcf-check") << "Assign to unassigned, rep = " << r << "..." << std::endl;
- int index = 0;
- std::vector< int > 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_index<d_unassigned_nvar ){
+ if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
+ d_una_eqc_count.push_back( -1 );
}else{
- eqc_count.push_back( 0 );
+ d_var_mg[ d_unassigned[d_una_index] ]->reset( 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_index<d_unassigned_nvar ){
+ if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
+ Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
+ d_una_index++;
+ }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( 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<unassigned[r].size(); i++ ){
- int ui = unassigned[r][i];
- if( !d_match[ui].isNull() ){
- Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << 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_unassigned.size(); i++ ){
+ int ui = d_unassigned[i];
+ if( !d_match[ui].isNull() ){
+ Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << 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; i<d_q[0].getNumChildren(); i++ ){
+ //Node cv = qi->getCurrentValue( 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<assigned.size(); i++ ){
+ d_match[ assigned[i] ] = TNode::null();
+ }
+}
+
void QuantInfo::debugPrintMatch( const char * c ) {
for( int i=0; i<getNumVars(); i++ ){
Trace(c) << " " << d_vars[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; i<d_children.size(); i++ ){
d_children[i].reset_round( p );
}
@@ -849,6 +882,9 @@ void MatchGen::reset_round( QuantConflictFind * p ) { }
}
}
+ d_qni_bound_cons.clear();
+ d_qni_bound_cons_var.clear();
+ d_qni_bound.clear();
}
void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
@@ -860,6 +896,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { d_qni.clear();
d_qni_bound.clear();
d_child_counter = -1;
+ d_tgt_orig = d_tgt;
//set up processing matches
if( d_type==typ_invalid ){
@@ -870,6 +907,25 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { if( d_ground_eval[0]==( d_tgt ? p->d_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; i<getNumChildren(); i++ ){
+ if( !getChild( i )->getExplanation( 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; i<t.getNumChildren(); i++ ){
+ Node vi = getExplanationTerm( p, qi, t[i], exp );
+ if( vi!=v[i] ){
+ Node eq = vi.eqNode( v[i] );
+ if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
+ Trace("qcf-explain") << " add : " << eq << "." << std::endl;
+ exp.push_back( eq );
+ }
+ }
+ }
+ }
+ return v;
+}
+
bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
if( !d_qn.empty() ){
if( d_qn[0]==NULL ){
@@ -1297,14 +1438,17 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { Assert( !d_qni[d_qni.size()-1]->second.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; i<n.getNumChildren(); i++ ){
+ if( !isHandled( n[i] ) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
QuantifiersModule( qe ),
@@ -1377,30 +1540,32 @@ Node QuantConflictFind::mkEqNode( Node a, Node b ) { //-------------------------------------------------- registration
void QuantConflictFind::registerQuantifier( Node q ) {
- d_quants.push_back( q );
- d_quant_id[q] = d_quants.size();
- Trace("qcf-qregister") << "Register ";
- debugPrintQuant( "qcf-qregister", q );
- Trace("qcf-qregister") << " : " << q << std::endl;
- //make QcfNode structure
- Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
- d_qinfo[q].initialize( q, q[1] );
-
- //debug print
- Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
- Trace("qcf-qregister") << " ";
- debugPrintQuantBody( "qcf-qregister", q, q[1] );
- Trace("qcf-qregister") << std::endl;
- if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
- Trace("qcf-qregister") << " with additional constraints : " << std::endl;
- for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
- Trace("qcf-qregister") << " ?x" << j << " = ";
- debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
- Trace("qcf-qregister") << std::endl;
+ if( !TermDb::isRewriteRule( q ) ){
+ d_quants.push_back( q );
+ d_quant_id[q] = d_quants.size();
+ Trace("qcf-qregister") << "Register ";
+ debugPrintQuant( "qcf-qregister", q );
+ Trace("qcf-qregister") << " : " << q << std::endl;
+ //make QcfNode structure
+ Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
+ d_qinfo[q].initialize( q, q[1] );
+
+ //debug print
+ Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
+ Trace("qcf-qregister") << " ";
+ debugPrintQuantBody( "qcf-qregister", q, q[1] );
+ Trace("qcf-qregister") << std::endl;
+ if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
+ Trace("qcf-qregister") << " with additional constraints : " << std::endl;
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
+ Trace("qcf-qregister") << " ?x" << j << " = ";
+ debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
+ Trace("qcf-qregister") << std::endl;
+ }
}
- }
- Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
+ Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
+ }
}
int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
@@ -1481,6 +1646,20 @@ int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) { return ret;
}
+short QuantConflictFind::getMaxQcfEffort() {
+ if( options::qcfMode()==QCF_CONFLICT_ONLY ){
+ return effort_conflict;
+ }else if( options::qcfMode()==QCF_PROP_EQ ){
+ return effort_prop_eq;
+ }else if( options::qcfMode()==QCF_PARTIAL ){
+ return effort_partial;
+ }else if( options::qcfMode()==QCF_MC ){
+ return effort_mc;
+ }else{
+ return 0;
+ }
+}
+
bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
//if( d_effort==QuantConflictFind::effort_mc ){
// return n1==n2 || !areDisequal( n1, n2 );
@@ -1500,14 +1679,16 @@ bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) { //-------------------------------------------------- handling assertions / eqc
void QuantConflictFind::assertNode( Node 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 );
- //}
+ 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; i<q[0].getNumChildren(); i++ ){
- //Node cv = qi->getCurrentValue( 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<exp.size(); c++ ){
+ Trace("qcf-check-exp") << " " << exp[c] << std::endl;
}
- Debug("qcf-check-inst") << "INST : " << i << " -> " << 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; c<exp.size(); c++ ){
+ bool pol = exp[c].getKind()!=NOT;
+ TNode lit = pol ? exp[c] : exp[c][0];
+ Trace("qcf-check-exp") << "Explain " << lit << ", polarity " << pol << std::endl;
+ if( lit.getKind()==EQUAL ){
+ if( !pol && !ee->areDisequal( 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; c<c_exp.size(); c++ ){
+ Trace("qcf-check-exp") << " " << c_exp[c] << std::endl;
+ Node ccc = c_exp[c].negate();
+ if( std::find( c_lem.begin(), c_lem.end(), ccc )==c_lem.end() ){
+ c_lem.push_back( ccc );
+ }
}
- }else{
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
- //Assert( false );
+
+ c_lem.push_back( q.negate() );
+ Node conf = NodeManager::currentNM()->mkNode( 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; i<assigned.size(); i++ ){
- qi->d_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.size(); i++ ){ + if( activeMap[args[i]] ){ + activeArgs.push_back( args[i] ); + } + } +} + + bool QuantifiersRewriter::hasArg( std::vector< Node >& 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<Node> 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<body.getNumChildren(); i++ ){ std::vector< Node > activeArgs; - computeArgs( args, activeArgs, body[i] ); + computeArgVec( args, activeArgs, body[i] ); for (unsigned j=0; j<activeArgs.size(); j++ ){ varLits[activeArgs[j]].push_back( body[i] ); } @@ -964,3 +987,220 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption return false; } } + + + + +Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { + Kind rrkind = r[2].getKind(); + + //guards, pattern, body + + // Replace variables by Inst_* variable and tag the terms that contain them + std::vector<Node> 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<Node> guards; + std::vector<Node> 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<head.getNumChildren(); i++ ){ + guards.push_back(head[i]); + pattern.push_back(head[i]); + } + break; + default: + if( head!=true_node ){ + guards.push_back(head); + pattern.push_back( head ); + } + break; + } + break; + default: + Unreachable("RewriteRules can be of only three kinds"); + break; + } + // Add the other guards + TNode g = r[1]; + switch(g.getKind()){ + case kind::AND: + for( unsigned i = 0; i<g.getNumChildren(); i++ ){ + guards.push_back(g[i]); + } + break; + default: + if( g != true_node ){ + guards.push_back( g ); + } + break; + } + // Add the other triggers + if( r[2].getNumChildren() >= 3 ){ + for( unsigned i=0; i<r[2][2][0].getNumChildren(); i++ ) { + pattern.push_back( r[2][2][0][i] ); + } + } + + Trace("rr-rewrite") << "Rule is " << r << std::endl; + Trace("rr-rewrite") << "Head is " << head << std::endl; + Trace("rr-rewrite") << "Patterns are "; + for( unsigned i=0; i<pattern.size(); i++ ){ + Trace("rr-rewrite") << pattern[i] << " "; + } + Trace("rr-rewrite") << std::endl; + + NodeBuilder<> 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<Node>(patternB); + forallB << static_cast<Node>(patternListB); + Node rn = (Node) forallB; + + return rn; +} + +struct ContainsQuantAttributeId {}; +typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> 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 ); @@ -79,6 +81,10 @@ private: 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<Node>& fvs); +public: //static Node rewriteQuants( Node n, bool isNested = false ); //static Node rewriteQuant( Node n, bool isNested = false ); };/* class QuantifiersRewriter */ 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; j<n.getNumChildren(); j++ ){ RDomain * rf = getRDomain( op, j ); rf->addTerm( 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; i<indicies.size(); i++ ){ - priority_order.push_back( d_rr_quant[indicies[i]] ); + if( e==Theory::EFFORT_FULL ){ + Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl; + //if( e==Theory::EFFORT_LAST_CALL ){ + // if( !d_quantEngine->getModel()->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; i<indicies.size(); i++ ){ + d_priority_order.push_back( d_rr_quant[indicies[i]] ); + } + d_needsSort = false; } //apply rewrite rules @@ -81,16 +88,17 @@ void RewriteEngine::check( Theory::Effort e ) { //per priority level int index = 0; bool success = true; - while( success && index<(int)priority_order.size() ) { - addedLemmas += checkRewriteRule( priority_order[index] ); + while( success && index<(int)d_priority_order.size() ) { + addedLemmas += checkRewriteRule( d_priority_order[index], e ); index++; - if( index<(int)priority_order.size() ){ - success = addedLemmas==0 || getPriority( priority_order[index] )==getPriority( priority_order[index-1] ); + if( index<(int)d_priority_order.size() ){ + success = addedLemmas==0 || getPriority( d_priority_order[index] )==getPriority( d_priority_order[index-1] ); } } - Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl; + Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl; if (addedLemmas==0) { + }else{ //otherwise, the search will continue d_quantEngine->flushLemmas( &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<f[2].getNumChildren(); i++ ){ - Node pat = f[2][i]; - std::vector< Node > nodes; - Trace("rewrite-engine-trigger") << "Trigger is : "; - for( int j=0; j<(int)pat.getNumChildren(); j++ ){ - Node p = d_quantEngine->getTermDatabase()->getInstConstantNode( pat[j], f ); - nodes.push_back( p ); - Trace("rewrite-engine-trigger") << p << " " << p.getKind() << " "; - } - Trace("rewrite-engine-trigger") << std::endl; - Assert( inst::Trigger::isUsableTrigger( nodes, f ) ); - inst::Trigger * tr = inst::Trigger::mkTrigger( d_quantEngine, f, nodes, 0, true, inst::Trigger::TR_MAKE_NEW, false ); - tr->getGenerator()->setActiveAdd(false); - triggers.push_back( tr ); - } - } - d_rr_triggers[f].insert( d_rr_triggers[f].end(), triggers.begin(), triggers.end() ); - } - for( unsigned i=0; i<d_rr_triggers[f].size(); i++ ){ - Trace("rewrite-engine-inst") << "Try trigger " << *d_rr_triggers[f][i] << std::endl; - d_rr_triggers[f][i]->resetInstantiationRound(); - d_rr_triggers[f][i]->reset( Node::null() ); - bool success; - do - { - InstMatch m( 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<f[0].getNumChildren(); i++ ){ + Trace("rewrite-engine-inst-debug") << " " << f[0][i] << " -> "; + if( i<inst.size() ){ + Trace("rewrite-engine-inst-debug") << inst[i] << std::endl; + }else{ + Trace("rewrite-engine-inst-debug") << "OUT_OF_RANGE" << std::endl; + Assert( false ); + } + } + //resize to remove auxiliary variables + if( inst.size()>f[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; i<rr[2][0].getNumChildren(); i++ ){ + to_remove.push_back( rr[2][0][i] ); + } + break; + default: + break; + } + for( unsigned j=0; j<to_remove.size(); j++ ){ + Node ns = d_quantEngine->getSubstitute( 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; a<assigned.size(); a++ ) { + // Trace("rewrite-engine-inst-debug") << assigned[a] << " "; //} + //Trace("rewrite-engine-inst-debug") << std::endl; + //qi->revertMatch( 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<f[0].getNumChildren(); i++ ){ + bvl.push_back( f[0][i] ); + } + + std::vector< Node > 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<f[2].getNumChildren(); i++ ){ + std::vector< Node > nc; + for( unsigned j=0; j<f[2][i].getNumChildren(); j++ ){ + Node nn; + Node nbv = NodeManager::currentNM()->mkBoundVar( 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; j<d_rr[f][1].getNumChildren(); j++ ){ + if( MatchGen::isHandled( d_rr[f][1][j] ) ){ + body_c.push_back( d_rr[f][1][j].negate() ); + } + } + }else if( d_rr[f][1]!=d_true ){ + if( MatchGen::isHandled( d_rr[f][1] ) ){ + body_c.push_back( d_rr[f][1].negate() ); + } + } + //add the patterns to the body + body_c.push_back( cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( 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<Node, bool, NodeHashFunction> NodeBoolMap; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> 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; i<n.getNumChildren(); i++ ){ addTerm( n[i], added, withinQuant ); - if( options::efficientEMatching() ){ - EfficientEMatcher* eem = d_quantEngine->getEfficientEMatcher(); - 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<InstLevelAttributeId, uint64_t> InstLevelAttribute; struct InstVarNumAttributeId {}; typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; -// Attribute that tell if a node have been asserted in this branch -struct AvailableInTermDbId {}; -/** use the special for boolean flag */ -typedef expr::Attribute<AvailableInTermDbId, - bool, - expr::attr::NullCleanupStrategy, - true // context dependent - > AvailableInTermDb; - struct ModelBasisAttributeId {}; typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; //for APPLY_UF terms, 1 : term has direct child with model basis attribute, @@ -60,10 +51,6 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; struct ModelBasisArgAttributeId {}; typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute; -//for rewrite rules -struct QRewriteRuleAttributeId {}; -typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute; - //for bounded integers struct BoundIntLitAttributeId {}; typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> 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<TypeConstant>(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<TypeConstant>(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<bool>(true) ){ + throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); + } + } + return TypeNode(nodeManager->mkTypeConst<TypeConstant>(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<n.getNumChildren(); i++ ){ - Node c = doSubstitute( n[i], terms ); + Node c = getSubstitute( n[i], terms ); cc.push_back( c ); changed = changed || c!=n[i]; } @@ -410,7 +411,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& 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<Node> & 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<Node>::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<Node>::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<bool>(true); - d_false = NodeManager::currentNM()->mkConst<bool>(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<Node> subst; - //AJR: replaced computeTermVec with this - for( size_t i=0; i<r->inst_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<Node> & 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<Guarded>(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<Node>(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<Node>::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<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->theoryOf( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(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<Node>::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<TNode, TNode, TNodeHashFunction> 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<Node> guards; - mutable std::vector<Node> to_remove; /** terms to remove */ - const Node body; - const TNode new_terms; /** new terms included in the body */ - std::vector<Node> free_vars; /* free variable in the rule */ - std::vector<Node> 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<TNode,RewriteRule* > > 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<true> CacheNode; - mutable CacheNode d_cache; - - const bool directrr; - - RewriteRule(TheoryRewriteRules & re, - Trigger & tr, ApplyMatcher * tr2, - std::vector<Node> & g, Node b, TNode nt, - std::vector<Node> & fv,std::vector<Node> & iv, - std::vector<Node> & 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<Node> 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<Node> & 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 T> -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<Node, Trigger > > Rules; - typedef context::CDList< RewriteRule *, - CleanUpPointer<RewriteRule >, - std::allocator< RewriteRule * > > Rules; - Rules d_rules; - typedef context::CDList< RuleInst *, - CleanUpPointer<RuleInst>, - 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<Node, GList *, NodeHashFunction> 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<size_t> d_checkLevel; - - /** explanation */ - typedef context::CDHashMap<Node, RuleInst , NodeHashFunction> 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<Node> & 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<Node> createInstVariable( Node r, std::vector<Node> & 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<TypeConstant>(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<TypeConstant>(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<bool>(true) ){ - throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least"); - } - } - return TypeNode(nodeManager->mkTypeConst<TypeConstant>(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 ); } |