options::instWhenMode.set( INST_WHEN_LAST_CALL );
}
}
- if ( ! options::fmfInstGen.wasSetByUser()) {
- //if full model checking is on, disable inst-gen techniques
- if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
- options::fmfInstGen.set( false );
- }else{
- options::fmfInstGen.set( true );
- }
- }
if ( options::fmfBoundInt() ){
- if( options::mbqiMode()!=quantifiers::MBQI_NONE ){
+ if( options::mbqiMode()!=quantifiers::MBQI_NONE &&
+ options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){
//if bounded integers are set, must use full model check for MBQI
options::mbqiMode.set( quantifiers::MBQI_FMC );
}
// each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){
++d_eval_formulas;
- //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
+ Debug("fmf-eval-debug2") << "Evaluate " << n << std::endl;
//Notice() << "Eval " << n << std::endl;
if( n.getKind()==NOT ){
int val = evaluate( n[0], depIndex, ri );
d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
d_uf_model_gen[op].makeModel( this, d_eval_uf_model[n] );
//Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
- //d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
+ //d_eval_uf_model[n].debugPrint( std::cout, d_qe->getModel(), 2 );
}
}
}
void FirstOrderModelFmc::processInitialize( bool ispre ) {
if( ispre ){
- if( options::fmfFmcInterval() && intervalOp.isNull() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && intervalOp.isNull() ){
std::vector< TypeNode > types;
for(unsigned i=0; i<2; i++){
types.push_back(NodeManager::currentNM()->integerType());
Node FirstOrderModelFmc::getStarElement(TypeNode tn) {
Node st = getStar(tn);
- if( options::fmfFmcInterval() && tn.isInteger() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && tn.isInteger() ){
st = getInterval( st, st );
}
return st;
return true;
}
}
- if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){
+ if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){
//for star: check if all children are defined and have generalizations
- if( options::fmfFmcCoverSimplify() && c[index]==st ){
+ if( c[index]==st ){ ///options::fmfFmcCoverSimplify()
//check if all children exist and are complete
int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);
if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){
return d_data;
}else{
int minIndex = -1;
- if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){
for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
//if( !m->isInterval( it->first ) ){
// std::cout << "Not an interval during getGenIndex " << it->first << std::endl;
bool FullModelChecker::optBuildAtFullModel() {
//need to build after full model has taken effect if we are constructing interval models
// this is because we need to have a constant in all integer equivalence classes
- return options::fmfFmcInterval();
+ return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL;
}
void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl;
}
children.push_back(ri);
- if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){
+ if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
if (fm->isModelBasisTerm(ri) ) {
ri = fm->getStar( ri.getType() );
}else{
}
- if( options::fmfFmcInterval() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
convertIntervalModel( fm, op );
}
}
}else{
if( !v.isNull() ){
- if( options::fmfFmcInterval() && v.getType().isInteger() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && v.getType().isInteger() ){
for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {
if( fm->isInRange( v, it->first ) ){
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
Trace("fmc-debug3") << "isCompat " << c << std::endl;
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
- if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
Node iv = doIntervalMeet( fm, cond[i], c[i-1], false );
if( iv.isNull() ){
return 0;
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
if( cond[i]!=c[i-1] ) {
- if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){
Node iv = doIntervalMeet( fm, cond[i], c[i-1] );
if( !iv.isNull() ){
cond[i] = iv;
}
void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
- Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl;
+ Trace("fmc-debug") << "Make default vec, intervals = " << (options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl;
//get function symbol for f
cond.push_back(d_quant_cond[f]);
for (unsigned i=0; i<f[0].getNumChildren(); i++) {
++(d_statistics.d_num_quants_init);
}
//try to add it
- if( optInstGen() ){
- Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
- //add model basis instantiation
- if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
- d_quant_basis_match_added[f] = true;
- return 1;
- }else{
- //shouldn't happen usually, but will occur if x != y is a required literal for f.
- //Notice() << "No model basis for " << f << std::endl;
- d_quant_basis_match_added[f] = false;
- }
+ Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
+ //add model basis instantiation
+ if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){
+ d_quant_basis_match_added[f] = true;
+ return 1;
+ }else{
+ //shouldn't happen usually, but will occur if x != y is a required literal for f.
+ //Notice() << "No model basis for " << f << std::endl;
+ d_quant_basis_match_added[f] = false;
}
}
return 0;
//if evaluate(...)==1, then the instantiation is already true in the model
// depIndex is the index of the least significant variable that this evaluation relies upon
depIndex = riter.getNumTerms()-1;
+ Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl;
eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
if( eval==1 ){
Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
QuantifiersModule( qe ){
Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
- if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){
+ if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
Trace("model-engine-debug") << "...make fmc builder." << std::endl;
d_builder = new fmcheck::FullModelChecker( c, qe );
}else if( options::mbqiMode()==MBQI_INTERVAL ){
}
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
- int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1;
+ int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : 1;
for( int e=0; e<e_max; e++) {
if (d_addedLemmas==0) {
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
if( optOneQuantPerRound() && d_addedLemmas>0 ){
break;
}
+ }else{
+ Trace("inst-fmf-ei") << "-> Inactive : " << f << std::endl;
}
}
}
d_builder->d_addedLemmas = 0;
d_builder->d_incomplete_check = false;
if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
+ Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
d_triedLemmas += d_builder->d_triedLemmas;
d_addedLemmas += d_builder->d_addedLemmas;
d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
}else{
- Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
+ Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << 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 ) << " ";
/** mbqi from Section 5.4.2 of AJR thesis */
MBQI_FMC,
/** mbqi with integer intervals */
- //MBQI_FMC_INTERVAL,
+ MBQI_FMC_INTERVAL,
/** mbqi with interval abstraction of uninterpreted sorts */
MBQI_INTERVAL,
} MbqiMode;
option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
choose literal matching mode
-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 cbqi --enable-cbqi bool :default false
+ turns on counterexample-based quantifier instantiation
option recurseCbqi --cbqi-recurse bool :default false
turns on recursive counterexample-based quantifier instantiation
option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
choose mode for model-based quantifier instantiation
+option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
+ only add one instantiation per quantifier per round for mbqi
+option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
+ only add instantiations for one quantifier per round for mbqi
-option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
- disable simple models in full model check for finite model finding
-option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true
- disable covering simplification of fmc models
-option fmfFmcInterval --fmf-fmc-interval bool :default false
- construct interval models for fmc models
-
-option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
- only add one instantiation per quantifier per round for fmf
-option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false
- only add instantiations for one quantifier per round for fmf
option fmfInstEngine --fmf-inst-engine bool :default false
use instantiation engine in conjunction with finite model finding
option fmfRelevantDomain --fmf-relevant-domain bool :default false
use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
-option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
- enable Inst-Gen instantiation techniques for finite model finding (default)
-/disable Inst-Gen instantiation techniques for finite model finding
+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 fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
+ disable simple models in full model check for finite model finding
option fmfBoundInt --fmf-bound-int bool :default false
finite model finding on bounded integer quantification
+ Use instantiation algorithm that mimics Inst-Gen calculus. \n\
\n\
fmc \n\
-+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
Modulo Theories.\n\
\n\
+fmc-interval \n\
++ Same as fmc, but with intervals for models of integer functions.\n\
+\n\
interval \n\
+ Use algorithm that abstracts domain elements as intervals. \n\
\n\
return MBQI_INST_GEN;
} else if(optarg == "fmc") {
return MBQI_FMC;
+ } else if(optarg == "fmc-interval") {
+ return MBQI_FMC_INTERVAL;
} else if(optarg == "interval") {
return MBQI_INTERVAL;
} else if(optarg == "help") {
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
//the model object
- if( options::mbqiMode()==quantifiers::MBQI_FMC || options::fmfBoundInt() ){
+ if( options::mbqiMode()==quantifiers::MBQI_FMC ||
+ options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() ){
d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
}else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" );
disable region-based method for discovering cliques and splits in uf strong solver
option ufssEagerSplits --uf-ss-eager-split bool :default false
add splits eagerly for uf strong solver
-option ufssColoringSat --uf-ss-coloring-sat bool :default false
- use coloring-based SAT heuristic for uf strong solver
option ufssTotality --uf-ss-totality bool :default false
always use totality axioms for enforcing cardinality constraints
option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
-option ufssTotalityLazy --uf-ss-totality-lazy bool :default false
- apply totality axioms lazily
option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
apply symmetry breaking for totality axioms
option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
-option ufssSmartSplits --uf-ss-smart-split bool :default false
- use smart splitting heuristic for uf strong solver
option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
use explained clique lemmas for uf strong solver
option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
void StrongSolverTheoryUF::SortModel::newEqClass( Node n ){
if( !d_conflict ){
if( d_regions_map.find( n )==d_regions_map.end() ){
- if( !options::ufssTotalityLazy() ){
- //must generate totality axioms for every cardinality we have allocated thus far
- for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){
- if( applyTotality( it->first ) ){
- addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
- }
+ //must generate totality axioms for every cardinality we have allocated thus far
+ for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it != d_cardinality_literal.end(); ++it ){
+ if( applyTotality( it->first ) ){
+ addTotalityAxiom( n, it->first, &d_thss->getOutputChannel() );
}
}
if( options::ufssTotality() ){
d_regions_index = 0;
}
d_regions_map[n] = d_regions_index;
- if( options::ufssSmartSplits() ){
- setSplitScore( n, 0 );
- }
Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n << std::endl;
Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() << std::endl;
if( d_regions_index<d_regions.size() ){
}
}
}
- if( applyTotality( d_cardinality ) ){
- //add totality axioms for all nodes that have not yet been equated to cardinality terms
- if( options::ufssTotalityLazy() ){ //this should always be true
- if( level==Theory::EFFORT_FULL ){
- for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
- if( !options::ufssTotality() || d_regions_map[ (*it).first ]!=-1 ){
- addTotalityAxiom( (*it).first, d_cardinality, &d_thss->getOutputChannel() );
- }
- }
- }
- }
- }else{
+ if( !applyTotality( d_cardinality ) ){
//do splitting on demand
bool addedLemma = false;
if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
//out->propagateAsDecision( lem[0] );
d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality );
- if( applyTotality( d_aloc_cardinality ) && !options::ufssTotalityLazy() ){
+ if( applyTotality( d_aloc_cardinality ) ){
//must send totality axioms for each existing term
for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){
addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_thss->getOutputChannel() );
int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
Node s;
if( r->hasSplits() ){
- if( !options::ufssSmartSplits() ){
- //take the first split you find
- for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
- if( (*it).second ){
- s = (*it).first;
- break;
- }
- }
- }else{
- int maxScore = -1;
- std::vector< Node > splits;
- for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
- if( (*it).second ){
- int score1 = d_split_score[ (*it).first[0] ];
- int score2 = d_split_score[ (*it).first[1] ];
- int score = score1<score2 ? score1 : score2;
- if( score>maxScore ){
- maxScore = -1;
- s = (*it).first;
- }
- }
+ //take the first split you find
+ for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
+ if( (*it).second ){
+ s = (*it).first;
+ break;
}
}
Assert( s!=Node::null() );
StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c )
{
- if( options::ufssColoringSat() ){
- d_term_amb = new TermDisambiguator( th->getQuantifiersEngine(), c );
- }else{
- d_term_amb = NULL;
- }
if( options::ufssDiseqPropagation() ){
d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this );
}else{
if( level==Theory::EFFORT_FULL ){
debugPrint( "uf-ss-debug" );
}
- if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
- int lemmas = d_term_amb->disambiguateTerms( d_out );
- d_statistics.d_disamb_term_lemmas += lemmas;
- if( lemmas>=0 ){
- return;
- }
- }
for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
it->second->check( level, d_out );
if( it->second->isConflict() ){
if( !d_conflict && options::ufssSymBreak() ){
d_sym_break->check( level );
}
- //disambiguate terms if necessary
- //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
- // Assert( d_term_amb!=NULL );
- // d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
- //}
Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl;
}
}
}
-int TermDisambiguator::disambiguateTerms( OutputChannel* out ){
- Debug("uf-ss-disamb") << "Disambiguate terms." << std::endl;
- int lemmaAdded = 0;
- //otherwise, determine ambiguous pairs of ground terms for relevant sorts
- quantifiers::TermDb* db = d_qe->getTermDatabase();
- for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){
- Debug("uf-ss-disamb") << "Check " << it->first << std::endl;
- if( it->second.size()>1 ){
- if(involvesRelevantType( it->second[0] ) ){
- for( int i=0; i<(int)it->second.size(); i++ ){
- for( int j=(i+1); j<(int)it->second.size(); j++ ){
- Kind knd = it->second[i].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
- Node eq = NodeManager::currentNM()->mkNode( knd, it->second[i], it->second[j] );
- eq = Rewriter::rewrite(eq);
- //determine if they are ambiguous
- if( d_term_amb.find( eq )==d_term_amb.end() ){
- Debug("uf-ss-disamb") << "Check disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
- d_term_amb[ eq ] = true;
- //if they are equal
- if( d_qe->getEqualityQuery()->areEqual( it->second[i], it->second[j] ) ){
- d_term_amb[ eq ] = false;
- }else{
- //if an argument is disequal, then they are not ambiguous
- for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
- if( d_qe->getEqualityQuery()->areDisequal( it->second[i][k], it->second[j][k] ) ){
- d_term_amb[ eq ] = false;
- break;
- }
- }
- }
- if( d_term_amb[ eq ] ){
- Debug("uf-ss-disamb") << "Disambiguate " << it->second[i] << " " << it->second[j] << std::endl;
- //must add lemma
- std::vector< Node > children;
- children.push_back( eq );
- for( int k=0; k<(int)it->second[i].getNumChildren(); k++ ){
- Kind knd2 = it->second[i][k].getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL;
- Node eqc = NodeManager::currentNM()->mkNode( knd2, it->second[i][k], it->second[j][k] );
- children.push_back( eqc.notNode() );
- }
- Assert( children.size()>1 );
- Node lem = NodeManager::currentNM()->mkNode( OR, children );
- Trace( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
- //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
- out->lemma( lem );
- d_term_amb[ eq ] = false;
- lemmaAdded++;
- return lemmaAdded;
- }
- }
- }
- }
- }
- }
- }
- Debug("uf-ss-disamb") << "Done disambiguate terms. " << lemmaAdded << std::endl;
- return lemmaAdded;
-}
-
-bool TermDisambiguator::involvesRelevantType( Node n ){
- if( n.getKind()==APPLY_UF ){
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( n[i].getType().isSort() ){
- return true;
- }
- }
- }
- return false;
-}
-
DisequalityPropagator::DisequalityPropagator(QuantifiersEngine* qe, StrongSolverTheoryUF* ufss) :
d_qe(qe), d_ufss(ufss){
d_true = NodeManager::currentNM()->mkConst( true );
namespace uf {
class TheoryUF;
-class TermDisambiguator;
class DisequalityPropagator;
class StrongSolverTheoryUF{
/** check */
void checkCombinedCardinality();
private:
- /** term disambiguator */
- TermDisambiguator* d_term_amb;
/** disequality propagator */
DisequalityPropagator* d_deq_prop;
/** symmetry breaking techniques */
~StrongSolverTheoryUF() {}
/** get theory */
TheoryUF* getTheory() { return d_th; }
- /** term disambiguator */
- TermDisambiguator* getTermDisambiguator() { return d_term_amb; }
/** disequality propagator */
DisequalityPropagator* getDisequalityPropagator() { return d_deq_prop; }
/** symmetry breaker */
Statistics d_statistics;
};/* class StrongSolverTheoryUF */
-
-class TermDisambiguator
-{
-private:
- /** quantifiers engine */
- QuantifiersEngine* d_qe;
- /** whether two terms are ambiguous (indexed by equalities) */
- context::CDHashMap<Node, bool, NodeHashFunction> d_term_amb;
- /** involves relevant type */
- static bool involvesRelevantType( Node n );
-public:
- TermDisambiguator( QuantifiersEngine* qe, context::Context* c ) : d_qe( qe ), d_term_amb( c ){}
- ~TermDisambiguator(){}
- /** check ambiguous terms */
- int disambiguateTerms( OutputChannel* out );
-};
-
class DisequalityPropagator
{
private:
projects / cvc5.git / commitdiff