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.
theory/quantifiers/quant_conflict_find.h \
theory/quantifiers/quant_conflict_find.cpp \
theory/quantifiers/options_handlers.h \
- theory/rewriterules/theory_rewriterules_rules.h \
- theory/rewriterules/theory_rewriterules_rules.cpp \
theory/rewriterules/theory_rewriterules.h \
theory/rewriterules/theory_rewriterules.cpp \
- theory/rewriterules/theory_rewriterules_rewriter.h \
- theory/rewriterules/theory_rewriterules_type_rules.h \
- theory/rewriterules/theory_rewriterules_preprocess.h \
- theory/rewriterules/theory_rewriterules_params.h \
- theory/rewriterules/rr_inst_match.h \
- theory/rewriterules/rr_inst_match_impl.h \
- theory/rewriterules/rr_inst_match.cpp \
- theory/rewriterules/rr_trigger.h \
- theory/rewriterules/rr_trigger.cpp \
- theory/rewriterules/rr_candidate_generator.h \
- theory/rewriterules/rr_candidate_generator.cpp \
- theory/rewriterules/efficient_e_matching.h \
- theory/rewriterules/efficient_e_matching.cpp \
theory/arith/theory_arith_type_rules.h \
theory/arith/type_enumerator.h \
theory/arith/arithvar.h \
#include "util/sort_inference.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/macros.h"
-#include "theory/datatypes/options.h"
#include "theory/quantifiers/first_order_reasoning.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/options.h"
+#include "theory/datatypes/options.h"
#include "theory/strings/theory_strings_preprocess.h"
using namespace std;
return applySubstitutions(n).toExpr();
}
- /**
- * Pre-skolemize quantifiers.
- */
- Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs);
-
/**
* Substitute away all AbstractValues in a node.
*/
//instantiate only on last call
if( options::fmfInstEngine() ){
Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
- options::instWhenMode.set( INST_WHEN_LAST_CALL );
+ options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL );
}
}
if ( options::fmfBoundInt() ){
return result.top();
}
-
-struct ContainsQuantAttributeId {};
-typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute;
-
-// check if the given node contains a universal quantifier
-static bool containsQuantifiers(Node n) {
- if( n.hasAttribute(ContainsQuantAttribute()) ){
- return n.getAttribute(ContainsQuantAttribute())==1;
- } else if(n.getKind() == kind::FORALL) {
- return true;
- } else {
- bool cq = false;
- for( unsigned i = 0; i < n.getNumChildren(); ++i ){
- if( containsQuantifiers(n[i]) ){
- cq = true;
- break;
- }
- }
- ContainsQuantAttribute cqa;
- n.setAttribute(cqa, cq ? 1 : 0);
- return cq;
- }
-}
-
-Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
- Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
- if( n.getKind()==kind::NOT ){
- Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs );
- return nn.negate();
- }else if( n.getKind()==kind::FORALL ){
- if( polarity ){
- vector< Node > children;
- children.push_back( n[0] );
- //add children to current scope
- vector< Node > fvss;
- fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
- for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
- fvss.push_back( n[0][i] );
- }
- //process body
- children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) );
- if( n.getNumChildren()==3 ){
- children.push_back( n[2] );
- }
- //return processed quantifier
- return NodeManager::currentNM()->mkNode( kind::FORALL, children );
- }else{
- //process body
- Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs );
- //now, substitute skolems for the variables
- vector< TypeNode > argTypes;
- for( int i=0; i<(int)fvs.size(); i++ ){
- argTypes.push_back( fvs[i].getType() );
- }
- //calculate the variables and substitution
- vector< Node > vars;
- vector< Node > subs;
- for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
- vars.push_back( n[0][i] );
- }
- for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
- //make the new function symbol
- if( argTypes.empty() ){
- Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" );
- subs.push_back( s );
- }else{
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
- Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
- //DOTHIS: set attribute on op, marking that it should not be selected as trigger
- vector< Node > funcArgs;
- funcArgs.push_back( op );
- funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );
- subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) );
- }
- }
- //apply substitution
- nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- return nn;
- }
- }else{
- //check if it contains a quantifier as a subterm
- //if so, we will write this node
- if( containsQuantifiers( n ) ){
- if( n.getType().isBoolean() ){
- if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
- Node nn;
- //must remove structure
- if( n.getKind()==kind::ITE ){
- nn = NodeManager::currentNM()->mkNode( kind::AND,
- NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
- NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
- }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
- nn = NodeManager::currentNM()->mkNode( kind::AND,
- NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
- NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
- }else if( n.getKind()==kind::IMPLIES ){
- nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
- }
- return preSkolemizeQuantifiers( nn, polarity, fvs );
- }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
- vector< Node > children;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
- }
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
- }else{
- //must pull ite's
- }
- }
- }
- return n;
- }
-}
-
void SmtEnginePrivate::removeITEs() {
d_smt.finalOptionsAreSet();
dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
}
if( d_smt.d_logic.isQuantified() ){
+ //remove rewrite rules
+ for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) {
+ if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){
+ Node prev = d_assertionsToPreprocess[i];
+ Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl;
+ d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) );
+ Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl;
+ Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
+ }
+ }
+
dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
if( options::preSkolemQuant() ){
//apply pre-skolemization to existential quantifiers
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
Node prev = d_assertionsToPreprocess[i];
+ Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
vector< Node > fvs;
- d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) );
+ d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvs ) );
if( prev!=d_assertionsToPreprocess[i] ){
Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl;
//quantifiers macro expansion
bool success;
do{
- QuantifierMacros qm;
+ quantifiers::QuantifierMacros qm;
success = qm.simplify( d_assertionsToPreprocess, true );
}while( success );
}
Trace("fo-rsn-enable") << std::endl;
if( options::foPropQuant() ){
- FirstOrderPropagation fop;
+ quantifiers::FirstOrderPropagation fop;
fop.simplify( d_assertionsToPreprocess );
}
}
Debug("boolean-terms") << "++ got " << n << endl;
Notice() << "SmtEngine::checkModel(): -- substitutes to " << n << endl;
- if(Theory::theoryOf(n) != THEORY_REWRITERULES) {
+ //AJR : FIXME need to ignore quantifiers too?
+ if( n.getKind() != kind::REWRITE_RULE ){
// In case it's a quantifier (or contains one), look up its value before
// simplifying, or the quantifier might be irreparably altered.
n = m->getValue(n);
- }
-
- // Simplify the result.
- n = d_private->simplify(n);
- Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl;
-
- TheoryId thy = Theory::theoryOf(n);
- if(thy == THEORY_REWRITERULES) {
+ } else {
// Note this "skip" is done here, rather than above. This is
// because (1) the quantifier could in principle simplify to false,
// which should be reported, and (2) checking for the quantifier
// above, before simplification, doesn't catch buried quantifiers
// anyway (those not at the top-level).
- Notice() << "SmtEngine::checkModel(): -- skipping rewrite-rules assertion"
+ Notice() << "SmtEngine::checkModel(): -- skipping quantifiers/rewrite-rules assertion"
<< endl;
continue;
}
+ // Simplify the result.
+ n = d_private->simplify(n);
+ Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl;
+
// Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
n = d_private->d_iteRemover.replace(n);
Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
#include "theory/theory_model.h"
#include "theory/arith/options.h"
+#include "theory/quantifiers/options.h"
+
#include "theory/quantifiers/bounded_integers.h"
}
ConstraintP c = d_constraintDatabase.lookup(n);
Assert(c != NullConstraint);
-
+
Debug("arith::preregister") << "setup constraint" << c << endl;
Assert(!c->canBePropagated());
c->setPreregistered();
#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;
#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;
#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
#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 ){
return NodeManager::currentNM()->mkNode( n.getKind(), children );
}
}
-
-}
#include "expr/type_node.h"
namespace CVC4 {
+namespace theory {
+namespace quantifiers {
class FirstOrderPropagation {
private:
void simplify( std::vector< Node >& assertions );
};
+}
+}
}
#endif
#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;
#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
#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;
//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
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 );
}
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] );
+ }
}
}
}
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
#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;
}
bool QModelBuilder::isQuantifierActive( Node f ) {
- return !f.hasAttribute(QRewriteRuleAttribute());
+ return !TermDb::isRewriteRule( f );
}
}
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();
}
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
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\
\r
\r
#include "theory/quantifiers/qinterval_builder.h"\r
+#include "theory/quantifiers/term_database.h"\r
+\r
\r
using namespace std;\r
using namespace CVC4;\r
#include "theory/quantifiers/quant_conflict_find.h"\r
#include "theory/quantifiers/quant_util.h"\r
#include "theory/theory_engine.h"\r
+#include "theory/quantifiers/options.h"\r
+#include "theory/quantifiers/term_database.h"\r
\r
using namespace CVC4;\r
using namespace CVC4::kind;\r
std::vector< int > bvars;\r
d_mg->determineVariableOrder( this, bvars );\r
}\r
-\r
- //must also contain all variables?\r
- if( d_isPartial ){\r
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
- if( d_has_var.find( q[0][i] )==d_has_var.end() ){\r
- d_isPartial = false;\r
- d_mg->setInvalid();\r
- break;\r
- }\r
- }\r
- }\r
}\r
- Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? ( isPartial() ? "PARTIAL " : "VALID " ) : "INVALID" ) << " : " << q << std::endl;\r
+ Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;\r
}\r
\r
void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {\r
Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;\r
if( n.getKind()==FORALL ){\r
registerNode( n[1], hasPol, pol, true );\r
- }else{\r
- if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){\r
+ }else{
+ if( !MatchGen::isHandledBoolConnective( n ) ){\r
if( n.hasBoundVar() ){\r
//literals\r
if( n.getKind()==EQUAL ){\r
}\r
}else if( MatchGen::isHandledUfTerm( n ) ){\r
flatten( n, beneathQuant );\r
- }else if( n.getKind()==ITE ){\r
- if( !n[1].getType().isBoolean() ){\r
- for( unsigned i=1; i<=2; i++ ){\r
- flatten( n[i], beneathQuant );\r
- }\r
+ }else if( n.getKind()==ITE ){
+ for( unsigned i=1; i<=2; i++ ){\r
+ flatten( n[i], beneathQuant );\r
}\r
}\r
}\r
for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){\r
it->second->reset_round( p );\r
}\r
+ //now, reset for matching\r
+ d_mg->reset( p, false, this );\r
}\r
\r
int QuantInfo::getCurrentRepVar( int v ) {\r
}\r
}\r
\r
+TNode QuantInfo::getCurrentExpValue( TNode n ) {\r
+ int v = getVarNum( n );\r
+ if( v==-1 ){\r
+ return n;\r
+ }else{\r
+ if( d_match[v].isNull() ){\r
+ return n;\r
+ }else{\r
+ Assert( getVarNum( d_match[v] )!=v );\r
+ if( d_match_term[v].isNull() ){\r
+ return getCurrentValue( d_match[v] );\r
+ }else{\r
+ return d_match_term[v];\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {\r
//check disequalities\r
std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );\r
return false;\r
}\r
\r
-bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned ) {\r
+bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {\r
//assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
- Trace("qcf-check") << std::endl;\r
- std::vector< int > unassigned[2];\r
- std::vector< TypeNode > unassigned_tn[2];\r
- for( int i=0; i<getNumVars(); i++ ){\r
- if( d_match[i].isNull() ){\r
- //Assert( i<(int)q[0].getNumChildren() );\r
- int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
- unassigned[rindex].push_back( i );\r
- unassigned_tn[rindex].push_back( getVar( i ).getType() );\r
- assigned.push_back( i );\r
+ bool doFail = false;\r
+ bool success = true;\r
+ if( doContinue ){\r
+ doFail = true;\r
+ success = false;\r
+ }else{\r
+ d_unassigned.clear();\r
+ d_unassigned_tn.clear();\r
+ std::vector< int > unassigned[2];\r
+ std::vector< TypeNode > unassigned_tn[2];\r
+ for( int i=0; i<getNumVars(); i++ ){\r
+ if( d_match[i].isNull() ){\r
+ int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
+ unassigned[rindex].push_back( i );\r
+ unassigned_tn[rindex].push_back( getVar( i ).getType() );\r
+ assigned.push_back( i );\r
+ }\r
+ }\r
+ d_unassigned_nvar = unassigned[0].size();\r
+ for( unsigned i=0; i<2; i++ ){\r
+ d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );\r
+ d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );\r
}\r
+ d_una_eqc_count.clear();\r
+ d_una_index = 0;\r
}\r
- bool success = true;\r
- for( unsigned r=0; r<2; r++ ){\r
- if( success && !unassigned[r].empty() ){\r
- Trace("qcf-check") << "Assign to unassigned, rep = " << r << "..." << std::endl;\r
- int index = 0;\r
- std::vector< int > eqc_count;\r
- bool doFail = false;\r
- do {\r
- if( doFail ){\r
- Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;\r
- }\r
- bool invalidMatch = false;\r
- while( ( index>=0 && (int)index<(int)unassigned[r].size() ) || invalidMatch || doFail ){\r
- invalidMatch = false;\r
- if( !doFail && index==(int)eqc_count.size() ){\r
- //check if it has now been assigned\r
- if( r==0 ){\r
- if( !isConstrainedVar( unassigned[r][index] ) ){\r
- eqc_count.push_back( -1 );\r
- }else{\r
- d_var_mg[ unassigned[r][index] ]->reset( p, true, this );\r
- eqc_count.push_back( 0 );\r
- }\r
+ if( !d_unassigned.empty() ){\r
+ Trace("qcf-check") << "Assign to unassigned..." << std::endl;\r
+ do {\r
+ if( doFail ){\r
+ Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;\r
+ }\r
+ bool invalidMatch = false;\r
+ while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){\r
+ invalidMatch = false;\r
+ if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){\r
+ //check if it has now been assigned\r
+ if( d_una_index<d_unassigned_nvar ){\r
+ if( !isConstrainedVar( d_unassigned[d_una_index] ) ){\r
+ d_una_eqc_count.push_back( -1 );\r
}else{\r
- eqc_count.push_back( 0 );\r
+ d_var_mg[ d_unassigned[d_una_index] ]->reset( p, true, this );\r
+ d_una_eqc_count.push_back( 0 );\r
}\r
}else{\r
- if( r==0 ){\r
- if( !doFail && !isConstrainedVar( unassigned[r][index] ) ){\r
- Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << index << std::endl;\r
- index++;\r
- }else if( !doFail && d_var_mg[unassigned[r][index]]->getNextMatch( p, this ) ){\r
- Trace("qcf-check-unassign") << "Succeeded match with mg at " << index << std::endl;\r
- index++;\r
+ d_una_eqc_count.push_back( 0 );\r
+ }\r
+ }else{\r
+ bool failed = false;\r
+ if( !doFail ){\r
+ if( d_una_index<d_unassigned_nvar ){\r
+ if( !isConstrainedVar( d_unassigned[d_una_index] ) ){\r
+ Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;\r
+ d_una_index++;\r
+ }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( p, this ) ){\r
+ Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;\r
+ d_una_index++;\r
}else{\r
- Trace("qcf-check-unassign") << "Failed match with mg at " << index << std::endl;\r
- do{\r
- if( !doFail ){\r
- eqc_count.pop_back();\r
- }else{\r
- doFail = false;\r
- }\r
- index--;\r
- }while( index>=0 && eqc_count[index]==-1 );\r
+ failed = true;\r
+ Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;\r
}\r
}else{\r
- Assert( doFail || index==(int)eqc_count.size()-1 );\r
- if( !doFail && eqc_count[index]<(int)p->d_eqcs[unassigned_tn[r][index]].size() ){\r
- int currIndex = eqc_count[index];\r
- eqc_count[index]++;\r
- Trace("qcf-check-unassign") << unassigned[r][index] << "->" << p->d_eqcs[unassigned_tn[r][index]][currIndex] << std::endl;\r
- if( setMatch( p, unassigned[r][index], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) ){\r
- //if( currIndex==0 ){\r
- // Assert( p->areEqual( p->d_model_basis[unassigned_tn[r][index]], p->d_eqcs[unassigned_tn[r][index]][currIndex] ) );\r
- // d_match_term[unassigned[r][index]] = p->d_model_basis[unassigned_tn[r][index]];\r
- //}else{\r
- d_match_term[unassigned[r][index]] = TNode::null();\r
- //}\r
- Trace("qcf-check-unassign") << "Succeeded match " << index << std::endl;\r
- index++;\r
+ Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 );\r
+ if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){\r
+ int currIndex = d_una_eqc_count[d_una_index];\r
+ d_una_eqc_count[d_una_index]++;\r
+ Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;\r
+ if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){\r
+ d_match_term[d_unassigned[d_una_index]] = TNode::null();\r
+ Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;\r
+ d_una_index++;\r
}else{\r
- Trace("qcf-check-unassign") << "Failed match " << index << std::endl;\r
+ Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;\r
invalidMatch = true;\r
}\r
}else{\r
- Trace("qcf-check-unassign") << "No more matches " << index << std::endl;\r
- if( !doFail ){\r
- eqc_count.pop_back();\r
- }else{\r
- doFail = false;\r
- }\r
- index--;\r
+ failed = true;\r
+ Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;\r
}\r
}\r
}\r
+ if( doFail || failed ){\r
+ do{\r
+ if( !doFail ){\r
+ d_una_eqc_count.pop_back();\r
+ }else{\r
+ doFail = false;\r
+ }\r
+ d_una_index--;\r
+ }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 );\r
+ }\r
}\r
- success = index>=0;\r
- if( success ){\r
- doFail = true;\r
- Trace("qcf-check-unassign") << " Try: " << std::endl;\r
- for( unsigned i=0; i<unassigned[r].size(); i++ ){\r
- int ui = unassigned[r][i];\r
- if( !d_match[ui].isNull() ){\r
- Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
- }\r
+ }\r
+ success = d_una_index>=0;\r
+ if( success ){\r
+ doFail = true;\r
+ Trace("qcf-check-unassign") << " Try: " << std::endl;\r
+ for( unsigned i=0; i<d_unassigned.size(); i++ ){\r
+ int ui = d_unassigned[i];\r
+ if( !d_match[ui].isNull() ){\r
+ Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
}\r
}\r
- }while( success && isMatchSpurious( p ) );\r
- }\r
+ }\r
+ }while( success && isMatchSpurious( p ) );\r
}\r
if( success ){\r
return true;\r
}\r
}\r
\r
+void QuantInfo::getMatch( std::vector< Node >& terms ){\r
+ for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){\r
+ //Node cv = qi->getCurrentValue( qi->d_match[i] );\r
+ int repVar = getCurrentRepVar( i );\r
+ Node cv;\r
+ //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );\r
+ if( !d_match_term[repVar].isNull() ){\r
+ cv = d_match_term[repVar];\r
+ }else{\r
+ cv = d_match[repVar];\r
+ }\r
+ Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;\r
+ terms.push_back( cv );\r
+ }\r
+}\r
+\r
+void QuantInfo::revertMatch( std::vector< int >& assigned ) {\r
+ for( unsigned i=0; i<assigned.size(); i++ ){\r
+ d_match[ assigned[i] ] = TNode::null();\r
+ }\r
+}\r
+\r
void QuantInfo::debugPrintMatch( const char * c ) {\r
for( int i=0; i<getNumVars(); i++ ){\r
Trace(c) << " " << d_vars[i] << " -> ";\r
}\r
Trace(c) << "}";\r
}\r
- Trace(c) << std::endl;\r
+ if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){\r
+ Trace(c) << ", EXP : " << d_match_term[i];\r
+ }\r
+ Trace(c) << std::endl;\r
}\r
}\r
\r
Trace("qcf-qregister-debug") << " is var #" << v << std::endl;\r
d_qni_var_num[d_qni_size] = v;\r
//qi->addFuncParent( v, f, j );\r
- if( nn.getKind()==BOUND_VARIABLE && !beneathQuant ){\r
- qi->d_has_var[nn] = true;\r
- }\r
}else{\r
Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
d_qni_gterm[d_qni_size] = nn;\r
d_type_not = !d_type_not;\r
}\r
\r
- if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE || d_n.getKind()==FORALL ){\r
+ if( isHandledBoolConnective( d_n ) ){\r
//non-literals\r
d_type = typ_formula;\r
bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;\r
if( d_n[i].hasBoundVar() ){\r
if( !qi->isVar( d_n[i] ) ){\r
Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;\r
- }else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){\r
- qi->d_has_var[d_n[i]] = true;\r
}\r
Assert( qi->isVar( d_n[i] ) );\r
}else{\r
}else if( isHandledUfTerm( d_n ) ){\r
Assert( qi->isVar( d_n ) );\r
d_type = typ_pred;\r
+ }else if( d_n.getKind()==BOUND_VARIABLE ){\r
+ d_type = typ_bool_var;\r
}else{\r
Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;\r
}\r
Trace("qcf-qregister-debug") << std::endl;\r
//Assert( d_children.size()==d_children_order.size() );\r
\r
- if( !isValid() && options::qcfMode()>=QCF_PARTIAL ){\r
- qi->d_isPartial = true;\r
- }\r
}\r
\r
void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {\r
\r
\r
void MatchGen::reset_round( QuantConflictFind * p ) {\r
+ d_wasSet = false;\r
for( unsigned i=0; i<d_children.size(); i++ ){\r
d_children[i].reset_round( p );\r
}\r
}\r
}\r
}\r
+ d_qni_bound_cons.clear();\r
+ d_qni_bound_cons_var.clear();\r
+ d_qni_bound.clear();\r
}\r
\r
void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {\r
d_qni.clear();\r
d_qni_bound.clear();\r
d_child_counter = -1;\r
+ d_tgt_orig = d_tgt;\r
\r
//set up processing matches\r
if( d_type==typ_invalid ){\r
if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){\r
d_child_counter = 0;\r
}\r
+ }else if( d_type==typ_bool_var ){\r
+ //get current value of the variable\r
+ TNode n = qi->getCurrentValue( d_n );\r
+ int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );\r
+ if( vn==-1 ){\r
+ //evaluate the value, see if it is compatible\r
+ int e = p->evaluate( n );\r
+ if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){\r
+ d_child_counter = 0;\r
+ }\r
+ }else{\r
+ //unassigned, set match to true/false\r
+ d_qni_bound[0] = vn;\r
+ qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );\r
+ d_child_counter = 0;\r
+ }\r
+ if( d_child_counter==0 ){\r
+ d_qn.push_back( NULL );\r
+ }\r
}else if( d_type==typ_var ){\r
Assert( isHandledUfTerm( d_n ) );\r
Node f = getOperator( p, d_n );\r
}\r
bool success;\r
if( vn[0]==-1 && vn[1]==-1 ){\r
+ //Trace("qcf-explain") << " reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;\r
Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;\r
//just compare values\r
if( d_tgt ){\r
success = addc!=-1;\r
//if successful and non-redundant, store that we need to cleanup this\r
if( addc==1 ){\r
+ //Trace("qcf-explain") << " reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;\r
for( unsigned i=0; i<2; i++ ){\r
if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){\r
d_qni_bound[vn[i]] = vn[i];\r
}\r
}\r
d_binding = false;\r
+ d_wasSet = true;\r
Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;\r
}\r
\r
d_child_counter = -1;\r
return true;\r
}else{\r
+ d_wasSet = false;\r
return false;\r
}\r
- }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred ){\r
+ }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){\r
bool success = false;\r
bool terminate = false;\r
do {\r
Debug("qcf-match-debug") << " failed." << std::endl;\r
success = false;\r
}else{\r
- Debug("qcf-match-debug") << " decrement..." << std::endl;\r
--d_binding_it;\r
+ Debug("qcf-match-debug") << " decrement..." << std::endl;\r
}\r
}while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );\r
doReset = false;\r
Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;\r
std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );\r
int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;\r
+ //Trace("qcf-explain") << " cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl;\r
qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );\r
}\r
}\r
*/\r
}\r
Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;\r
+ d_wasSet = success;\r
return success;\r
}else if( d_type==typ_formula || d_type==typ_ite_var ){\r
bool success = false;\r
}else{\r
while( !success && d_child_counter>=0 ){\r
//transition system based on d_child_counter\r
- if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){\r
+ if( d_n.getKind()==OR || d_n.getKind()==AND ){\r
if( (d_n.getKind()==AND)==d_tgt ){\r
//all children must match simultaneously\r
if( getChild( d_child_counter )->getNextMatch( p, qi ) ){\r
}\r
}\r
}\r
+ d_wasSet = success;\r
Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;\r
return success;\r
}\r
return false;\r
}\r
\r
+bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) {\r
+ if( d_type==typ_eq ){\r
+ Node n[2];\r
+ for( unsigned i=0; i<2; i++ ){\r
+ Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl;\r
+ n[i] = getExplanationTerm( p, qi, d_n[i], exp );\r
+ }\r
+ Node eq = n[0].eqNode( n[1] );\r
+ if( !d_tgt_orig ){\r
+ eq = eq.negate();\r
+ }\r
+ exp.push_back( eq );\r
+ Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl;\r
+ return true;\r
+ }else if( d_type==typ_pred ){\r
+ Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl;\r
+ Node n = getExplanationTerm( p, qi, d_n, exp );\r
+ if( !d_tgt_orig ){\r
+ n = n.negate();\r
+ }\r
+ exp.push_back( n );\r
+ Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl;\r
+ return true;\r
+ }else if( d_type==typ_formula ){\r
+ Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl;\r
+ if( d_n.getKind()==OR || d_n.getKind()==AND ){\r
+ if( (d_n.getKind()==AND)==d_tgt ){\r
+ for( unsigned i=0; i<getNumChildren(); i++ ){\r
+ if( !getChild( i )->getExplanation( p, qi, exp ) ){\r
+ return false;\r
+ }\r
+ }\r
+ }else{\r
+ return getChild( d_child_counter )->getExplanation( p, qi, exp );\r
+ }\r
+ }else if( d_n.getKind()==IFF ){\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( !getChild( i )->getExplanation( p, qi, exp ) ){\r
+ return false;\r
+ }\r
+ }\r
+ }else if( d_n.getKind()==ITE ){\r
+ for( unsigned i=0; i<3; i++ ){\r
+ bool isActive = ( ( i==0 && d_child_counter!=5 ) ||\r
+ ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) ||\r
+ ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) );\r
+ if( isActive ){\r
+ if( !getChild( i )->getExplanation( p, qi, exp ) ){\r
+ return false;\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ return false;\r
+ }\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) {\r
+ Node v = qi->getCurrentExpValue( t );\r
+ if( isHandledUfTerm( t ) ){\r
+ for( unsigned i=0; i<t.getNumChildren(); i++ ){\r
+ Node vi = getExplanationTerm( p, qi, t[i], exp );\r
+ if( vi!=v[i] ){\r
+ Node eq = vi.eqNode( v[i] );\r
+ if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){\r
+ Trace("qcf-explain") << " add : " << eq << "." << std::endl;\r
+ exp.push_back( eq );\r
+ }\r
+ }\r
+ }\r
+ }\r
+ return v;\r
+}\r
+\r
bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {\r
if( !d_qn.empty() ){\r
if( d_qn[0]==NULL ){\r
Assert( !d_qni[d_qni.size()-1]->second.d_children.empty() );\r
TNode t = d_qni[d_qni.size()-1]->second.d_children.begin()->first;\r
Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl;\r
+ qi->d_match_term[d_qni_var_num[0]] = t;\r
//set the match terms\r
for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;\r
- 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\r
+ //if( it->second<(int)qi->d_q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term\r
+ if( it->first>0 ){\r
Assert( !qi->d_match[ it->second ].isNull() );\r
Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );\r
qi->d_match_term[it->second] = t[it->first-1];\r
}\r
+ //}\r
}\r
}\r
}\r
case typ_formula: Trace(c) << "formula";break;\r
case typ_var: Trace(c) << "var";break;\r
case typ_ite_var: Trace(c) << "ite_var";break;\r
- case typ_top: Trace(c) << "top";break;\r
+ case typ_bool_var: Trace(c) << "bool_var";break;\r
}\r
}else{\r
switch( typ ){\r
case typ_formula: Debug(c) << "formula";break;\r
case typ_var: Debug(c) << "var";break;\r
case typ_ite_var: Debug(c) << "ite_var";break;\r
- case typ_top: Debug(c) << "top";break;\r
+ case typ_bool_var: Debug(c) << "bool_var";break;\r
}\r
}\r
}\r
d_children.clear();\r
}\r
\r
+bool MatchGen::isHandledBoolConnective( TNode n ) {\r
+ return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );\r
+}\r
+\r
bool MatchGen::isHandledUfTerm( TNode n ) {\r
- return n.getKind()==APPLY_UF;// || n.getKind()==GEQ;\r
+ return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||\r
+ n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;\r
}\r
\r
Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {\r
if( isHandledUfTerm( n ) ){\r
- return n.getOperator();\r
+ return p->getQuantifiersEngine()->getTermDatabase()->getOperator( n );\r
}else{\r
return Node::null();\r
}\r
}\r
\r
+bool MatchGen::isHandled( TNode n ) {\r
+ if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){\r
+ if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){\r
+ return false;\r
+ }\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ if( !isHandled( n[i] ) ){\r
+ return false;\r
+ }\r
+ }\r
+ }\r
+ return true;\r
+}\r
+\r
\r
QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :\r
QuantifiersModule( qe ),\r
//-------------------------------------------------- registration\r
\r
void QuantConflictFind::registerQuantifier( Node q ) {\r
- d_quants.push_back( q );\r
- d_quant_id[q] = d_quants.size();\r
- Trace("qcf-qregister") << "Register ";\r
- debugPrintQuant( "qcf-qregister", q );\r
- Trace("qcf-qregister") << " : " << q << std::endl;\r
- //make QcfNode structure\r
- Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;\r
- d_qinfo[q].initialize( q, q[1] );\r
-\r
- //debug print\r
- Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
- Trace("qcf-qregister") << " ";\r
- debugPrintQuantBody( "qcf-qregister", q, q[1] );\r
- Trace("qcf-qregister") << std::endl;\r
- if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
- Trace("qcf-qregister") << " with additional constraints : " << std::endl;\r
- for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
- Trace("qcf-qregister") << " ?x" << j << " = ";\r
- debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );\r
- Trace("qcf-qregister") << std::endl;\r
+ if( !TermDb::isRewriteRule( q ) ){\r
+ d_quants.push_back( q );\r
+ d_quant_id[q] = d_quants.size();\r
+ Trace("qcf-qregister") << "Register ";\r
+ debugPrintQuant( "qcf-qregister", q );\r
+ Trace("qcf-qregister") << " : " << q << std::endl;\r
+ //make QcfNode structure\r
+ Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;\r
+ d_qinfo[q].initialize( q, q[1] );\r
+\r
+ //debug print\r
+ Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
+ Trace("qcf-qregister") << " ";\r
+ debugPrintQuantBody( "qcf-qregister", q, q[1] );\r
+ Trace("qcf-qregister") << std::endl;\r
+ if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
+ Trace("qcf-qregister") << " with additional constraints : " << std::endl;\r
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
+ Trace("qcf-qregister") << " ?x" << j << " = ";\r
+ debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );\r
+ Trace("qcf-qregister") << std::endl;\r
+ }\r
}\r
- }\r
\r
- Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
+ Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
+ }\r
}\r
\r
int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {\r
return ret;\r
}\r
\r
+short QuantConflictFind::getMaxQcfEffort() {\r
+ if( options::qcfMode()==QCF_CONFLICT_ONLY ){\r
+ return effort_conflict;\r
+ }else if( options::qcfMode()==QCF_PROP_EQ ){\r
+ return effort_prop_eq;\r
+ }else if( options::qcfMode()==QCF_PARTIAL ){\r
+ return effort_partial;\r
+ }else if( options::qcfMode()==QCF_MC ){\r
+ return effort_mc;\r
+ }else{\r
+ return 0;\r
+ }\r
+}\r
+\r
bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {\r
//if( d_effort==QuantConflictFind::effort_mc ){\r
// return n1==n2 || !areDisequal( n1, n2 );\r
//-------------------------------------------------- handling assertions / eqc\r
\r
void QuantConflictFind::assertNode( Node q ) {\r
- Trace("qcf-proc") << "QCF : assertQuantifier : ";\r
- debugPrintQuant("qcf-proc", q);\r
- Trace("qcf-proc") << std::endl;\r
- d_qassert.push_back( q );\r
- //set the eqRegistries that this depends on to true\r
- //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){\r
- // it->first->d_active.set( true );\r
- //}\r
+ if( !TermDb::isRewriteRule( q ) ){\r
+ Trace("qcf-proc") << "QCF : assertQuantifier : ";\r
+ debugPrintQuant("qcf-proc", q);\r
+ Trace("qcf-proc") << std::endl;\r
+ d_qassert.push_back( q );\r
+ //set the eqRegistries that this depends on to true\r
+ //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){\r
+ // it->first->d_active.set( true );\r
+ //}\r
+ }\r
}\r
\r
eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {\r
return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );\r
}\r
bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {\r
- return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );\r
+ return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );\r
}\r
Node QuantConflictFind::getRepresentative( Node n ) {\r
if( getEqualityEngine()->hasTerm( n ) ){\r
\r
//-------------------------------------------------- check function\r
\r
+void QuantConflictFind::reset_round( Theory::Effort level ) {\r
+ d_needs_computeRelEqr = true;\r
+}\r
+\r
/** check */\r
void QuantConflictFind::check( Theory::Effort level ) {\r
Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
clSet = double(clock())/double(CLOCKS_PER_SEC);\r
Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;\r
}\r
- Trace("qcf-check") << "Compute relevant equalities..." << std::endl;\r
computeRelevantEqr();\r
\r
//determine order for quantified formulas\r
Trace("qcf-debug") << std::endl;\r
debugPrint("qcf-debug");\r
Trace("qcf-debug") << std::endl;\r
- }\r
- short end_e;\r
- if( options::qcfMode()==QCF_CONFLICT_ONLY ){\r
- end_e = effort_conflict;\r
- }else if( options::qcfMode()==QCF_PROP_EQ ){\r
- end_e = effort_prop_eq;\r
- }else if( options::qcfMode()==QCF_PARTIAL ){\r
- end_e = effort_partial;\r
- }else{\r
- end_e = effort_mc;\r
- }\r
+ }
+ short end_e = getMaxQcfEffort();\r
for( short e = effort_conflict; e<=end_e; e++ ){\r
d_effort = e;\r
Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;\r
\r
Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
if( qi->d_mg->isValid() ){\r
- if( qi->isPartial()==(e==effort_partial) ){\r
- Trace("qcf-check") << "Check quantified formula ";\r
- debugPrintQuant("qcf-check", q);\r
- Trace("qcf-check") << " : " << q << "..." << std::endl;\r
-\r
- Trace("qcf-check-debug") << "Reset round..." << std::endl;\r
- qi->reset_round( this );\r
- //try to make a matches making the body false\r
- Trace("qcf-check-debug") << "Reset..." << std::endl;\r
- qi->d_mg->reset( this, false, qi );\r
- Trace("qcf-check-debug") << "Get next match..." << std::endl;\r
- while( qi->d_mg->getNextMatch( this, qi ) ){\r
-\r
- Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r
- qi->debugPrintMatch("qcf-check");\r
- Trace("qcf-check") << std::endl;\r
-\r
- if( !qi->isMatchSpurious( this ) ){\r
- std::vector< int > assigned;\r
- if( qi->completeMatch( this, assigned ) ){\r
- std::vector< Node > terms;\r
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
- //Node cv = qi->getCurrentValue( qi->d_match[i] );\r
- int repVar = qi->getCurrentRepVar( i );\r
- Node cv;\r
- //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );\r
- if( !qi->d_match_term[repVar].isNull() ){\r
- cv = qi->d_match_term[repVar];\r
- }else{\r
- cv = qi->d_match[repVar];\r
+ Trace("qcf-check") << "Check quantified formula ";\r
+ debugPrintQuant("qcf-check", q);\r
+ Trace("qcf-check") << " : " << q << "..." << std::endl;\r
+\r
+ Trace("qcf-check-debug") << "Reset round..." << std::endl;\r
+ qi->reset_round( this );\r
+ //try to make a matches making the body false\r
+ Trace("qcf-check-debug") << "Get next match..." << std::endl;\r
+ while( qi->d_mg->getNextMatch( this, qi ) ){\r
+ Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;\r
+ qi->debugPrintMatch("qcf-check");\r
+ Trace("qcf-check") << std::endl;\r
+ std::vector< int > assigned;\r
+ if( !qi->isMatchSpurious( this ) ){\r
+ if( qi->completeMatch( this, assigned ) ){\r
+ /*\r
+ if( options::qcfExp() && d_effort==effort_conflict ){\r
+ std::vector< Node > exp;\r
+ if( qi->d_mg->getExplanation( this, qi, exp ) ){\r
+ Trace("qcf-check-exp") << "Base explanation is : " << std::endl;\r
+ for( unsigned c=0; c<exp.size(); c++ ){\r
+ Trace("qcf-check-exp") << " " << exp[c] << std::endl;\r
}\r
- Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << qi->d_match[i] << std::endl;\r
- terms.push_back( cv );\r
- }\r
- if( Debug.isOn("qcf-check-inst") ){\r
- //if( e==effort_conflict ){\r
- Node inst = d_quantEngine->getInstantiation( q, terms );\r
- Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
- Assert( evaluate( inst )!=1 );\r
- Assert( evaluate( inst )==-1 || e>effort_conflict );\r
- //}\r
- }\r
- if( d_quantEngine->addInstantiation( q, terms ) ){\r
- Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
- ++addedLemmas;\r
- if( e==effort_conflict ){\r
- d_quant_order.insert( d_quant_order.begin(), q );\r
- d_conflict.set( true );\r
- ++(d_statistics.d_conflict_inst);\r
- break;\r
- }else if( e==effort_prop_eq ){\r
- ++(d_statistics.d_prop_inst);\r
- }else if( e==effort_partial ){\r
- ++(d_statistics.d_partial_inst);\r
+ std::vector< TNode > c_exp;\r
+ eq::EqualityEngine* ee = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine() ;\r
+ for( unsigned c=0; c<exp.size(); c++ ){\r
+ bool pol = exp[c].getKind()!=NOT;\r
+ TNode lit = pol ? exp[c] : exp[c][0];\r
+ Trace("qcf-check-exp") << "Explain " << lit << ", polarity " << pol << std::endl;\r
+ if( lit.getKind()==EQUAL ){\r
+ if( !pol && !ee->areDisequal( lit[0], lit[1], true ) ){\r
+ exit( 98 );\r
+ }else if( pol && !ee->areEqual( lit[0], lit[1] ) ){\r
+ exit( 99 );\r
+ }\r
+ ee->explainEquality( lit[0], lit[1], pol, c_exp );\r
+ }else{\r
+ if( !ee->areEqual( lit, pol ? d_true : d_false ) ){\r
+ exit( pol ? 96 : 97 );\r
+ }\r
+ ee->explainPredicate( lit, pol, c_exp );\r
+ }\r
+ }\r
+ std::vector< Node > c_lem;\r
+ Trace("qcf-check-exp") << "Actual explanation is : " << std::endl;\r
+ for( unsigned c=0; c<c_exp.size(); c++ ){\r
+ Trace("qcf-check-exp") << " " << c_exp[c] << std::endl;\r
+ Node ccc = c_exp[c].negate();\r
+ if( std::find( c_lem.begin(), c_lem.end(), ccc )==c_lem.end() ){\r
+ c_lem.push_back( ccc );\r
+ }\r
}\r
- }else{\r
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;\r
- //Assert( false );\r
+\r
+ c_lem.push_back( q.negate() );\r
+ Node conf = NodeManager::currentNM()->mkNode( OR, c_lem );\r
+ Trace("qcf-conflict") << "QCF conflict : " << conf << std::endl;\r
+ d_quantEngine->addLemma( conf, false );\r
+ d_conflict.set( true );\r
+ ++(d_statistics.d_conflict_inst);\r
+ ++addedLemmas;\r
+ break;\r
}\r
- //clean up assigned\r
- for( unsigned i=0; i<assigned.size(); i++ ){\r
- qi->d_match[ assigned[i] ] = TNode::null();\r
+ }\r
+ */\r
+ std::vector< Node > terms;\r
+ qi->getMatch( terms );\r
+ if( Debug.isOn("qcf-check-inst") ){\r
+ //if( e==effort_conflict ){\r
+ Node inst = d_quantEngine->getInstantiation( q, terms );\r
+ Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
+ Assert( evaluate( inst )!=1 );\r
+ Assert( evaluate( inst )==-1 || e>effort_conflict );\r
+ //}\r
+ }\r
+ if( d_quantEngine->addInstantiation( q, terms ) ){\r
+ Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
+ ++addedLemmas;\r
+ if( e==effort_conflict ){\r
+ d_quant_order.insert( d_quant_order.begin(), q );\r
+ d_conflict.set( true );\r
+ ++(d_statistics.d_conflict_inst);\r
+ break;\r
+ }else if( e==effort_prop_eq ){\r
+ ++(d_statistics.d_prop_inst);\r
}\r
}else{\r
- Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
+ Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;\r
+ //Assert( false );\r
}\r
+ //clean up assigned\r
+ qi->revertMatch( assigned );\r
}else{\r
- Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
+ Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
}\r
- }\r
- if( d_conflict ){\r
- break;\r
- }\r
+ }else{\r
+ Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl;\r
+ }
+ }\r
+ if( d_conflict ){\r
+ break;\r
}\r
}\r
}\r
\r
bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
d_performCheck = false;\r
- if( !d_conflict ){\r
+ if( options::quantConflictFind() && !d_conflict ){\r
if( level==Theory::EFFORT_LAST_CALL ){\r
d_performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;\r
}else if( level==Theory::EFFORT_FULL ){\r
}\r
\r
void QuantConflictFind::computeRelevantEqr() {\r
- d_uf_terms.clear();\r
- d_eqc_uf_terms.clear();\r
- d_eqcs.clear();\r
- d_model_basis.clear();\r
- d_arg_reps.clear();\r
- //double clSet = 0;\r
- //if( Trace.isOn("qcf-opt") ){\r
- // clSet = double(clock())/double(CLOCKS_PER_SEC);\r
- //}\r
-\r
- //long nTermst = 0;\r
- //long nTerms = 0;\r
- //long nEqc = 0;\r
+ if( d_needs_computeRelEqr ){\r
+ d_needs_computeRelEqr = false;\r
+ Trace("qcf-check") << "Compute relevant equalities..." << std::endl;\r
+ d_uf_terms.clear();\r
+ d_eqc_uf_terms.clear();\r
+ d_eqcs.clear();\r
+ d_model_basis.clear();\r
+ d_arg_reps.clear();\r
+ //double clSet = 0;\r
+ //if( Trace.isOn("qcf-opt") ){\r
+ // clSet = double(clock())/double(CLOCKS_PER_SEC);\r
+ //}\r
\r
- //which nodes are irrelevant for disequality matches\r
- std::map< TNode, bool > irrelevant_dnode;\r
- //now, store matches\r
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
- while( !eqcs_i.isFinished() ){\r
- //nEqc++;\r
- Node r = (*eqcs_i);\r
- TypeNode rtn = r.getType();\r
- if( options::qcfMode()==QCF_MC ){\r
- std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );\r
- if( itt==d_eqcs.end() ){\r
- Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );\r
- if( !getEqualityEngine()->hasTerm( mb ) ){\r
- Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;\r
- Assert( false );\r
- }\r
- Node mbr = getRepresentative( mb );\r
- if( mbr!=r ){\r
- d_eqcs[rtn].push_back( mbr );\r
+ //long nTermst = 0;\r
+ //long nTerms = 0;\r
+ //long nEqc = 0;\r
+\r
+ //which nodes are irrelevant for disequality matches\r
+ std::map< TNode, bool > irrelevant_dnode;\r
+ //now, store matches\r
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
+ while( !eqcs_i.isFinished() ){\r
+ //nEqc++;\r
+ Node r = (*eqcs_i);\r
+ TypeNode rtn = r.getType();\r
+ if( options::qcfMode()==QCF_MC ){\r
+ std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );\r
+ if( itt==d_eqcs.end() ){\r
+ Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );\r
+ if( !getEqualityEngine()->hasTerm( mb ) ){\r
+ Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;\r
+ Assert( false );\r
+ }\r
+ Node mbr = getRepresentative( mb );\r
+ if( mbr!=r ){\r
+ d_eqcs[rtn].push_back( mbr );\r
+ }\r
+ d_eqcs[rtn].push_back( r );\r
+ d_model_basis[rtn] = mb;\r
+ }else{\r
+ itt->second.push_back( r );\r
}\r
- d_eqcs[rtn].push_back( r );\r
- d_model_basis[rtn] = mb;\r
}else{\r
- itt->second.push_back( r );\r
- }\r
- }else{\r
- d_eqcs[rtn].push_back( r );\r
- }\r
- /*\r
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
- while( !eqc_i.isFinished() ){\r
- TNode n = (*eqc_i);\r
- if( n.hasBoundVar() ){\r
- std::cout << "BAD TERM IN DB : " << n << std::endl;\r
- exit( 199 );\r
- }\r
- ++eqc_i;\r
- }\r
- */\r
+ d_eqcs[rtn].push_back( r );\r
+ }
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
+ while( !eqc_i.isFinished() ){\r
+ TNode n = (*eqc_i);\r
+ if( n.hasBoundVar() ){\r
+ std::cout << "BAD TERM IN DB : " << n << std::endl;\r
+ exit( 199 );\r
+ }\r
+ ++eqc_i;\r
+ }
\r
- //if( r.getType().isInteger() ){\r
- // Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;\r
- //}\r
- //EqcInfo * eqcir = getEqcInfo( r, false );\r
- //get relevant nodes that we are disequal from\r
- /*\r
- std::vector< Node > deqc;\r
- if( eqcir ){\r
- for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){\r
- if( (*it).second ){\r
- //Node rd = (*it).first;\r
- //if( rd!=getRepresentative( rd ) ){\r
- // std::cout << "Bad rep!" << std::endl;\r
- // exit( 0 );\r
- //}\r
- deqc.push_back( (*it).first );\r
+ //if( r.getType().isInteger() ){\r
+ // Trace("qcf-mv") << "Model value for eqc(" << r << ") : " << d_quantEngine->getValuation().getModelValue( r ) << std::endl;\r
+ //}\r
+ //EqcInfo * eqcir = getEqcInfo( r, false );\r
+ //get relevant nodes that we are disequal from\r
+ /*\r
+ std::vector< Node > deqc;\r
+ if( eqcir ){\r
+ for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){\r
+ if( (*it).second ){\r
+ //Node rd = (*it).first;\r
+ //if( rd!=getRepresentative( rd ) ){\r
+ // std::cout << "Bad rep!" << std::endl;\r
+ // exit( 0 );\r
+ //}\r
+ deqc.push_back( (*it).first );\r
+ }\r
}\r
}\r
- }\r
- */\r
- //process disequalities\r
- /*\r
- eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
- while( !eqc_i.isFinished() ){\r
- TNode n = (*eqc_i);\r
- if( n.getKind()!=EQUAL ){\r
- nTermst++;\r
- //node_to_rep[n] = r;\r
- //if( n.getNumChildren()>0 ){\r
- // if( n.getKind()!=APPLY_UF ){\r
- // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;\r
- // }\r
- //}\r
- if( !n.hasBoundVar() ){ //temporary\r
-\r
- bool isRedundant;\r
- std::map< TNode, std::vector< TNode > >::iterator it_na;\r
- TNode fn;\r
- if( MatchGen::isHandledUfTerm( n ) ){\r
- Node f = MatchGen::getOperator( this, n );\r
- computeArgReps( n );\r
- it_na = d_arg_reps.find( n );\r
- Assert( it_na!=d_arg_reps.end() );\r
- Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );\r
- isRedundant = (nadd!=n);\r
- d_uf_terms[f].addTerm( n, d_arg_reps[n] );\r
+ */\r
+ //process disequalities\r
+ /*\r
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
+ while( !eqc_i.isFinished() ){\r
+ TNode n = (*eqc_i);\r
+ if( n.getKind()!=EQUAL ){\r
+ nTermst++;\r
+ //node_to_rep[n] = r;\r
+ //if( n.getNumChildren()>0 ){\r
+ // if( n.getKind()!=APPLY_UF ){\r
+ // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;\r
+ // }\r
+ //}\r
+ if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){ //temporary\r
+\r
+ bool isRedundant;\r
+ std::map< TNode, std::vector< TNode > >::iterator it_na;\r
+ TNode fn;\r
+ if( MatchGen::isHandledUfTerm( n ) ){\r
+ Node f = MatchGen::getOperator( this, n );\r
+ computeArgReps( n );\r
+ it_na = d_arg_reps.find( n );\r
+ Assert( it_na!=d_arg_reps.end() );\r
+ Node nadd = d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );\r
+ isRedundant = (nadd!=n);\r
+ d_uf_terms[f].addTerm( n, d_arg_reps[n] );\r
+ }else{\r
+ isRedundant = false;\r
+ }\r
+ nTerms += isRedundant ? 0 : 1;\r
}else{\r
- isRedundant = false;\r
- }\r
- nTerms += isRedundant ? 0 : 1;\r
- }else{\r
- if( Debug.isOn("qcf-nground") ){\r
- Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl;\r
- Assert( false );\r
+ if( Debug.isOn("qcf-nground") ){\r
+ Debug("qcf-nground") << "Non-ground term in eqc : " << n << std::endl;\r
+ Assert( false );\r
+ }\r
}\r
}\r
+ ++eqc_i;\r
}\r
- ++eqc_i;\r
+ */\r
+ ++eqcs_i;\r
+ }\r
+ /*\r
+ if( Trace.isOn("qcf-opt") ){\r
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("qcf-opt") << "Compute rel eqc : " << std::endl;\r
+ Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;\r
+ Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;\r
+ Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;\r
}\r
*/\r
- ++eqcs_i;\r
}\r
- /*\r
- if( Trace.isOn("qcf-opt") ){\r
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
- Trace("qcf-opt") << "Compute rel eqc : " << std::endl;\r
- Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;\r
- Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;\r
- Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;\r
- }\r
- */\r
}\r
\r
void QuantConflictFind::computeArgReps( TNode n ) {\r
QuantConflictFind::Statistics::Statistics():\r
d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),\r
d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),\r
- d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),\r
- d_partial_inst("QuantConflictFind::Instantiations_Partial", 0 )\r
+ d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )\r
{\r
StatisticsRegistry::registerStat(&d_inst_rounds);\r
StatisticsRegistry::registerStat(&d_conflict_inst);\r
StatisticsRegistry::registerStat(&d_prop_inst);\r
- StatisticsRegistry::registerStat(&d_partial_inst);\r
}\r
\r
QuantConflictFind::Statistics::~Statistics(){\r
StatisticsRegistry::unregisterStat(&d_inst_rounds);\r
StatisticsRegistry::unregisterStat(&d_conflict_inst);\r
StatisticsRegistry::unregisterStat(&d_prop_inst);\r
- StatisticsRegistry::unregisterStat(&d_partial_inst);\r
}\r
\r
}\r
typ_formula,\r
typ_var,\r
typ_ite_var,\r
- typ_top,\r
+ typ_bool_var,\r
};\r
void debugPrintType( const char * c, short typ, bool isTrace = false );\r
public:\r
MatchGen() : d_type( typ_invalid ){}\r
MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );\r
bool d_tgt;\r
+ bool d_tgt_orig;\r
+ bool d_wasSet;\r
Node d_n;\r
std::vector< MatchGen > d_children;\r
short d_type;\r
void reset_round( QuantConflictFind * p );\r
void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );\r
bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );\r
+ bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );\r
+ Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );\r
bool isValid() { return d_type!=typ_invalid; }\r
void setInvalid();\r
\r
// is this term treated as UF application?\r
+ static bool isHandledBoolConnective( TNode n );\r
static bool isHandledUfTerm( TNode n );\r
static Node getOperator( QuantConflictFind * p, Node n );\r
+ //can this node be handled by the algorithm\r
+ static bool isHandled( TNode n );\r
};\r
\r
//info for quantifiers\r
class QuantInfo {\r
private:\r
void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );\r
- void flatten( Node n, bool beneathQuant );\r
+ void flatten( Node n, bool beneathQuant );
+private: //for completing match\r
+ std::vector< int > d_unassigned;\r
+ std::vector< TypeNode > d_unassigned_tn;\r
+ int d_unassigned_nvar;\r
+ int d_una_index;\r
+ std::vector< int > d_una_eqc_count;\r
public:\r
- QuantInfo() : d_mg( NULL ), d_isPartial( false ) {}\r
+ QuantInfo() : d_mg( NULL ) {}\r
std::vector< TNode > d_vars;\r
std::map< TNode, int > d_var_num;\r
std::map< TNode, bool > d_nbeneathQuant;\r
bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }\r
int getNumVars() { return (int)d_vars.size(); }\r
TNode getVar( int i ) { return d_vars[i]; }\r
+\r
MatchGen * d_mg;\r
Node d_q;\r
std::map< int, MatchGen * > d_var_mg;\r
std::map< int, std::map< TNode, int > > d_curr_var_deq;\r
int getCurrentRepVar( int v );\r
TNode getCurrentValue( TNode n );\r
+ TNode getCurrentExpValue( TNode n );\r
bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );\r
int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );\r
int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );\r
bool setMatch( QuantConflictFind * p, int v, TNode n );\r
bool isMatchSpurious( QuantConflictFind * p );\r
- bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned );\r
+ bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );\r
+ void revertMatch( std::vector< int >& assigned );\r
void debugPrintMatch( const char * c );\r
- bool isConstrainedVar( int v );\r
-public:\r
- // is partial\r
- bool d_isPartial;\r
- //the variables that this quantified formula has not beneath nested quantifiers\r
- std::map< TNode, bool > d_has_var;\r
- bool isPartial() { return d_isPartial; }\r
+ bool isConstrainedVar( int v );
+public:
+ void getMatch( std::vector< Node >& terms );\r
};\r
\r
class QuantConflictFind : public QuantifiersModule\r
effort_mc,\r
};\r
short d_effort;\r
+ void setEffort( int e ) { d_effort = e; }\r
+ static short getMaxQcfEffort();\r
bool areMatchEqual( TNode n1, TNode n2 );\r
bool areMatchDisequal( TNode n1, TNode n2 );\r
public:\r
void merge( Node a, Node b );\r
/** assert disequal */\r
void assertDisequal( Node a, Node b );\r
+ /** reset round */\r
+ void reset_round( Theory::Effort level );\r
/** check */\r
void check( Theory::Effort level );\r
/** needs check */\r
bool needsCheck( Theory::Effort level );\r
private:\r
+ bool d_needs_computeRelEqr;\r
+public:\r
void computeRelevantEqr();\r
private:\r
void debugPrint( const char * c );\r
IntStat d_inst_rounds;\r
IntStat d_conflict_inst;\r
IntStat d_prop_inst;\r
- IntStat d_partial_inst;\r
Statistics();\r
~Statistics();\r
};\r
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/options.h"
+#include "theory/quantifiers/term_database.h"
using namespace std;
using namespace CVC4;
}
}
-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;
}
}
-
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 ){
}
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;
}
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
}
//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 );
}
}
}
+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;
//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() );
//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);
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 ){
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{
}
}
-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
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();
}
//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;
}
}
}
- 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 ){
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] );
}
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;
+ }
+}
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 );
static bool doMiniscopingNoFreeVar();
static bool doMiniscopingAnd();
static bool doOperation( Node f, bool isNested, int computeOption );
+public:
+ static Node rewriteRewriteRule( Node r );
+ static bool containsQuantifiers(Node n);
+ static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector<Node>& fvs);
public:
//static Node rewriteQuants( Node n, bool isNested = false );
//static Node rewriteQuant( Node n, bool isNested = false );
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;
}
}
}
}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 );
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 );
}
#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;
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 ){
}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
//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() );
}
}
-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] );
+ }
}
}
}
+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
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 );
#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;
}
}
-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();
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 ) ){
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;
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);
- }
}
}
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();
+ }
+}
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,
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;
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
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 */
}
};/* 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 */
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
-#include "theory/rewriterules/efficient_e_matching.h"
-#include "theory/rewriterules/rr_trigger.h"
+//#include "theory/rewriterules/efficient_e_matching.h"
+//#include "theory/rewriterules/rr_trigger.h"
#include "theory/quantifiers/bounded_integers.h"
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/uf/options.h"
+#include "theory/uf/theory_uf.h"
using namespace std;
using namespace CVC4;
d_eq_query = new EqualityQueryQuantifiersEngine( this );
d_term_db = new quantifiers::TermDb( this );
d_tr_trie = new inst::TriggerTrie;
- d_rr_tr_trie = new rrinst::TriggerTrie;
- d_eem = new EfficientEMatcher( this );
+ //d_rr_tr_trie = new rrinst::TriggerTrie;
+ //d_eem = new EfficientEMatcher( this );
d_hasAddedLemma = false;
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
}
//add quantifiers modules
- if( options::quantConflictFind() ){
+ if( options::quantConflictFind() || options::quantRewriteRules() ){
d_qcf = new quantifiers::QuantConflictFind( this, c);
d_modules.push_back( d_qcf );
}else{
d_model_engine = NULL;
d_bint = NULL;
}
- if( options::rewriteRulesAsAxioms() ){
+ if( options::quantRewriteRules() ){
d_rr_engine = new quantifiers::RewriteEngine( c, this );
d_modules.push_back(d_rr_engine);
}else{
return d_eq_query;
}
-//Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
-// return d_te->theoryOf( id )->getInstantiator();
-//}
-
context::Context* QuantifiersEngine::getSatContext(){
return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext();
}
if( d_rel_dom ){
d_rel_dom->reset();
}
+ for( int i=0; i<(int)d_modules.size(); i++ ){
+ d_modules[i]->reset_round( e );
+ }
if( e==Theory::EFFORT_LAST_CALL ){
//if effort is last call, try to minimize model first
if( options::finiteModelFind() ){
void QuantifiersEngine::registerQuantifier( Node f ){
if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){
- Trace("quant") << "Register quantifier : " << f << std::endl;
+ Trace("quant") << "QuantifiersEngine : Register quantifier ";
+ if( d_term_db->isRewriteRule( f ) ){
+ Trace("quant") << " (rewrite rule)";
+ }
+ Trace("quant") << " : " << f << std::endl;
d_quants.push_back( f );
++(d_statistics.d_num_quant);
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
std::set< Node > added;
getTermDatabase()->addTerm( n, added, withinQuant );
- if( options::efficientEMatching() ){
- d_eem->newTerms( added );
- }
//added contains also the Node that just have been asserted in this branch
if( d_quant_rel ){
for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){
}
}
-Node QuantifiersEngine::doSubstitute( Node n, std::vector< Node >& terms ){
+Node QuantifiersEngine::getSubstitute( Node n, std::vector< Node >& terms ){
if( n.getKind()==INST_CONSTANT ){
Debug("check-inst") << "Substitute inst constant : " << n << std::endl;
return terms[n.getAttribute(InstVarNumAttribute())];
}
bool changed = false;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- Node c = doSubstitute( n[i], terms );
+ Node c = getSubstitute( n[i], terms );
cc.push_back( c );
changed = changed || c!=n[i];
}
}else{
//do optimized version
Node icb = d_term_db->getInstConstantBody( f );
- body = doSubstitute( icb, terms );
+ body = getSubstitute( icb, terms );
if( Debug.isOn("check-inst") ){
Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() );
if( body!=body2 ){
d_triggers("QuantifiersEngine::Triggers", 0),
d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
- d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0),
- d_term_in_termdb("QuantifiersEngine::Term_in_TermDb", 0),
- d_num_mono_candidates("QuantifiersEngine::NumMonoCandidates", 0),
- d_num_mono_candidates_new_term("QuantifiersEngine::NumMonoCandidatesNewTerm", 0),
- d_num_multi_candidates("QuantifiersEngine::NumMultiCandidates", 0),
- d_mono_candidates_cache_hit("QuantifiersEngine::MonoCandidatesCacheHit", 0),
- d_mono_candidates_cache_miss("QuantifiersEngine::MonoCandidatesCacheMiss", 0),
- d_multi_candidates_cache_hit("QuantifiersEngine::MultiCandidatesCacheHit", 0),
- d_multi_candidates_cache_miss("QuantifiersEngine::MultiCandidatesCacheMiss", 0)
+ d_multi_trigger_instantiations("QuantifiersEngine::Multi_Trigger_Instantiations", 0)
{
StatisticsRegistry::registerStat(&d_num_quant);
StatisticsRegistry::registerStat(&d_instantiation_rounds);
StatisticsRegistry::registerStat(&d_simple_triggers);
StatisticsRegistry::registerStat(&d_multi_triggers);
StatisticsRegistry::registerStat(&d_multi_trigger_instantiations);
- StatisticsRegistry::registerStat(&d_term_in_termdb);
- StatisticsRegistry::registerStat(&d_num_mono_candidates);
- StatisticsRegistry::registerStat(&d_num_mono_candidates_new_term);
- StatisticsRegistry::registerStat(&d_num_multi_candidates);
- StatisticsRegistry::registerStat(&d_mono_candidates_cache_hit);
- StatisticsRegistry::registerStat(&d_mono_candidates_cache_miss);
- StatisticsRegistry::registerStat(&d_multi_candidates_cache_hit);
- StatisticsRegistry::registerStat(&d_multi_candidates_cache_miss);
}
QuantifiersEngine::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_simple_triggers);
StatisticsRegistry::unregisterStat(&d_multi_triggers);
StatisticsRegistry::unregisterStat(&d_multi_trigger_instantiations);
- StatisticsRegistry::unregisterStat(&d_term_in_termdb);
- StatisticsRegistry::unregisterStat(&d_num_mono_candidates);
- StatisticsRegistry::unregisterStat(&d_num_mono_candidates_new_term);
- StatisticsRegistry::unregisterStat(&d_num_multi_candidates);
- StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_hit);
- StatisticsRegistry::unregisterStat(&d_mono_candidates_cache_miss);
- StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_hit);
- StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
}
eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
#include "theory/theory.h"
#include "util/hash.h"
#include "theory/quantifiers/inst_match.h"
-#include "theory/rewriterules/rr_inst_match.h"
#include "theory/quantifiers/quant_util.h"
+#include "expr/attribute.h"
#include "util/statistics_registry.h"
virtual void finishInit() {}
/* whether this module needs to check this round */
virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+ /* reset at a round */
+ virtual void reset_round( Theory::Effort e ){}
/* Call during quantifier engine's check */
virtual void check( Theory::Effort e ) = 0;
/* Called for new quantifiers */
class TriggerTrie;
}/* CVC4::theory::inst */
-namespace rrinst {
- class TriggerTrie;
-}/* CVC4::theory::inst */
-
-class EfficientEMatcher;
+//class EfficientEMatcher;
class EqualityQueryQuantifiersEngine;
class QuantifiersEngine {
quantifiers::RelevantDomain* d_rel_dom;
/** phase requirements for each quantifier for each instantiation literal */
std::map< Node, QuantPhaseReq* > d_phase_reqs;
- /** efficient e-matcher */
- EfficientEMatcher* d_eem;
/** instantiation engine */
quantifiers::InstantiationEngine* d_inst_engine;
/** model engine */
quantifiers::TermDb* d_term_db;
/** all triggers will be stored in this trie */
inst::TriggerTrie* d_tr_trie;
- /** all triggers for rewrite rules will be stored in this trie */
- rrinst::TriggerTrie* d_rr_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
/** statistics for debugging */
public:
QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te);
~QuantifiersEngine();
- /** get instantiator for id */
- //Instantiator* getInstantiator( theory::TheoryId id );
/** get theory engine */
TheoryEngine* getTheoryEngine() { return d_te; }
/** get equality query object for the given type. The default is the
QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; }
/** get phase requirement terms */
void getPhaseReqTerms( Node f, std::vector< Node >& nodes );
- /** get efficient e-matching utility */
- EfficientEMatcher* getEfficientEMatcher() { return d_eem; }
/** get bounded integers utility */
quantifiers::BoundedIntegers * getBoundedIntegers() { return d_bint; }
/** Conflict find mechanism for quantifiers */
bool addInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
/** set instantiation level attr */
void setInstantiationLevelAttr( Node n, uint64_t level );
- /** do substitution */
- Node doSubstitute( Node n, std::vector< Node >& terms );
public:
/** get instantiation */
Node getInstantiation( Node f, std::vector< Node >& vars, std::vector< Node >& terms );
Node getInstantiation( Node f, InstMatch& m );
/** get instantiation */
Node getInstantiation( Node f, std::vector< Node >& terms );
+ /** do substitution */
+ Node getSubstitute( Node n, std::vector< Node >& terms );
/** exist instantiation ? */
bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
/** add lemma lem */
quantifiers::TermDb* getTermDatabase() { return d_term_db; }
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
- /** get rewrite trigger database */
- rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; }
/** add term to database */
void addTermToDatabase( Node n, bool withinQuant = false );
/** get the master equality engine */
IntStat d_simple_triggers;
IntStat d_multi_triggers;
IntStat d_multi_trigger_instantiations;
- IntStat d_term_in_termdb;
- IntStat d_num_mono_candidates;
- IntStat d_num_mono_candidates_new_term;
- IntStat d_num_multi_candidates;
- IntStat d_mono_candidates_cache_hit;
- IntStat d_mono_candidates_cache_miss;
- IntStat d_multi_candidates_cache_hit;
- IntStat d_multi_candidates_cache_miss;
Statistics();
~Statistics();
};/* class QuantifiersEngine::Statistics */
# constants...
-# types...
-sort RRHB_TYPE \
- Cardinality::INTEGERS \
- not-well-founded \
- "head and body of the rule type"
-
-# operators...
-
-# variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
-operator REWRITE_RULE 3 "general rewrite rule"
-#HEAD/BODY/TRIGGER
-operator RR_REWRITE 2:3 "actual rewrite rule"
-operator RR_REDUCTION 2:3 "actual reduction rule"
-operator RR_DEDUCTION 2:3 "actual deduction rule"
-
-typerule REWRITE_RULE ::CVC4::theory::rewriterules::RewriteRuleTypeRule
-typerule RR_REWRITE ::CVC4::theory::rewriterules::RRRewriteTypeRule
-typerule RR_REDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule
-typerule RR_DEDUCTION ::CVC4::theory::rewriterules::RRRedDedTypeRule
-
endtheory
**/
#include "theory/rewriterules/theory_rewriterules.h"
-#include "theory/rewriterules/theory_rewriterules_rules.h"
-#include "theory/rewriterules/theory_rewriterules_params.h"
-
-#include "theory/rewriterules/theory_rewriterules_preprocess.h"
#include "theory/rewriter.h"
-#include "theory/rewriterules/options.h"
using namespace std;
namespace rewriterules {
-inline std::ostream& operator <<(std::ostream& stream, const RuleInst& ri) {
- ri.toStream(stream);
- return stream;
-}
-
-static const RuleInst* RULEINST_TRUE = (RuleInst*) 1;
-static const RuleInst* RULEINST_FALSE = (RuleInst*) 2;
-
- /** Rule an instantiation with the given match */
-RuleInst::RuleInst(TheoryRewriteRules & re, const RewriteRule * r,
- std::vector<Node> & inst_subst,
- Node matched):
- rule(r), d_matched(matched)
-{
- Assert(r != NULL);
- Assert(!r->directrr || !d_matched.isNull());
- subst.swap(inst_subst);
-};
-
-Node RuleInst::substNode(const TheoryRewriteRules & re, TNode r,
- TCache cache ) const {
- Assert(this != RULEINST_TRUE && this != RULEINST_FALSE);
- return r.substitute (rule->free_vars.begin(),rule->free_vars.end(),
- subst.begin(),subst.end(),cache);
-};
-size_t RuleInst::findGuard(TheoryRewriteRules & re, size_t start)const{
- TCache cache;
- Assert(this != RULEINST_TRUE && this != RULEINST_FALSE);
- while (start < (rule->guards).size()){
- Node g = substNode(re,rule->guards[start],cache);
- switch(re.addWatchIfDontKnow(g,this,start)){
- case ATRUE:
- Debug("rewriterules::guards") << g << "is true" << std::endl;
- ++start;
- continue;
- case AFALSE:
- Debug("rewriterules::guards") << g << "is false" << std::endl;
- return -1;
- case ADONTKNOW:
- Debug("rewriterules::guards") << g << "is unknown" << std::endl;
- return start;
- }
- }
- /** All the guards are verified */
- re.propagateRule(this,cache);
- return start;
-};
-
-bool RuleInst::alreadyRewritten(TheoryRewriteRules & re) const{
- Assert(this != RULEINST_TRUE && this != RULEINST_FALSE);
- static NoMatchAttribute rewrittenNodeAttribute;
- TCache cache;
- for(std::vector<Node>::const_iterator
- iter = rule->to_remove.begin();
- iter != rule->to_remove.end(); ++iter){
- if (substNode(re,*iter,cache).getAttribute(rewrittenNodeAttribute))
- return true;
- };
- return false;
-}
-
-void RuleInst::toStream(std::ostream& out) const{
- if(this == RULEINST_TRUE){ out << "TRUE"; return;};
- if(this == RULEINST_FALSE){ out << "FALSE"; return;};
- out << "(" << *rule << ") ";
- for(std::vector<Node>::const_iterator
- iter = subst.begin(); iter != subst.end(); ++iter){
- out << *iter << " ";
- };
-}
-
-
-void Guarded::nextGuard(TheoryRewriteRules & re)const{
- Assert(inst != RULEINST_TRUE && inst != RULEINST_FALSE);
- if(simulateRewritting && inst->alreadyRewritten(re)) return;
- inst->findGuard(re,d_guard+1);
-};
-
-/** start indicate the first guard which is not true */
-Guarded::Guarded(const RuleInst* ri, const size_t start) :
- d_guard(start),inst(ri) {};
-Guarded::Guarded(const Guarded & g) :
- d_guard(g.d_guard),inst(g.inst) {};
-Guarded::Guarded() :
- //dumb value
- d_guard(-1),inst(RULEINST_TRUE) {};
-
TheoryRewriteRules::TheoryRewriteRules(context::Context* c,
context::UserContext* u,
OutputChannel& out,
Valuation valuation,
const LogicInfo& logicInfo) :
- Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo),
- d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0),
- d_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false)
+ Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo)
{
- d_true = NodeManager::currentNM()->mkConst<bool>(true);
- d_false = NodeManager::currentNM()->mkConst<bool>(false);
-}
-
-void TheoryRewriteRules::addMatchRuleTrigger(const RewriteRule * r,
- rrinst::InstMatch & im,
- bool delay){
- ++r->nb_matched;
- ++d_statistics.d_match_found;
- if(rewrite_instantiation) im.applyRewrite();
- if(representative_instantiation)
- im.makeRepresentative( getQuantifiersEngine() );
- if(!cache_match || !r->inCache(*this,im)){
- ++r->nb_applied;
- ++d_statistics.d_cache_miss;
- std::vector<Node> subst;
- //AJR: replaced computeTermVec with this
- for( size_t i=0; i<r->inst_vars.size(); i++ ){
- Node n = im.getValue( r->inst_vars[i] );
- Assert( !n.isNull() );
- subst.push_back( n );
- }
- RuleInst * ri = new RuleInst(*this,r,subst,
- r->directrr ? im.d_matched : Node::null());
- Debug("rewriterules::matching") << "One matching found"
- << (delay? "(delayed)":"")
- << ":" << *ri << std::endl;
- // Find the first non verified guard, don't save the rule if the
- // rule can already be fired In fact I save it otherwise strange
- // things append.
- Assert(ri->rule != NULL);
- if(delay) d_ruleinsts_to_add.push_back(ri);
- else{
- if(simulateRewritting && ri->alreadyRewritten(*this)) return;
- if(ri->findGuard(*this, 0) != (r->guards).size())
- d_ruleinsts.push_back(ri);
- else delete(ri);
- };
- }else{
- ++d_statistics.d_cache_hit;
- };
}
void TheoryRewriteRules::check(Effort level) {
CodeTimer codeTimer(d_theoryTime);
- Assert(d_ruleinsts_to_add.empty());
-
while(!done()) {
// Get all the assertions
// TODO: Test that it have already been ppAsserted
//if we are here and ppAssert has not been done
// that means that ppAssert is off so we need to assert now
- if(!d_ppAssert_on) addRewriteRule(get());
- else get();
+ Assertion assertion = get();
// Assertion assertion = get();
// TNode fact = assertion.assertion;
// Unhandled(getValuation().getDecisionLevel());
// addRewriteRule(fact);
- };
-
- Debug("rewriterules::check") << "RewriteRules::Check start " << d_checkLevel << (level==EFFORT_FULL? " EFFORT_FULL":"") << std::endl;
-
- /** Test each rewrite rule */
- for(size_t rid = 0, end = d_rules.size(); rid < end; ++rid) {
- RewriteRule * r = d_rules[rid];
- if (level!=EFFORT_FULL && r->d_split) continue;
- Debug("rewriterules::check") << "RewriteRules::Check rule: " << *r << std::endl;
- Trigger & tr = r->trigger;
- //reset instantiation round for trigger (set up match production)
- tr.resetInstantiationRound();
-
- /** Test the possible matching one by one */
- while(tr.getNextMatch()){
- rrinst::InstMatch im = tr.getInstMatch();
- addMatchRuleTrigger(r, im, true);
- }
- }
-
- const bool do_notification = d_checkLevel == 0 || level==EFFORT_FULL;
- bool polldone = false;
-
- if(level==EFFORT_FULL) ++d_statistics.d_full_check;
- else ++d_statistics.d_check;
-
- GuardedMap::const_iterator p = d_guardeds.begin();
- do{
-
-
- //dequeue instantiated rules
- for(; !d_ruleinsts_to_add.empty();){
- RuleInst * ri = d_ruleinsts_to_add.back(); d_ruleinsts_to_add.pop_back();
- if(simulateRewritting && ri->alreadyRewritten(*this)) continue;
- if(ri->findGuard(*this, 0) != ri->rule->guards.size())
- d_ruleinsts.push_back(ri);
- else delete(ri);
- };
-
- if(do_notification)
- /** Temporary way. Poll value */
- for (; p != d_guardeds.end(); ++p){
- TNode g = (*p).first;
- const GList * const l = (*p).second;
- const Guarded & glast = l->back();
- // Notice() << "Polled?:" << g << std::endl;
- if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) continue;
- // Notice() << "Polled!:" << g << "->" << (glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE) << std::endl;
- bool value;
- if(getValuation().hasSatValue(g,value)){
- if(value) polldone = true; //One guard is true so pass n check
- Debug("rewriterules::guards") << "Poll value:" << g
- << " is " << (value ? "true" : "false") << std::endl;
- notification(g,value);
- //const Guarded & glast2 = (*l)[l->size()-1];
- // Notice() << "Polled!!:" << g << "->" << (glast2.inst == RULEINST_TRUE||glast2.inst == RULEINST_FALSE) << std::endl;
- };
- };
-
- }while(!d_ruleinsts_to_add.empty() ||
- (p != d_guardeds.end() && do_notification));
-
- if(polldone) d_checkLevel = checkSlowdown;
- else d_checkLevel = d_checkLevel > 0 ? (d_checkLevel - 1) : 0;
-
- /** Narrowing by splitting on the guards */
- /** Perhaps only when no notification? */
- if(narrowing_full_effort && level==EFFORT_FULL){
- for (GuardedMap::const_iterator p = d_guardeds.begin();
- p != d_guardeds.end(); ++p){
- TNode g = (*p).first;
- const GList * const l = (*p).second;
- const Guarded & glast = (*l)[l->size()-1];
- if(glast.inst == RULEINST_TRUE||glast.inst == RULEINST_FALSE)
- continue;
- // If it has a value it should already has been notified
- bool value CVC4_UNUSED;
- Assert(!getValuation().hasSatValue(g,value));
- Debug("rewriterules::check") << "RewriteRules::Check Narrowing on:" << g << std::endl;
- /** Can split on already rewritten instrule... but... */
- getOutputChannel().split(g);
}
- }
-
- Assert(d_ruleinsts_to_add.empty());
- Debug("rewriterules::check") << "RewriteRules::Check done " << d_checkLevel << std::endl;
-
-};
-
-void TheoryRewriteRules::registerQuantifier( Node n ){};
-
-Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern ) {
- // Debug("rewriterules") << "createTrigger:";
- getQuantifiersEngine()->registerPattern(pattern);
- return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern,
- options::efficientEMatching()?
- Trigger::MATCH_GEN_EFFICIENT_E_MATCH :
- Trigger::MATCH_GEN_DEFAULT,
- true,
- Trigger::TR_MAKE_NEW,
- false);
- // options::smartMultiTriggers());
-};
-
-bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested,
- GList * const lpropa) {
- Assert(ltested->size() > 0);
- const Guarded & glast = (*ltested)[ltested->size()-1];
- if(glast.inst == RULEINST_TRUE || glast.inst == RULEINST_FALSE){
- notification(lpropa,glast.inst == RULEINST_TRUE);
- return true;
- };
- return false;
-};
-
-void TheoryRewriteRules::notification(GList * const lpropa, bool b){
- if (b){
- for(size_t ig = 0;
- ig != lpropa->size(); ++ig) {
- (*lpropa)[ig].nextGuard(*this);
- };
- lpropa->push_back(Guarded(RULEINST_TRUE,0));
- }else{
- lpropa->push_back(Guarded(RULEINST_FALSE,0));
- };
- Assert(lpropa->back().inst == RULEINST_TRUE ||
- lpropa->back().inst == RULEINST_FALSE);
};
-
-
-Answer TheoryRewriteRules::addWatchIfDontKnow(Node g0, const RuleInst* ri,
- const size_t gid){
- /** Currently create a node with a literal */
- Node g = getValuation().ensureLiteral(g0);
- GuardedMap::iterator l_i = d_guardeds.find(g);
- GList* l;
- if( l_i == d_guardeds.end() ) {
- /** Normally Not watched so IDONTNOW but since we poll, we can poll now */
- bool value;
- if(getValuation().hasSatValue(g,value)){
- if(value) return ATRUE;
- else return AFALSE;
- };
- //Not watched so IDONTNOW
- l = new(getSatContext()->getCMM())
- GList(true, getSatContext());//,
- //ContextMemoryAllocator<Guarded>(getContext()->getCMM()));
- d_guardeds.insert(g ,l);//.insertDataFromContextMemory(g, l);
- /* TODO Add register propagation */
- } else {
- l = (*l_i).second;
- Assert(l->size() > 0);
- const Guarded & glast = (*l)[l->size()-1];
- if(glast.inst == RULEINST_TRUE) return ATRUE;
- if(glast.inst == RULEINST_FALSE) return AFALSE;
-
- };
- /** I DONT KNOW because not watched or because not true nor false */
- l->push_back(Guarded(ri,gid));
- return ADONTKNOW;
-};
-
-void TheoryRewriteRules::notification(Node g, bool b){
- GuardedMap::const_iterator l = d_guardeds.find(g);
- /** Should be a propagated node already known */
- Assert(l != d_guardeds.end());
- notification((*l).second,b);
-}
-
-
-void TheoryRewriteRules::notifyEq(TNode lhs, TNode rhs) {
- GuardedMap::const_iterator ilhs = d_guardeds.find(lhs);
- GuardedMap::const_iterator irhs = d_guardeds.find(rhs);
- /** Should be a propagated node already known */
- Assert(ilhs != d_guardeds.end());
- if( irhs == d_guardeds.end() ) {
- /** Not watched so points to the list directly */
- d_guardeds.insertDataFromContextMemory(rhs, (*ilhs).second);
- } else {
- GList * const llhs = (*ilhs).second;
- GList * const lrhs = (*irhs).second;
- if(!(notifyIfKnown(llhs,lrhs) || notifyIfKnown(lrhs,llhs))){
- /** If none of the two is known */
- for(GList::const_iterator g = llhs->begin(); g != llhs->end(); ++g){
- lrhs->push_back(*g);
- };
- };
- };
-};
-
-
-Node TheoryRewriteRules::normalizeConjunction(NodeBuilder<> & conjunction){
- Assert(conjunction.getKind() == kind::AND);
- switch(conjunction.getNumChildren()){
- case 0:
- return d_true;
- case 1:
- return conjunction[0];
- default:
- return conjunction;
- }
-
-}
-
-void explainInstantiation(const RuleInst *inst, TNode substHead, NodeBuilder<> & conjunction ){
- TypeNode booleanType = NodeManager::currentNM()->booleanType();
- // if the rule is directly applied by the rewriter,
- // we should take care to use the representative that can't be directly rewritable:
- // If "car(a)" is somewhere and we know that "a = cons(x,l)" we shouldn't
- // add the constraint car(cons(x,l) = x because it is rewritten to x = x.
- // But we should say cons(a) = x
- Assert(!inst->d_matched.isNull());
- Assert( inst->d_matched.getKind() == kind::APPLY_UF);
- Assert( substHead.getKind() == kind::APPLY_UF );
- Assert( inst->d_matched.getOperator() == substHead.getOperator() );
- Assert(conjunction.getKind() == kind::AND);
- // replace the left hand side by the term really matched
- NodeBuilder<2> nb;
- for(size_t i = 0,
- iend = inst->d_matched.getNumChildren(); i < iend; ++i){
- nb.clear( inst->d_matched[i].getType(false) == booleanType ?
- kind::IFF : kind::EQUAL );
- nb << inst->d_matched[i] << substHead[i];
- conjunction << static_cast<Node>(nb);
- }
-}
-
-Node skolemizeBody( Node f ){
- /*TODO skolemize the subformula of s with constant or skolemize
- directly in the body of the rewrite rule with an uninterpreted
- function.
- */
- if ( f.getKind()!=EXISTS ) return f;
- std::vector< Node > vars;
- std::vector< Node > csts;
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- csts.push_back( NodeManager::currentNM()->mkSkolem( "skolem_$$", f[0][i].getType(), "is from skolemizing the body of a rewrite rule" ) );
- vars.push_back( f[0][i] );
- }
- return f[ 1 ].substitute( vars.begin(), vars.end(),
- csts.begin(), csts.end() );
-}
-
-
-void TheoryRewriteRules::propagateRule(const RuleInst * inst, TCache cache){
- // Debug("rewriterules") << "A rewrite rules is verified. Add lemma:";
- Debug("rewriterules::propagate") << "propagateRule" << *inst << std::endl;
- const RewriteRule * rule = inst->rule;
- ++rule->nb_applied;
- // Can be more something else than an equality in fact (eg. propagation rule)
- Node equality = skolemizeBody(inst->substNode(*this,rule->body,cache));
- if(propagate_as_lemma){
- Node lemma = equality;
- if(rule->directrr){
- NodeBuilder<> conjunction(kind::AND);
- explainInstantiation(inst,
- rule->guards.size() > 0?
- inst->substNode(*this,rule->guards[0],cache) : equality[0],
- conjunction);
- Debug("rewriterules-directrr") << "lemma:" << lemma << " :: " << inst->d_matched;
- //rewrite rule
- TypeNode booleanType = NodeManager::currentNM()->booleanType();
- if(equality[1].getType(false) == booleanType)
- equality = inst->d_matched.iffNode(equality[1]);
- else equality = inst->d_matched.eqNode(equality[1]);
- lemma = normalizeConjunction(conjunction).impNode(equality);
- Debug("rewriterules-directrr") << " -> " << lemma << std::endl;
- }
- else if(rule->guards.size() > 0){
- // We can use implication for reduction rules since the head is known
- // to be true
- NodeBuilder<> conjunction(kind::AND);
- substGuards(inst,cache,conjunction);
- lemma = normalizeConjunction(conjunction).impNode(equality);
- }
- Debug("rewriterules::propagate") << "propagated " << lemma << std::endl;
- getOutputChannel().lemma(lemma);
- }else{
- Node lemma_lit = equality;
- if(rule->directrr && rule->guards.size() == 0)
- lemma_lit = inst->d_matched.eqNode(equality[1]); // rewrite rules
- lemma_lit = getValuation().ensureLiteral(lemma_lit);
- ExplanationMap::const_iterator p = d_explanations.find(lemma_lit);
- if(p!=d_explanations.end()) return; //Already propagated
- bool value;
- if(getValuation().hasSatValue(lemma_lit,value)){
- /* Already assigned */
- if (!value){
- NodeBuilder<> conflict(kind::AND);
-
- if(rule->directrr){
- explainInstantiation(inst,
- rule->guards.size() > 0?
- inst->substNode(*this,rule->guards[0],cache) : equality[0],
- conflict);
- if(rule->guards.size() > 0){
- //reduction rule
- Assert(rule->guards.size() == 1);
- conflict << inst->d_matched; //this one will be two times
- }
- }
- substGuards(inst,cache,conflict);
- conflict << lemma_lit;
- getOutputChannel().conflict(normalizeConjunction(conflict));
- };
- }else{
- getOutputChannel().propagate(lemma_lit);
- d_explanations.insert(lemma_lit, *inst);
- };
- };
-
- if(simulateRewritting){
- static NoMatchAttribute rewrittenNodeAttribute;
- // Tag the rewritted terms
- // for(std::vector<Node>::iterator i = rule->to_remove.begin();
- // i == rule->to_remove.end(); ++i){
- // (*i).setAttribute(rewrittenNodeAttribute,true);
- // };
- for(size_t i = 0; i < rule->to_remove.size(); ++i){
- Node rewritten = inst->substNode(*this,rule->to_remove[i],cache);
- Debug("rewriterules::simulateRewriting") << "tag " << rewritten << " as rewritten" << std::endl;
- rewritten.setAttribute(rewrittenNodeAttribute,true);
- };
-
- };
-
- if ( compute_opt && !rule->body_match.empty() ){
-
- uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(getQuantifiersEngine()->getTheoryEngine()->theoryOf( theory::THEORY_UF ));
- eq::EqualityEngine* ee =
- static_cast<eq::EqualityEngine*>(uf->getEqualityEngine());
-
- //Verify that this instantiation can't immediately fire another rule
- for(RewriteRule::BodyMatch::const_iterator p = rule->body_match.begin();
- p != rule->body_match.end(); ++p){
- RewriteRule * r = (*p).second;
- // Use trigger2 since we can be in check
- ApplyMatcher * tr = r->trigger_for_body_match;
- Assert(tr != NULL);
- tr->resetInstantiationRound(getQuantifiersEngine());
- rrinst::InstMatch im;
- TNode m = inst->substNode(*this,(*p).first, cache);
- Assert( m.getKind() == kind::APPLY_UF );
- ee->addTerm(m);
- if( tr->reset(m,im,getQuantifiersEngine()) ){
- im.d_matched = m;
- Debug("rewriterules::matching") << "SimulatedRewrite: " << std::endl;
- addMatchRuleTrigger(r, im);
- }
- }
-
- }
-};
-
-void TheoryRewriteRules::substGuards(const RuleInst *inst,
- TCache cache,
- NodeBuilder<> & conjunction){
- const RewriteRule * r = inst->rule;
- /** Guards */ /* TODO remove the duplicate with a set like in uf? */
- for(std::vector<Node>::const_iterator p = r->guards.begin();
- p != r->guards.end(); ++p) {
- Assert(!p->isNull());
- conjunction << inst->substNode(*this,*p,cache);
- };
-}
-
Node TheoryRewriteRules::explain(TNode n){
- ExplanationMap::const_iterator p = d_explanations.find(n);
- Assert(p!=d_explanations.end(),"I forget the explanation...");
- RuleInst inst = (*p).second;
- const RewriteRule * rule = inst.rule;
- TCache cache;
- NodeBuilder<> explanation(kind::AND);
- if(rule->directrr){
- explainInstantiation(&inst,
- rule->guards.size() > 0?
- inst.substNode(*this,rule->guards[0],cache):
- inst.substNode(*this,rule->body[0] ,cache),
- explanation);
- if(rule->guards.size() > 0){
- //reduction rule
- Assert(rule->guards.size() == 1);
- explanation << inst.d_matched; //this one will be two times
- }
- };
- substGuards(&inst, cache ,explanation);
- return normalizeConjunction(explanation);
-}
-
-void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){
+ return Node::null();
}
-Theory::PPAssertStatus TheoryRewriteRules::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
- //TODO: here add only to the rewriterules database for ppRewrite,
- //and not for the general one. Otherwise rewriting that occur latter
- //on this rewriterules will be lost. But if the rewriting of the
- //body is not done in "in", will it be done latter after
- //substitution? Perhaps we should add the rewriterules to the
- //database for ppRewrite also after the subtitution at the levvel of check
-
- // addRewriteRule(in);
- // d_ppAssert_on = true;
- return PP_ASSERT_STATUS_UNSOLVED;
-}
-
-TheoryRewriteRules::Statistics::Statistics():
- d_num_rewriterules("TheoryRewriteRules::Num_RewriteRules", 0),
- d_check("TheoryRewriteRules::Check", 0),
- d_full_check("TheoryRewriteRules::FullCheck", 0),
- d_poll("TheoryRewriteRules::Poll", 0),
- d_match_found("TheoryRewriteRules::MatchFound", 0),
- d_cache_hit("TheoryRewriteRules::CacheHit", 0),
- d_cache_miss("TheoryRewriteRules::CacheMiss", 0)
-{
- StatisticsRegistry::registerStat(&d_num_rewriterules);
- StatisticsRegistry::registerStat(&d_check);
- StatisticsRegistry::registerStat(&d_full_check);
- StatisticsRegistry::registerStat(&d_poll);
- StatisticsRegistry::registerStat(&d_match_found);
- StatisticsRegistry::registerStat(&d_cache_hit);
- StatisticsRegistry::registerStat(&d_cache_miss);
-}
+void TheoryRewriteRules::collectModelInfo( TheoryModel* m, bool fullModel ){
-TheoryRewriteRules::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_num_rewriterules);
- StatisticsRegistry::unregisterStat(&d_check);
- StatisticsRegistry::unregisterStat(&d_full_check);
- StatisticsRegistry::unregisterStat(&d_poll);
- StatisticsRegistry::unregisterStat(&d_match_found);
- StatisticsRegistry::unregisterStat(&d_cache_hit);
- StatisticsRegistry::unregisterStat(&d_cache_miss);
}
-
}/* CVC4::theory::rewriterules namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "theory/theory_engine.h"
#include "theory/quantifiers_engine.h"
#include "context/context_mm.h"
-#include "theory/rewriterules/rr_inst_match_impl.h"
-#include "theory/rewriterules/rr_trigger.h"
-#include "theory/rewriterules/rr_inst_match.h"
#include "util/statistics_registry.h"
-#include "theory/rewriterules/theory_rewriterules_preprocess.h"
namespace CVC4 {
namespace theory {
namespace rewriterules {
-using namespace CVC4::theory::rrinst;
-typedef CVC4::theory::rrinst::Trigger Trigger;
-
-typedef std::hash_map<TNode, TNode, TNodeHashFunction> TCache;
-
- enum Answer {ATRUE, AFALSE, ADONTKNOW};
-
- class TheoryRewriteRules; /** forward */
-
- class RewriteRule{
- public:
- // constant
- const size_t id; //for debugging
- const bool d_split;
- mutable Trigger trigger;
- std::vector<Node> guards;
- mutable std::vector<Node> to_remove; /** terms to remove */
- const Node body;
- const TNode new_terms; /** new terms included in the body */
- std::vector<Node> free_vars; /* free variable in the rule */
- std::vector<Node> inst_vars; /* corresponding vars in the triggers */
- /* After instantiating the body new match can appear (TNode
- because is a subterm of a body on the assicaited rewrite
- rule) */
- typedef context::CDList< std::pair<TNode,RewriteRule* > > BodyMatch;
- mutable BodyMatch body_match;
- mutable ApplyMatcher * trigger_for_body_match; // used because we can be matching
- // trigger when we need new match.
- // So currently we use another
- // trigger for that.
-
- //context dependent
- typedef InstMatchTrie2<true> CacheNode;
- mutable CacheNode d_cache;
-
- const bool directrr;
-
- RewriteRule(TheoryRewriteRules & re,
- Trigger & tr, ApplyMatcher * tr2,
- std::vector<Node> & g, Node b, TNode nt,
- std::vector<Node> & fv,std::vector<Node> & iv,
- std::vector<Node> & to_r, bool drr);
- RewriteRule(const RewriteRule & r) CVC4_UNUSED;
- RewriteRule& operator=(const RewriteRule &) CVC4_UNUSED;
- ~RewriteRule();
-
- bool noGuard()const throw () { return guards.size() == 0; };
- bool inCache(TheoryRewriteRules & re, rrinst::InstMatch & im)const;
-
- void toStream(std::ostream& out) const;
-
- /* statistics */
- mutable size_t nb_matched;
- mutable size_t nb_applied;
- mutable size_t nb_propagated;
-
- };
-
- class RuleInst{
- public:
- /** The rule has at least one guard */
- const RewriteRule* rule;
-
- /** the substitution */
- std::vector<Node> subst;
-
- /** the term matched (not null if mono-pattern and direct-rr) */
- Node d_matched;
-
- /** Rule an instantiation with the given match */
- RuleInst(TheoryRewriteRules & re, const RewriteRule* r,
- std::vector<Node> & inst_subst,
- Node matched);
- RuleInst():rule(NULL){} // Dumb
-
- Node substNode(const TheoryRewriteRules & re, TNode r, TCache cache) const;
- size_t findGuard(TheoryRewriteRules & re, size_t start)const;
-
- void toStream(std::ostream& out) const;
-
- bool alreadyRewritten(TheoryRewriteRules & re) const;
- };
-
-/** A pair? */
- class Guarded {
- public:
- /** The backtracking is done somewhere else */
- const size_t d_guard; /* the id of the guard */
-
- /** The shared instantiation data */
- const RuleInst* inst;
-
- void nextGuard(TheoryRewriteRules & re)const;
-
- /** start indicate the first guard which is not true */
- Guarded(const RuleInst* ri, const size_t start);
- Guarded(const Guarded & g);
- /** Should be ssigned by a good garded after */
- Guarded();
-
- ~Guarded(){};
- void destroy(){};
- };
-
-template<class T>
-class CleanUpPointer{
-public:
- inline void operator()(T** e){
- delete(*e);
- };
-};
class TheoryRewriteRules : public Theory {
private:
KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::rewriterules::theoryTime");
-
- /** list of all rewrite rules */
- /* std::vector< Node > d_rules; */
- // typedef std::vector< std::pair<Node, Trigger > > Rules;
- typedef context::CDList< RewriteRule *,
- CleanUpPointer<RewriteRule >,
- std::allocator< RewriteRule * > > Rules;
- Rules d_rules;
- typedef context::CDList< RuleInst *,
- CleanUpPointer<RuleInst>,
- std::allocator< RuleInst * > > RuleInsts;
- RuleInsts d_ruleinsts;
-
- /** The GList* will lead too memory leaks since that doesn't use
- CDChunckList */
- typedef context::CDList< Guarded > GList;
- typedef context::CDHashMap<Node, GList *, NodeHashFunction> GuardedMap;
- GuardedMap d_guardeds;
-
- /* In order to not monopolize, the system slow down himself: If a
- guard stored in d_guardeds become true or false, it waits
- checkSlowdown(=10) checks before checking again if some guard take a
- value. At FULL_EFFORT regardless of d_checkLevel it check the
- guards
- */
- context::CDO<size_t> d_checkLevel;
-
- /** explanation */
- typedef context::CDHashMap<Node, RuleInst , NodeHashFunction> ExplanationMap;
- ExplanationMap d_explanations;
-
- /** new instantiation must be cleared at each conflict used only
- inside check */
- typedef std::vector< RuleInst* > QRuleInsts;
- QRuleInsts d_ruleinsts_to_add;
- bool d_ppAssert_on; //Indicate if a ppAssert have been done
-
public:
- /** true and false for predicate */
- Node d_true;
- Node d_false;
-
/** Constructs a new instance of TheoryRewriteRules
w.r.t. the provided context.*/
TheoryRewriteRules(context::Context* c,
return "THEORY_REWRITERULES";
}
- Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-
- bool ppDontRewriteSubterm(TNode atom) { return true; }
-
-
- private:
- void registerQuantifier( Node n );
-
- public:
- /* TODO modify when notification will be available */
- void notification( Node n, bool b);
-
- Trigger createTrigger( TNode n, std::vector<Node> & pattern );
-
- /** return if the guard (already substituted) is known true or false
- or unknown. In the last case it add the Guarded(rid,gid) to the watch
- list of this guard */
- Answer addWatchIfDontKnow(Node g, const RuleInst* r, const size_t gid);
-
- /** An instantiation of a rule is fired (all guards true) we
- propagate the body. That can be done by theory propagation if
- possible or by lemmas.
- */
- void propagateRule(const RuleInst * r, TCache cache);
-
- /** Auxiliary functions */
-private:
- /** A guard is verify, notify the Guarded */
- void notification(GList * const lpropa, bool b);
- /* If two guards becomes equals we should notify if one of them is
- already true */
- bool notifyIfKnown(const GList * const ltested, GList * const lpropa);
-
- void substGuards(const RuleInst * inst,
- TCache cache,
- NodeBuilder<> & conjunction);
-
- void addRewriteRule(const Node r);
- void computeMatchBody ( const RewriteRule * r, size_t start = 0);
- void addMatchRuleTrigger(const RewriteRule* r,
- rrinst::InstMatch & im, bool delay = true);
-
- Node normalizeConjunction(NodeBuilder<> & conjunction);
-
- /* rewrite pattern */
- typedef std::hash_map< Node, rewriter::RRPpRewrite*, NodeHashFunction > RegisterRRPpRewrite;
- RegisterRRPpRewrite d_registeredRRPpRewrite;
-
- bool addRewritePattern(TNode pattern, TNode body,
- rewriter::Subst & pvars,
- rewriter::Subst & vars);
-
- //create inst variable
- std::vector<Node> createInstVariable( Node r, std::vector<Node> & vars );
-
- /** statistics class */
- class Statistics {
- public:
- IntStat d_num_rewriterules;
- IntStat d_check;
- IntStat d_full_check;
- IntStat d_poll;
- IntStat d_match_found;
- IntStat d_cache_hit;
- IntStat d_cache_miss;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-
};/* class TheoryRewriteRules */
}/* CVC4::theory::rewriterules namespace */
namespace theory {
namespace rewriterules {
-class RewriteRuleTypeRule {
-public:
- /**
- * Compute the type for (and optionally typecheck) a term belonging
- * to the theory of rewriterules.
- *
- * @param nodeManager the NodeManager in use
- * @param n the node to compute the type of
- * @param check if true, the node's type should be checked as well
- * as computed.
- */
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
- bool check)
- throw(TypeCheckingExceptionPrivate) {
- Debug("typecheck-r") << "type check for rr " << n << std::endl;
- Assert(n.getKind() == kind::REWRITE_RULE && n.getNumChildren()==3 );
- if( check ){
- if( n[ 0 ].getType(check)!=nodeManager->boundVarListType() ){
- throw TypeCheckingExceptionPrivate(n[0],
- "first argument of rewrite rule is not bound var list");
- }
- if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
- throw TypeCheckingExceptionPrivate(n[1],
- "guard of rewrite rule is not an actual guard");
- }
- if( n[2].getType(check) !=
- TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE))){
- throw TypeCheckingExceptionPrivate(n[2],
- "not a correct rewrite rule");
- }
- }
- return nodeManager->booleanType();
- }
-};/* class RewriteRuleTypeRule */
-
-
-class RRRewriteTypeRule {
-public:
-
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw(TypeCheckingExceptionPrivate) {
- Assert(n.getKind() == kind::RR_REWRITE );
- if( check ){
- if( n[0].getType(check)!=n[1].getType(check) ){
- throw TypeCheckingExceptionPrivate(n,
- "terms of rewrite rule are not equal");
- }
- if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
- throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
- }
- if( n[0].getKind()!=kind::APPLY_UF ){
- throw TypeCheckingExceptionPrivate(n[0], "head of rewrite rules must start with an uninterpreted symbols. If you want to write a propagation rule, add the guard [true] for disambiguation");
- }
- }
- return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
- }
-};/* struct QuantifierReductionRuleRule */
-
-class RRRedDedTypeRule {
-public:
-
- inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw(TypeCheckingExceptionPrivate) {
- Assert(n.getKind() == kind::RR_REDUCTION ||
- n.getKind() == kind::RR_DEDUCTION );
- if( check ){
- if( n[ 0 ].getType(check)!=nodeManager->booleanType() ){
- throw TypeCheckingExceptionPrivate(n, "head of reduction rule is not boolean");
- }
- if( n[ 1 ].getType(check)!=nodeManager->booleanType() ){
- throw TypeCheckingExceptionPrivate(n, "body of reduction rule is not boolean");
- }
- if( n.getNumChildren() == 3 && n[2].getType(check)!=nodeManager->instPatternListType() ){
- throw TypeCheckingExceptionPrivate(n, "third argument of rewrite rule is not instantiation pattern list");
- }
- if( n.getNumChildren() < 3 && n[ 0 ] == nodeManager->mkConst<bool>(true) ){
- throw TypeCheckingExceptionPrivate(n, "A rewrite rule must have one head or one trigger at least");
- }
- }
- return TypeNode(nodeManager->mkTypeConst<TypeConstant>(RRHB_TYPE));
- }
-};/* struct QuantifierReductionRuleRule */
}/* CVC4::theory::rewriterules namespace */
}/* CVC4::theory namespace */
#include "theory/uf/equality_engine.h"
-#include "theory/rewriterules/efficient_e_matching.h"
+//#include "theory/rewriterules/efficient_e_matching.h"
#include "proof/proof_manager.h"
void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
//TODO: add notification to efficient E-matching
if( d_logicInfo.isQuantified() ){
- d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
+ //d_quantEngine->getEfficientEMatcher()->merge( t1, t2 );
if( options::quantConflictFind() ){
d_quantEngine->getConflictFind()->merge( t1, t2 );
}
(check-sat)
(pop)
-; EXPECT: sat
+; EXPECT: unknown
(push);;sat
(assert (and (not (R e1 e3)) (R e4 e1)))
(check-sat)
-CVC4_REGRESSION_ARGS ?= --efficient-e-matching
+CVC4_REGRESSION_ARGS ?= --rewrite-rules
export CVC4_REGRESSION_ARGS
# don't override a BINARY imported from a personal.mk
# put it below in "TESTS +="
TESTS = \
length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \
- datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \
- set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \
- reachability_back_to_the_future.smt2 native_arrays.smt2
-# reachability_bbttf_eT_arrays.smt2
+ datatypes.smt2 datatypes_sat.smt2 reachability_back_to_the_future.smt2 \
+ relation.smt2 simulate_rewriting.smt2 \
+ native_arrays.smt2
+
+# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2
EXTRA_DIST = $(TESTS)
;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
(set-logic AUFLIA)
-(set-info :status sat)
+(set-info :status unsat)
(declare-sort elt1 0)
(declare-sort elt2 0)
projects / cvc5.git / commitdiff