From 44d9a7c29f565dbba0baea3f9df23d6d3e5bd74f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 6 Mar 2013 10:46:07 -0600 Subject: [PATCH] fixed two bugs for the new E-matching implementation, added aggressive miniscoping option --ag-miniscope-quant, minor cleanup --- .../quantifiers/inst_match_generator.cpp | 45 ++-- src/theory/quantifiers/model_builder.cpp | 27 ++- src/theory/quantifiers/model_builder.h | 2 + src/theory/quantifiers/model_engine.cpp | 12 +- src/theory/quantifiers/options | 6 + .../quantifiers/quantifiers_rewriter.cpp | 211 +++++++++++------- src/theory/quantifiers/quantifiers_rewriter.h | 6 +- src/theory/quantifiers/term_database.cpp | 4 +- src/theory/quantifiers/trigger.cpp | 5 +- src/theory/quantifiers_engine.cpp | 4 +- src/theory/uf/theory_uf_strong_solver.cpp | 49 ++-- 11 files changed, 226 insertions(+), 145 deletions(-) diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 386834385..5484e25e9 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -144,6 +144,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi return false; }else{ EqualityQuery* q = qe->getEqualityQuery(); + bool success = true; //save previous match InstMatch prev( &m ); //if t is null @@ -162,33 +163,36 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi << m.get(d_match_pattern[i]) << std::endl; Debug("matching-fail") << "Match fail: " << m.get(d_match_pattern[i]) << " and " << t[i] << std::endl; - return false; + success = false; + break; } } }else{ if( !q->areEqual( d_match_pattern[i], t[i] ) ){ Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl; //ground arguments are not equal - return false; + success = false; + break; } } } - //now, fit children into match - //we will be requesting candidates for matching terms for each child - std::vector< Node > reps; - for( int i=0; i<(int)d_children.size(); i++ ){ - Node rep = q->getRepresentative( t[ d_children_index[i] ] ); - reps.push_back( rep ); - d_children[i]->reset( rep, qe ); - } - bool success = true; - if( d_next!=NULL ){ - success = d_next->getNextMatch( f, m, qe ); - }else{ - if( d_active_add ){ - Trace("active-add") << "Active Adding instantiation " << m << std::endl; - success = qe->addInstantiation( f, m ); - Trace("active-add") << "Success = " << success << std::endl; + if( success ){ + //now, fit children into match + //we will be requesting candidates for matching terms for each child + std::vector< Node > reps; + for( int i=0; i<(int)d_children.size(); i++ ){ + Node rep = q->getRepresentative( t[ d_children_index[i] ] ); + reps.push_back( rep ); + d_children[i]->reset( rep, qe ); + } + if( d_next!=NULL ){ + success = d_next->getNextMatch( f, m, qe ); + }else{ + if( d_active_add ){ + Trace("active-add") << "Active Adding instantiation " << m << std::endl; + success = qe->addInstantiation( f, m ); + Trace("active-add") << "Success = " << success << std::endl; + } } } if( !success ){ @@ -317,10 +321,10 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif return addedLemmas; } } - m.clear(); }else{ addedLemmas++; } + m.clear(); } //return number of lemmas added return addedLemmas; @@ -463,10 +467,11 @@ int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, Qu std::vector< InstMatch > newMatches; InstMatch m; while( d_children[i]->getNextMatch( f, m, qe ) ){ - m.makeRepresentative( qe ); + //m.makeRepresentative( qe ); newMatches.push_back( InstMatch( &m ) ); m.clear(); } + Debug("smart-multi-trigger") << "Made " << newMatches.size() << " new matches for index " << i << std::endl; for( int j=0; j<(int)newMatches.size(); j++ ){ processNewMatch( qe, newMatches[j], i, addedLemmas ); } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index d1c04ceab..d8b154b95 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -368,15 +368,32 @@ void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){ d_op_selection_terms.clear(); } + +int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { + /* + size_t maxChildren = 0; + for( size_t i=0; imaxChildren ){ + maxChildren = uf_terms[i].getNumChildren(); + } + } + //TODO: look at how many entries they have? + return (int)maxChildren; + */ + return 0; +} + void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; //the pro/con preferences for this quantifier std::vector< Node > pro_con[2]; //the terms in the selection literal we choose std::vector< Node > selectionLitTerms; + Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl; //for each asserted quantifier f, // - determine selection literals // - check which function/predicates have good and bad definitions for satisfying f + int selectLitScore = -1; QuantPhaseReq* qpr = d_qe->getPhaseRequirements( f ); for( std::map< Node, bool >::iterator it = qpr->d_phase_reqs.begin(); it != qpr->d_phase_reqs.end(); ++it ){ //the literal n is phase-required for quantifier f @@ -433,10 +450,18 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) selectLit = true; } } + //also check if it is naturally a better literal + if( !selectLit ){ + int score = getSelectionScore( uf_terms ); + //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl; + selectLit = score d_term_selection_lit; //map from operators to terms that appear in selection literals std::map< Node, std::vector< Node > > d_op_selection_terms; + //get selection score + int getSelectionScore( std::vector< Node >& uf_terms ); protected: //reset void reset( FirstOrderModel* fm ); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 39377d11c..1522d0828 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -224,7 +224,7 @@ int ModelEngine::checkModel( int checkOption ){ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ int addedLemmas = 0; - Debug("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl; + Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl; Debug("inst-fmf-ei") << " Instantiation Constants: "; for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; @@ -298,12 +298,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ relevantInst = relevantInst * (int)riter.d_domain[i].size(); } d_relevantLemmas += relevantInst; - Debug("inst-fmf-ei") << "Finished: " << std::endl; + Trace("inst-fmf-ei") << "Finished: " << std::endl; //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl; - Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; - Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; - Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl; + Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl; + Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl; + Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; + Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl; if( addedLemmas>1000 ){ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl; //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 6b204eb60..7a3687dd5 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -37,6 +37,9 @@ option cnfQuant --cnf-quant bool :default false option preSkolemQuant --pre-skolem-quant bool :default false apply skolemization eagerly to bodies of quantified formulas +# Whether to perform agressive miniscoping +option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false + perform aggressive miniscoping for quantifiers # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions @@ -65,6 +68,7 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false turns on counterexample-based quantifier instantiation [off by default] /turns off counterexample-based quantifier instantiation + option userPatternsQuant /--ignore-user-patterns bool :default true ignore user-provided patterns for quantifier instantiation @@ -94,6 +98,8 @@ option fmfInstGen /--disable-fmf-inst-gen bool :default true disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round +option fmfFreshDistConst --fmf-fresh-dc bool :default false + use fresh distinguished representative when applying Inst-Gen techniques option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" policy for instantiating axioms diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index dabaa2188..bf6a025f8 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -90,29 +90,15 @@ void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){ } } -void QuantifiersRewriter::computeArgs( std::map< Node, bool >& active, Node n ){ - if( active.find( n )!=active.end() ){ - active[n] = true; +void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, 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 ); + } }else{ for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeArgs( active, n[i] ); - } - } -} - -void QuantifiersRewriter::computeArgs( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n ){ - std::map< Node, bool > active; - for( int i=0; i<(int)args.size(); i++ ){ - active[ args[i] ] = false; - } - //Notice() << "For " << n << " : " << std::endl; - computeArgs( active, n ); - activeArgs.clear(); - for( std::map< Node, bool >::iterator it = active.begin(); it != active.end(); ++it ){ - Node n = it->first; - //Notice() << " " << it->first << " is " << it->second << std::endl; - if( it->second ){ //only add bound variables that occur in body - activeArgs.push_back( it->first ); + computeArgs( args, activeArgs, n[i] ); } } } @@ -468,37 +454,19 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui } } -Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq ){ +Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){ if( body.getKind()==FORALL ){ - if( pol==polReq ){ + if( pol ){ std::vector< Node > terms; std::vector< Node > subs; - if( polReq ){ - //for doing prenexing of same-signed quantifiers - //must rename each variable that already exists - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){ - terms.push_back( body[0][i] ); - subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); - } - args.insert( args.end(), subs.begin(), subs.end() ); - }else{ - std::vector< TypeNode > argTypes; - for( int i=0; i<(int)args.size(); i++ ){ - argTypes.push_back( args[i].getType() ); - } - //for doing pre-skolemization of opposite-signed quantifiers - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - terms.push_back( body[0][i] ); - //make the new function symbol - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, body[0][i].getType() ); - Node op = NodeManager::currentNM()->mkSkolem( "op_$$", typ, "was created by the quantifiers rewriter" ); - std::vector< Node > funcArgs; - funcArgs.push_back( op ); - funcArgs.insert( funcArgs.end(), args.begin(), args.end() ); - subs.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, funcArgs ) ); - } + //for doing prenexing of same-signed quantifiers + //must rename each variable that already exists + for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ + //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){ + terms.push_back( body[0][i] ); + subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); } + args.insert( args.end(), subs.begin(), subs.end() ); Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl; @@ -514,7 +482,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b std::vector< Node > newChildren; for( int i=0; i<(int)body.getNumChildren(); i++ ){ bool newPol = ( body.getKind()==NOT || ( body.getKind()==IMPLIES && i==0 ) ) ? !pol : pol; - Node n = computePrenex( body[i], args, newPol, polReq ); + Node n = computePrenex( body[i], args, newPol ); newChildren.push_back( n ); if( n!=body[i] ){ childrenChanged = true; @@ -549,10 +517,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){ if( computeOption==COMPUTE_MINISCOPING ){ //return directly return computeMiniscoping( args, n, ipl, f.hasAttribute(NestedQuantAttribute()) ); + }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ + return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) ); }else if( computeOption==COMPUTE_NNF ){ n = computeNNF( n ); - }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){ - n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX ); + }else if( computeOption==COMPUTE_PRENEX ){ + n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ Node prev; do{ @@ -670,42 +640,113 @@ Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node bo } return mkForAll( args, body, ipl ); } -/* -Node QuantifiersRewriter::rewriteQuants( Node n, bool isNested ){ - if( n.getKind()==FORALL ){ - return rewriteQuant( n, isNested ); - }else if( isLiteral( n ) ){ - return n; - }else{ - NodeBuilder<> tt(n.getKind()); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - tt << rewriteQuants( n[i], isNested ); - } - return tt.constructNode(); - } -} -Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested ){ - Node prev = n; - for( int op=0; op& args, Node body, bool isNested ){ + if( !isNested ){ + std::map< Node, std::vector< Node > > varLits; + std::map< Node, std::vector< Node > > litVars; + if( body.getKind()==OR ){ + Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl; + for( size_t i=0; i activeArgs; + computeArgs( args, activeArgs, body[i] ); + for (unsigned j=0; j >::iterator it = varLits.begin(); it != varLits.end(); ++it ){ + if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){ + bestVar = it->first; + } + } + Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl; + if( !bestVar.isNull() && varLits[bestVar].size() qlit1; + qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() ); + std::vector< Node > qlitt; + //for all literals not containing bestVar + for( size_t i=0; i qvl1; + std::vector< Node > qvl2; + std::vector< Node > qvsh; + for( unsigned i=0; i qlitsh; + std::vector< Node > qlit2; + for( size_t i=0; imkNode( OR, qlit1 ); + n1 = computeAggressiveMiniscoping( qvl1, n1 ); + qlitsh.push_back( n1 ); + if( !qlit2.empty() ){ + Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 ); + n2 = computeAggressiveMiniscoping( qvl2, n2 ); + qlitsh.push_back( n2 ); + } + Node n = NodeManager::currentNM()->mkNode( OR, qlitsh ); + if( !qvsh.empty() ){ + Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh); + n = NodeManager::currentNM()->mkNode( FORALL, bvl, n ); + } + Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl; + return n; } } } - if( prev==n ){ - return n; - }else{ - //rewrite again until fix point is reached - return rewriteQuant( n, isNested ); - } + return mkForAll( args, body, Node::null() ); } -*/ bool QuantifiersRewriter::doMiniscopingNoFreeVar(){ return options::miniscopeQuantFreeVar(); @@ -726,12 +767,12 @@ bool QuantifiersRewriter::doMiniscopingAnd(){ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption ){ if( computeOption==COMPUTE_MINISCOPING ){ return true; + }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ + return options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_NNF ){ return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities) - }else if( computeOption==COMPUTE_PRE_SKOLEM ){ - return false;//options::preSkolemQuant(); }else if( computeOption==COMPUTE_PRENEX ){ - return options::prenexQuant(); + return options::prenexQuant() && !options::aggressiveMiniscopeQuant(); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return options::varElimQuant(); }else if( computeOption==COMPUTE_CNF ){ diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 00301c610..75b392e15 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -41,19 +41,19 @@ private: static void computeArgs( 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 computeArgs( std::map< Node, bool >& active, Node n ); static Node computeClause( Node n ); private: static Node computeMiniscoping( 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 computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ); static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); - static Node computePrenex( Node body, std::vector< Node >& args, bool pol, bool polReq ); + static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); private: enum{ COMPUTE_MINISCOPING = 0, + COMPUTE_AGGRESSIVE_MINISCOPING, COMPUTE_NNF, - COMPUTE_PRE_SKOLEM, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, //COMPUTE_FLATTEN_ARGS_UF, diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 65624686a..f6518cfd3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -75,7 +75,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ //Call the children? if( inst::Trigger::isAtomicTrigger( n ) ){ if( !n.hasAttribute(InstConstantAttribute()) ){ - Debug("term-db") << "register trigger term " << n << std::endl; + Trace("term-db") << "register term in db " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; Node op = n.getOperator(); d_op_map[op].push_back( n ); @@ -194,7 +194,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ Node mbt; - if( d_type_map[ tn ].empty() ){ + if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){ std::stringstream ss; ss << Expr::setlanguage(options::outputLanguage()); ss << "e_" << tn; diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c4bc248d3..cff28f243 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -38,7 +38,8 @@ d_quantEngine( qe ), d_f( f ){ for( int i=0; i<(int)d_nodes.size(); i++ ){ Trace("trigger") << " " << d_nodes[i] << std::endl; } - Trace("trigger") << ", smart triggers = " << smartTriggers << std::endl; + Trace("trigger-debug") << ", smart triggers = " << smartTriggers; + Trace("trigger") << std::endl; if( smartTriggers ){ if( d_nodes.size()==1 ){ if( isSimpleTrigger( d_nodes[0] ) ){ @@ -49,6 +50,8 @@ d_quantEngine( qe ), d_f( f ){ } }else{ d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption ); + //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); + //d_mg->setActiveAdd(); } }else{ d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe ); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 50433facd..a11cc85c0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -616,7 +616,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, getEquivalenceClass( r, eqc ); //find best selection for representative Node r_best; - int r_best_score; + int r_best_score = -1; for( size_t i=0; i sortsFound; - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ - Node op = d_regions[i]->d_nodes.begin()->first; - int sort_id = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op) ; - if( sortsFound.find( sort_id )!=sortsFound.end() ){ - combineRegions( sortsFound[sort_id], i ); - recheck = true; - break; - }else{ - sortsFound[sort_id] = i; - } - } - } - } - if( !recheck ) { - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->d_valid ){ - forceCombineRegion( i, false ); + bool recheck = false; + if( options::sortInference()){ + //if sort inference is enabled, search for regions with same sort + std::map< int, int > sortsFound; + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + Node op = d_regions[i]->d_nodes.begin()->first; + int sort_id = d_thss->getTheory()->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op); + if( sortsFound.find( sort_id )!=sortsFound.end() ){ + combineRegions( sortsFound[sort_id], i ); recheck = true; break; + }else{ + sortsFound[sort_id] = i; } } } - if( recheck ){ - check( level, out ); + } + if( !recheck ) { + //naive strategy, force region combination involving the first valid region + for( int i=0; i<(int)d_regions_index; i++ ){ + if( d_regions[i]->d_valid ){ + forceCombineRegion( i, false ); + recheck = true; + break; + } } } + if( recheck ){ + check( level, out ); + } } } } -- 2.30.2