return false;
}else{
EqualityQuery* q = qe->getEqualityQuery();
+ bool success = true;
//save previous match
InstMatch prev( &m );
//if t is null
<< 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 ){
return addedLemmas;
}
}
- m.clear();
}else{
addedLemmas++;
}
+ m.clear();
}
//return number of lemmas added
return addedLemmas;
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 );
}
d_op_selection_terms.clear();
}
+
+int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
+ /*
+ size_t maxChildren = 0;
+ for( size_t i=0; i<uf_terms.size(); i++ ){
+ if( uf_terms[i].getNumChildren()>maxChildren ){
+ 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
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<selectLitScore;
+ }
//see if we wish to choose this as a selection literal
d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
if( selectLit ){
+ selectLitScore = getSelectionScore( uf_terms );
Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
+ Trace("inst-gen-debug") << " flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
d_quant_selection_lit[f] = value ? n : n.notNode();
selectionLitTerms.clear();
selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
}
}else{
- Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals (is the body of f clausified?)" << std::endl;
+ Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
}
//process information about requirements and preferences of quantifier f
if( d_quant_sat.find( f )!=d_quant_sat.end() ){
std::map< Node, Node > 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 );
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; i<f[0].getNumChildren(); i++ ){
Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
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;
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
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
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
}
}
-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] );
}
}
}
}
}
-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;
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;
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{
}
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<COMPUTE_LAST; op++ ){
- if( doOperation( n, isNested, op ) ){
- Node prev2 = n;
- n = computeOperation( n, op );
- if( prev2!=n ){
- Trace("quantifiers-rewrite-op") << "Rewrite op " << op << ": rewrite " << prev2 << std::endl;
- Trace("quantifiers-rewrite-op") << " to " << std::endl;
- Trace("quantifiers-rewrite-op") << n << std::endl;
+Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& 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<body.getNumChildren(); i++ ){
+ std::vector< Node > activeArgs;
+ computeArgs( args, activeArgs, body[i] );
+ for (unsigned j=0; j<activeArgs.size(); j++ ){
+ varLits[activeArgs[j]].push_back( body[i] );
+ }
+ litVars[body[i]].insert( litVars[body[i]].begin(), activeArgs.begin(), activeArgs.end() );
+ }
+ //find the variable in the least number of literals
+ Node bestVar;
+ for( std::map< Node, std::vector< Node > >::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()<body.getNumChildren() ){
+ //we can miniscope
+ Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
+ //make the bodies
+ std::vector< Node > 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<body.getNumChildren(); i++ ){
+ if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
+ qlitt.push_back( body[i] );
+ }
+ }
+ //make the variable lists
+ std::vector< Node > qvl1;
+ std::vector< Node > qvl2;
+ std::vector< Node > qvsh;
+ for( unsigned i=0; i<args.size(); i++ ){
+ bool found1 = false;
+ bool found2 = false;
+ for( size_t j=0; j<varLits[args[i]].size(); j++ ){
+ if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
+ found1 = true;
+ }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
+ found2 = true;
+ }
+ if( found1 && found2 ){
+ break;
+ }
+ }
+ if( found1 ){
+ if( found2 ){
+ qvsh.push_back( args[i] );
+ }else{
+ qvl1.push_back( args[i] );
+ }
+ }else{
+ Assert(found2);
+ qvl2.push_back( args[i] );
+ }
+ }
+ Assert( !qvl1.empty() );
+ Assert( !qvl2.empty() || !qvsh.empty() );
+ //check for literals that only contain shared variables
+ std::vector< Node > qlitsh;
+ std::vector< Node > qlit2;
+ for( size_t i=0; i<qlitt.size(); i++ ){
+ bool hasVar2 = false;
+ for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
+ if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
+ hasVar2 = true;
+ break;
+ }
+ }
+ if( hasVar2 ){
+ qlit2.push_back( qlitt[i] );
+ }else{
+ qlitsh.push_back( qlitt[i] );
+ }
+ }
+ varLits.clear();
+ litVars.clear();
+ Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
+ Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
+ Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( 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();
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 ){
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,
//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 );
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;
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] ) ){
}
}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 );
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<eqc.size(); i++ ){
int score = getRepScore( eqc[i], f, index );
if( optInternalRepSortInference() ){
}
bool EqualityQueryQuantifiersEngine::optInternalRepSortInference() {
- return false;
+ return false; //shown to be not effective
}
\ No newline at end of file
if( !addedLemma ){
Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
Trace("uf-ss-si") << "Must combine region" << std::endl;
- if( true || !options::ufssColoringSat() ){
- bool recheck = false;
- //naive strategy, force region combination involving the first valid region
- if( options::sortInference()){
- 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 ) {
- 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 );
+ }
}
}
}
projects / cvc5.git / commitdiff