From 9b97c9144875e072da4098f102f8989be26e5cdf Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 28 Apr 2014 17:34:00 +0200 Subject: [PATCH] Optimizations for datatypes: check for clashes modulo equality. Avoid building model at fullModel=false when possible. Minor cleanup. --- src/theory/datatypes/theory_datatypes.cpp | 169 +++++++++++++++--- src/theory/datatypes/theory_datatypes.h | 11 +- src/theory/quantifiers/bounded_integers.h | 3 + src/theory/quantifiers/instantiation_engine.h | 2 + src/theory/quantifiers/model_engine.cpp | 104 ++++++----- src/theory/quantifiers/model_engine.h | 2 + src/theory/quantifiers/quant_conflict_find.h | 8 +- src/theory/quantifiers/rewrite_engine.h | 4 +- src/theory/quantifiers_engine.cpp | 8 + src/theory/quantifiers_engine.h | 2 + 10 files changed, 231 insertions(+), 82 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index eef25ca80..9316c3fe8 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -49,6 +49,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), d_labels( c ), d_selector_apps( c ), + d_consEqc( c ), d_conflict( c, false ), d_collectTermsCache( c ), d_consTerms( c ), @@ -59,6 +60,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); d_equalityEngine.addFunctionKind(kind::APPLY_UF); + + d_true = NodeManager::currentNM()->mkConst( true ); } TheoryDatatypes::~TheoryDatatypes() { @@ -99,6 +102,15 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake } } +TNode TheoryDatatypes::getEqcConstructor( TNode r ) { + EqcInfo * ei = getOrMakeEqcInfo( r, false ); + if( ei && !ei->d_constructor.get().isNull() ){ + return ei->d_constructor.get(); + }else{ + return r; + } +} + void TheoryDatatypes::check(Effort e) { Trace("datatypes-debug") << "Check effort " << e << std::endl; while(!done() && !d_conflict) { @@ -189,7 +201,7 @@ void TheoryDatatypes::check(Effort e) { if( dt.getNumConstructors()==1 ){ Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); d_pending.push_back( t ); - d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); + d_pending_exp[ t ] = d_true; Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; d_infer.push_back( t ); }else{ @@ -252,7 +264,7 @@ void TheoryDatatypes::flushPendingFacts(){ if( mustCommunicateFact( fact, exp ) ){ Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl; Node lem = fact; - if( exp.isNull() || exp==NodeManager::currentNM()->mkConst( true ) ){ + if( exp.isNull() || exp==d_true ){ lem = fact; }else{ Trace("dt-lemma-debug") << "Get explanation..." << std::endl; @@ -345,7 +357,7 @@ Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); tst = Rewriter::rewrite( tst ); Node n_ret; - if( tst==NodeManager::currentNM()->mkConst( true ) ){ + if( tst==d_true ){ n_ret = sel; }else{ if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){ @@ -424,7 +436,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ nn = NodeManager::currentNM()->mkConst(false); }else{ - nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : + nn = rew.size()==0 ? d_true : ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); } return nn; @@ -562,6 +574,14 @@ Node TheoryDatatypes::explain( TNode literal ){ return mkAnd( assumptions ); } +Node TheoryDatatypes::explain( std::vector< Node >& lits ) { + std::vector< TNode > assumptions; + for( unsigned i=0; id_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){ + Node deq = ei->d_constructor.get().eqNode( t ).negate(); + d_pending.push_back( deq ); + d_pending_exp[ deq ] = d_true; + Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl; + d_infer.push_back( deq ); + } + } + } + } +*/ + d_consEqc[t] = true; } } @@ -615,18 +654,20 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //if both have constructor, then either clash or unification if( !cons1.isNull() && !cons2.isNull() ){ Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl; - if( cons1.getOperator()!=cons2.getOperator() ){ + Node unifEq = cons1.eqNode( cons2 ); + std::vector< Node > exp; + if( checkClashModEq( cons1, cons2, exp ) ){ + exp.push_back( unifEq ); //check for clash - d_conflictNode = explain( cons1.eqNode( cons2 ) ); + d_conflictNode = explain( exp ); Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; return; }else{ //do unification - Node unifEq = cons1.eqNode( cons2 ); for( int i=0; i<(int)cons1.getNumChildren(); i++ ) { - if( cons1[i]!=cons2[i] ){ + if( !areEqual( cons1[i], cons2[i] ) ){ Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] ); d_pending.push_back( eq ); d_pending_exp[ eq ] = unifEq; @@ -634,19 +675,37 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ d_infer.push_back( eq ); d_infer_exp.push_back( unifEq ); } + } +/* + std::vector< Node > rew; + if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){ + Assert(false); + }else{ + for( unsigned i=0; id_inst && eqc2->d_inst ){ eqc1->d_inst = true; } - if( cons1.isNull() && !cons2.isNull() ){ - Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; - checkInst = true; - addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); - if( d_conflict ){ - return; + if( !cons2.isNull() ){ + if( cons1.isNull() ){ + Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; + checkInst = true; + addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); + if( d_conflict ){ + return; + } + d_consEqc[t1] = true; } + d_consEqc[t2] = false; } }else{ Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl; @@ -939,7 +998,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { //if( r!=rr ){ //Node eq_exp = NodeManager::currentNM()->mkConst(true); //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr ); - if( s!=rr ){ + if( s!=rr ){:: Node eq_exp = c.eqNode( s[0] ); Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); @@ -988,14 +1047,29 @@ void TheoryDatatypes::computeCareGraph(){ }else if( !areEqual( x, y ) ){ Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; //check if they are definately disequal - - if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES); - Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl; - //EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); - //if( eqStatus!=EQUALITY_UNKNOWN ){ - currentPairs.push_back(make_pair(x_shared, y_shared)); + bool defDiseq = false; +/* + TNode rx = getRepresentative( x ); + EqcInfo* eix = getOrMakeEqcInfo( rx, false ); + if( eix ){ + TNode ry = getRepresentative( y ); + EqcInfo* eiy = getOrMakeEqcInfo( ry, false ); + if( eiy ){ + if( !eix->d_constructor.get().isNull() && !eiy->d_constructor.get().isNull() ){ + defDiseq = eix->d_constructor.get().getOperator()!=eiy->d_constructor.get().getOperator(); + }else{ + } + } + } +*/ + if( !defDiseq && d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ + EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y); + if( eqStatus!=EQUALITY_UNKNOWN ){ + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES); + Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl; + currentPairs.push_back(make_pair(x_shared, y_shared)); + } } } } @@ -1234,7 +1308,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ if( rn!=n && !areEqual( rn, n ) ){ Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); d_pending.push_back( eq ); - d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); + d_pending_exp[ eq ] = d_true; Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl; d_infer.push_back( eq ); } @@ -1266,7 +1340,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ Node exp; Node tt; if( !eqc->d_constructor.get().isNull() ){ - exp = NodeManager::currentNM()->mkConst( true ); + exp = d_true; tt = eqc->d_constructor; }else{ exp = getLabel( n ); @@ -1622,7 +1696,7 @@ bool TheoryDatatypes::areDisequal( TNode a, TNode b ){ } } -Node TheoryDatatypes::getRepresentative( TNode a ){ +TNode TheoryDatatypes::getRepresentative( TNode a ){ if( hasTerm( a ) ){ return d_equalityEngine.getRepresentative( a ); }else{ @@ -1692,10 +1766,51 @@ void TheoryDatatypes::printModelDebug( const char* c ){ Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { if( assumptions.empty() ){ - return NodeManager::currentNM()->mkConst( true ); + return d_true; }else if( assumptions.size()==1 ){ return assumptions[0]; }else{ return NodeManager::currentNM()->mkNode( AND, assumptions ); } } + +bool TheoryDatatypes::checkClashModEq( Node n1, Node n2, std::vector< Node >& exp ) { + if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || + (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || + (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { + if( n1.getOperator() != n2.getOperator() ) { + return true; + } else { + Assert( n1.getNumChildren() == n2.getNumChildren() ); + for( int i=0; i<(int)n1.getNumChildren(); i++ ) { + TNode nc1 = n1[i]; + TNode nc2 = n2[i]; + if( DatatypesRewriter::isTermDatatype( n1[i] ) ){ + nc1 = getEqcConstructor( n1[i] ); + nc2 = getEqcConstructor( n2[i] ); + } + if( checkClashModEq( nc1, nc2, exp ) ) { + if( nc1!=n1[i] ){ + exp.push_back( nc1.eqNode( n1[i] ) ); + } + if( nc2!=n2[i] ){ + exp.push_back( nc2.eqNode( n2[i] ) ); + } + return true; + } + } + } + }else if( n1!=n2 ){ + if( n1.isConst() && n2.isConst() ){ + return true; + }else{ + Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); + if( d_equalityEngine.areDisequal( n1, n2, true ) ){ + exp.push_back( eq.negate() ); + return true; + } + } + } + return false; +} + diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index eb86c3f76..1c21c63b4 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -50,7 +50,7 @@ private: /** inferences */ NodeList d_infer; NodeList d_infer_exp; - + Node d_true; /** mkAnd */ Node mkAnd( std::vector< TNode >& assumptions ); private: @@ -156,6 +156,8 @@ private: NodeListMap d_labels; /** selector apps for eqch equivalence class */ NodeListMap d_selector_apps; + /** constructor terms */ + BoolMap d_consEqc; /** Are we in conflict */ context::CDO d_conflict; /** The conflict node */ @@ -183,6 +185,8 @@ private: EqcInfo* getOrMakeEqcInfo( Node n, bool doMake = false ); /** has eqc info */ bool hasEqcInfo( Node n ) { return d_labels.find( n )!=d_labels.end(); } + /** get eqc constructor */ + TNode getEqcConstructor( TNode r ); protected: /** compute care graph */ void computeCareGraph(); @@ -204,6 +208,7 @@ public: void explainPredicate( TNode p, bool polarity, std::vector& assumptions ); void explain( TNode literal, std::vector& assumptions ); Node explain( TNode literal ); + Node explain( std::vector< Node >& lits ); /** Conflict when merging two constants */ void conflict(TNode a, TNode b); /** called when a new equivalance class is created */ @@ -263,12 +268,14 @@ private: bool mustSpecifyAssignment(); /** must communicate fact */ bool mustCommunicateFact( Node n, Node exp ); + /** check clash mod eq */ + bool checkClashModEq( Node n1, Node n2, std::vector< Node >& exp ); private: //equality queries bool hasTerm( TNode a ); bool areEqual( TNode a, TNode b ); bool areDisequal( TNode a, TNode b ); - Node getRepresentative( TNode a ); + TNode getRepresentative( TNode a ); public: /** get equality engine */ eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 972bdb2ec..4130bffee 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -121,6 +121,9 @@ public: void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); bool isGroundRange(Node f, Node v); + + /** Identify this module */ + std::string identify() const { return "BoundedIntegers"; } }; } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 5f7e26297..394d53d42 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -150,6 +150,8 @@ public: ~Statistics(); }; Statistics d_statistics; + /** Identify this module */ + std::string identify() const { return "InstEngine"; } };/* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 8b62fc39b..d7b074acc 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -55,68 +55,74 @@ QuantifiersModule( qe ){ void ModelEngine::check( Theory::Effort e ){ if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ - FirstOrderModel* fm = d_quantEngine->getModel(); - //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers int addedLemmas = 0; - //quantifiers are initialized, we begin an instantiation round - double clSet = 0; - if( Trace.isOn("model-engine") ){ - clSet = double(clock())/double(CLOCKS_PER_SEC); - } - ++(d_statistics.d_inst_rounds); - bool buildAtFullModel = d_builder->optBuildAtFullModel(); - //two effort levels: first try exhaustive instantiation without axioms, then with. - int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; - for( int effort=startEffort; effort<2; effort++ ){ - // for effort = 0, we only instantiate non-axioms - // for effort = 1, we instantiate everything - if( addedLemmas==0 ){ - Trace("model-engine") << "---Model Engine Round---" << std::endl; - //initialize the model - Trace("model-engine-debug") << "Build model..." << std::endl; - d_builder->d_considerAxioms = effort>=1; - d_builder->d_addedLemmas = 0; - d_builder->buildModel( fm, buildAtFullModel ); - addedLemmas += (int)d_builder->d_addedLemmas; - //if builder has lemmas, add and return + bool needsBuild = true; + FirstOrderModel* fm = d_quantEngine->getModel(); + if( fm->getNumAssertedQuantifiers()>0 ){ + //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers + //quantifiers are initialized, we begin an instantiation round + double clSet = 0; + if( Trace.isOn("model-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + } + ++(d_statistics.d_inst_rounds); + bool buildAtFullModel = d_builder->optBuildAtFullModel(); + needsBuild = !buildAtFullModel; + //two effort levels: first try exhaustive instantiation without axioms, then with. + int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; + for( int effort=startEffort; effort<2; effort++ ){ + // for effort = 0, we only instantiate non-axioms + // for effort = 1, we instantiate everything if( addedLemmas==0 ){ - Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; - //let the strong solver verify that the model is minimal - //for debugging, this will if there are terms in the model that the strong solver was not notified of - if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){ - Trace("model-engine-debug") << "Check model..." << std::endl; - d_incomplete_check = false; - //print debug - Debug("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); - //successfully built an acceptable model, now check it - addedLemmas += checkModel(); - }else{ - addedLemmas++; + Trace("model-engine") << "---Model Engine Round---" << std::endl; + //initialize the model + Trace("model-engine-debug") << "Build model..." << std::endl; + d_builder->d_considerAxioms = effort>=1; + d_builder->d_addedLemmas = 0; + d_builder->buildModel( fm, buildAtFullModel ); + addedLemmas += (int)d_builder->d_addedLemmas; + //if builder has lemmas, add and return + if( addedLemmas==0 ){ + Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; + //let the strong solver verify that the model is minimal + //for debugging, this will if there are terms in the model that the strong solver was not notified of + if( ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm ) ){ + Trace("model-engine-debug") << "Check model..." << std::endl; + d_incomplete_check = false; + //print debug + Debug("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + //successfully built an acceptable model, now check it + addedLemmas += checkModel(); + }else{ + addedLemmas++; + } } } - } - if( addedLemmas==0 ){ - //if we have not added lemmas yet and axiomInstMode=trust, then we are done - if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ - //we must return unknown if an axiom is asserted - if( effort==0 ){ - d_incomplete_check = true; + if( addedLemmas==0 ){ + //if we have not added lemmas yet and axiomInstMode=trust, then we are done + if( options::axiomInstMode()==AXIOM_INST_MODE_TRUST ){ + //we must return unknown if an axiom is asserted + if( effort==0 ){ + d_incomplete_check = true; + } + break; } - break; } } - } - if( Trace.isOn("model-engine") ){ - double clSet2 = double(clock())/double(CLOCKS_PER_SEC); - Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + if( Trace.isOn("model-engine") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + } + }else{ + Trace("model-engine-debug") << "No quantified formulas asserted." << std::endl; } if( addedLemmas==0 ){ Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl; //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - if( options::produceModels() && !buildAtFullModel ){ + if( options::produceModels() && needsBuild ){ // finish building the model d_builder->buildModel( fm, true ); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index cf770a7b9..3b34f7504 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -68,6 +68,8 @@ public: ~Statistics(); }; Statistics d_statistics; + /** Identify this module */ + std::string identify() const { return "ModelEngine"; } };/* class ModelEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 62bd347c7..8a0d956ac 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -116,7 +116,7 @@ public: class QuantInfo { private: void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false ); - void flatten( Node n, bool beneathQuant ); + void flatten( Node n, bool beneathQuant ); private: //for completing match std::vector< int > d_unassigned; std::vector< TypeNode > d_unassigned_tn; @@ -156,8 +156,8 @@ public: bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false ); void revertMatch( std::vector< int >& assigned ); void debugPrintMatch( const char * c ); - bool isConstrainedVar( int v ); -public: + bool isConstrainedVar( int v ); +public: void getMatch( std::vector< Node >& terms ); }; @@ -274,6 +274,8 @@ public: ~Statistics(); }; Statistics d_statistics; + /** Identify this module */ + std::string identify() const { return "QcfEngine"; } }; } diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index f85803617..a16a6d598 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -56,7 +56,9 @@ public: void check( Theory::Effort e ); void registerQuantifier( Node f ); - void assertNode( Node n ); + void assertNode( Node n ); + /** Identify this module */ + std::string identify() const { return "RewriteEngine"; } }; } diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 63697f5e7..1837a34f4 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -166,6 +166,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl; return; } + Trace("quant-engine-debug") << "Resetting modules..." << std::endl; //reset relevant information d_hasAddedLemma = false; d_term_db->reset( e ); @@ -176,6 +177,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->reset_round( e ); } + Trace("quant-engine-debug") << "Done resetting modules." << std::endl; + if( e==Theory::EFFORT_LAST_CALL ){ //if effort is last call, try to minimize model first if( options::finiteModelFind() ){ @@ -188,14 +191,19 @@ void QuantifiersEngine::check( Theory::Effort e ){ }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); } + Trace("quant-engine-debug") << "Check with modules..." << std::endl; for( int i=0; i<(int)d_modules.size(); i++ ){ + Trace("quant-engine-debug") << "Check " << d_modules[i]->identify().c_str() << "..." << std::endl; d_modules[i]->check( e ); } + Trace("quant-engine-debug") << "Done check with modules." << std::endl; //build the model if not done so already // this happens if no quantifiers are currently asserted and no model-building module is enabled if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ if( options::produceModels() && !d_model->isModelSet() ){ + Trace("quant-engine-debug") << "Build the model..." << std::endl; d_te->getModelBuilder()->buildModel( d_model, true ); + Trace("quant-engine-debug") << "Done building the model." << std::endl; } if( Trace.isOn("inst-per-quant") ){ for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 858093543..e7843ab95 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -59,6 +59,8 @@ public: virtual void propagate( Theory::Effort level ){} virtual Node getNextDecisionRequest() { return TNode::null(); } virtual Node explain(TNode n) { return TNode::null(); } + /** Identify this module (for debugging, dynamic configuration, etc..) */ + virtual std::string identify() const = 0; };/* class QuantifiersModule */ namespace quantifiers { -- 2.30.2