diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-02-20 09:45:46 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-03-11 11:29:45 -0500 |
| commit | 38d149261763e5f2f65abb21c2b647f2befa7807 (patch) | |
| tree | 51c3019eff61c7f3702f3dc888fb88d3a714f68a /src/theory/quantifiers | |
| parent | 3ed865aa12a94e935038d70b130701045b84a8b8 (diff) | |
Initial refactor of rewrite rules, make theory_rewriterules empty theory. Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.
Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.
QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master.
Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.
Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE.
Merging rewrite rules into master, check-model current fails on 3 FMF regressions.
Fix check-model issue, a line of code was omitted during merge.
Diffstat (limited to 'src/theory/quantifiers')
26 files changed, 1241 insertions, 564 deletions
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 */ |