#include "theory/quantifiers/term_database.h"
#include "theory/theory_model.h"
-//#define ONE_SPLIT_REGION
-//#define COMBINE_REGIONS_SMALL_INTO_LARGE
-//#define LAZY_REL_EQC
-
using namespace std;
using namespace CVC4::kind;
using namespace CVC4::context;
-
namespace CVC4 {
namespace theory {
namespace uf {
if (!d_state.isInConflict())
{
if( d_regions_map.find( n )==d_regions_map.end() ){
- // 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);
- }
- }
- if( options::ufssTotality() ){
- // Regions map will store whether we need to equate this term
- // with a constant equivalence class.
- if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
- d_regions_map[n] = 0;
- }else{
- d_regions_map[n] = -1;
- }
+ d_regions_map[n] = d_regions_index;
+ Debug("uf-ss") << "CardinalityExtension: 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())
+ {
+ d_regions[d_regions_index]->debugPrint("uf-ss-debug", true);
+ d_regions[d_regions_index]->setValid(true);
+ Assert(d_regions[d_regions_index]->getNumReps() == 0);
}else{
- d_regions_map[n] = d_regions_index;
- Debug("uf-ss") << "CardinalityExtension: 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() ){
- d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
- d_regions[ d_regions_index ]->setValid(true);
- Assert(d_regions[d_regions_index]->getNumReps() == 0);
- }else{
- d_regions.push_back(new Region(this, d_state.getSatContext()));
- }
- d_regions[ d_regions_index ]->addRep( n );
- d_regions_index = d_regions_index + 1;
+ d_regions.push_back(new Region(this, d_state.getSatContext()));
}
+ d_regions[d_regions_index]->addRep(n);
+ d_regions_index = d_regions_index + 1;
+
d_reps = d_reps + 1;
}
}
/** merge */
void SortModel::merge( Node a, Node b ){
- if (!d_state.isInConflict())
+ if (d_state.isInConflict())
+ {
+ return;
+ }
+ Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b << "..."
+ << std::endl;
+ if (a != b)
{
- if( options::ufssTotality() ){
- if( d_regions_map[b]==-1 ){
- d_regions_map[a] = -1;
+ Assert(d_regions_map.find(a) != d_regions_map.end());
+ Assert(d_regions_map.find(b) != d_regions_map.end());
+ int ai = d_regions_map[a];
+ int bi = d_regions_map[b];
+ Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
+ if (ai != bi)
+ {
+ if (d_regions[ai]->getNumReps() == 1)
+ {
+ int ri = combineRegions(bi, ai);
+ d_regions[ri]->setEqual(a, b);
+ checkRegion(ri);
}
- d_regions_map[b] = -1;
- }else{
- Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b
- << "..." << std::endl;
- if( a!=b ){
- Assert(d_regions_map.find(a) != d_regions_map.end());
- Assert(d_regions_map.find(b) != d_regions_map.end());
- int ai = d_regions_map[a];
- int bi = d_regions_map[b];
- Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
- if( ai!=bi ){
- if( d_regions[ai]->getNumReps()==1 ){
- int ri = combineRegions( bi, ai );
- d_regions[ri]->setEqual( a, b );
- checkRegion( ri );
- }else if( d_regions[bi]->getNumReps()==1 ){
- int ri = combineRegions( ai, bi );
- d_regions[ri]->setEqual( a, b );
- checkRegion( ri );
- }else{
- // Either move a to d_regions[bi], or b to d_regions[ai].
- RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
- RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
- int aex = ( a_region_info->getNumInternalDisequalities() -
- getNumDisequalitiesToRegion( a, bi ) );
- int bex = ( b_region_info->getNumInternalDisequalities() -
- getNumDisequalitiesToRegion( b, ai ) );
- // Based on which would produce the fewest number of
- // external disequalities.
- if( aex<bex ){
- moveNode( a, bi );
- d_regions[bi]->setEqual( a, b );
- }else{
- moveNode( b, ai );
- d_regions[ai]->setEqual( a, b );
- }
- checkRegion( ai );
- checkRegion( bi );
- }
+ else if (d_regions[bi]->getNumReps() == 1)
+ {
+ int ri = combineRegions(ai, bi);
+ d_regions[ri]->setEqual(a, b);
+ checkRegion(ri);
+ }
+ else
+ {
+ // Either move a to d_regions[bi], or b to d_regions[ai].
+ RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a);
+ RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b);
+ int aex = (a_region_info->getNumInternalDisequalities()
+ - getNumDisequalitiesToRegion(a, bi));
+ int bex = (b_region_info->getNumInternalDisequalities()
+ - getNumDisequalitiesToRegion(b, ai));
+ // Based on which would produce the fewest number of
+ // external disequalities.
+ if (aex < bex)
+ {
+ moveNode(a, bi);
+ d_regions[bi]->setEqual(a, b);
}else{
+ moveNode(b, ai);
d_regions[ai]->setEqual( a, b );
- checkRegion( ai );
}
- d_regions_map[b] = -1;
+ checkRegion(ai);
+ checkRegion(bi);
}
- d_reps = d_reps - 1;
}
+ else
+ {
+ d_regions[ai]->setEqual(a, b);
+ checkRegion(ai);
+ }
+ d_regions_map[b] = -1;
}
+ d_reps = d_reps - 1;
}
/** assert terms are disequal */
void SortModel::assertDisequal( Node a, Node b, Node reason ){
- if (!d_state.isInConflict())
+ if (d_state.isInConflict())
{
- if( options::ufssTotality() ){
- //do nothing
- }else{
- //if they are not already disequal
- eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine();
- a = ee->getRepresentative(a);
- b = ee->getRepresentative(b);
- int ai = d_regions_map[a];
- int bi = d_regions_map[b];
- if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){
- Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl;
- //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL ||
- // a!=reason[0][0] || b!=reason[0][1] ){
- // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl;
- //}
- Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl;
- //add to list of disequalities
- if( d_disequalities_index<d_disequalities.size() ){
- d_disequalities[d_disequalities_index] = reason;
- }else{
- d_disequalities.push_back( reason );
- }
- d_disequalities_index = d_disequalities_index + 1;
- //now, add disequalities to regions
- Assert(d_regions_map.find(a) != d_regions_map.end());
- Assert(d_regions_map.find(b) != d_regions_map.end());
- Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
- if( ai==bi ){
- //internal disequality
- d_regions[ai]->setDisequal( a, b, 1, true );
- d_regions[ai]->setDisequal( b, a, 1, true );
- checkRegion( ai, false ); //do not need to check if it needs to combine (no new ext. disequalities)
- }else{
- //external disequality
- d_regions[ai]->setDisequal( a, b, 0, true );
- d_regions[bi]->setDisequal( b, a, 0, true );
- checkRegion( ai );
- checkRegion( bi );
- }
- }
- }
+ return;
+ }
+ // if they are not already disequal
+ eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine();
+ a = ee->getRepresentative(a);
+ b = ee->getRepresentative(b);
+ int ai = d_regions_map[a];
+ int bi = d_regions_map[b];
+ if (d_regions[ai]->isDisequal(a, b, ai == bi))
+ {
+ // already disequal
+ return;
+ }
+ Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..."
+ << std::endl;
+ Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..."
+ << std::endl;
+ // add to list of disequalities
+ if (d_disequalities_index < d_disequalities.size())
+ {
+ d_disequalities[d_disequalities_index] = reason;
+ }
+ else
+ {
+ d_disequalities.push_back(reason);
+ }
+ d_disequalities_index = d_disequalities_index + 1;
+ // now, add disequalities to regions
+ Assert(d_regions_map.find(a) != d_regions_map.end());
+ Assert(d_regions_map.find(b) != d_regions_map.end());
+ Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl;
+ if (ai == bi)
+ {
+ // internal disequality
+ d_regions[ai]->setDisequal(a, b, 1, true);
+ d_regions[ai]->setDisequal(b, a, 1, true);
+ // do not need to check if it needs to combine (no new ext. disequalities)
+ checkRegion(ai, false);
+ }
+ else
+ {
+ // external disequality
+ d_regions[ai]->setDisequal(a, b, 0, true);
+ d_regions[bi]->setDisequal(b, a, 0, true);
+ checkRegion(ai);
+ checkRegion(bi);
}
}
}
}
-/** check */
void SortModel::check(Theory::Effort level)
{
Assert(options::ufssMode() == options::UfssMode::FULL);
- if (level >= Theory::EFFORT_STANDARD && d_hasCard && !d_state.isInConflict())
+ if (!d_hasCard && d_state.isInConflict())
{
- Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
- << std::endl;
+ // not necessary to check
+ return;
+ }
+ Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
+ << std::endl;
+ if (level == Theory::EFFORT_FULL)
+ {
+ Debug("fmf-full-check") << std::endl;
+ Debug("fmf-full-check")
+ << "Full check for SortModel " << d_type << ", status : " << std::endl;
+ debugPrint("fmf-full-check");
+ Debug("fmf-full-check") << std::endl;
+ }
+ if (d_reps <= (unsigned)d_cardinality)
+ {
+ Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type "
+ << d_type << ", <= " << d_cardinality << std::endl;
if( level==Theory::EFFORT_FULL ){
- Debug("fmf-full-check") << std::endl;
- Debug("fmf-full-check") << "Full check for SortModel " << d_type << ", status : " << std::endl;
- debugPrint("fmf-full-check");
- Debug("fmf-full-check") << std::endl;
+ Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type "
+ << d_type << ", <= " << d_cardinality << std::endl;
}
- if( d_reps<=(unsigned)d_cardinality ){
- Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
- if( level==Theory::EFFORT_FULL ){
- Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl;
- //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl;
- //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl;
- //Notice() << cardinality << " ";
+ return;
+ }
+ // first check if we can generate a clique conflict
+ // do a check within each region
+ for (size_t i = 0; i < d_regions_index; i++)
+ {
+ if (d_regions[i]->valid())
+ {
+ std::vector<Node> clique;
+ if (d_regions[i]->check(level, d_cardinality, clique))
+ {
+ // add clique lemma
+ addCliqueLemma(clique);
+ return;
}
- return;
- }else{
- //first check if we can generate a clique conflict
- if( !options::ufssTotality() ){
- //do a check within each region
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->valid() ){
- std::vector< Node > clique;
- if( d_regions[i]->check( level, d_cardinality, clique ) ){
- //add clique lemma
- addCliqueLemma(clique);
- return;
- }else{
- Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
- }
- }
+ else
+ {
+ Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
+ }
+ }
+ }
+ // do splitting on demand
+ bool addedLemma = false;
+ if (level == Theory::EFFORT_FULL)
+ {
+ Trace("uf-ss-debug") << "Add splits?" << std::endl;
+ // see if we have any recommended splits from large regions
+ for (size_t i = 0; i < d_regions_index; i++)
+ {
+ if (d_regions[i]->valid() && d_regions[i]->getNumReps() > d_cardinality)
+ {
+ int sp = addSplit(d_regions[i]);
+ if (sp == 1)
+ {
+ addedLemma = true;
+ }
+ else if (sp == -1)
+ {
+ check(level);
+ return;
}
}
- if( !applyTotality( d_cardinality ) ){
- //do splitting on demand
- bool addedLemma = false;
- if (level==Theory::EFFORT_FULL)
+ }
+ }
+ // If no added lemmas, force continuation via combination of regions.
+ if (level != Theory::EFFORT_FULL || addedLemma)
+ {
+ return;
+ }
+ // check at full effort
+ Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
+ Trace("uf-ss-si") << "Must combine region" << std::endl;
+ bool recheck = false;
+ SortInference* si = d_thss->getSortInference();
+ if (si != nullptr)
+ {
+ // If sort inference is enabled, search for regions with same sort.
+ std::map<int, int> sortsFound;
+ for (size_t i = 0; i < d_regions_index; i++)
+ {
+ if (d_regions[i]->valid())
+ {
+ Node op = d_regions[i]->frontKey();
+ int sort_id = si->getSortId(op);
+ if (sortsFound.find(sort_id) != sortsFound.end())
{
- Trace("uf-ss-debug") << "Add splits?" << std::endl;
- //see if we have any recommended splits from large regions
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
- int sp = addSplit(d_regions[i]);
- if( sp==1 ){
- addedLemma = true;
-#ifdef ONE_SPLIT_REGION
- break;
-#endif
- }else if( sp==-1 ){
- check(level);
- return;
- }
- }
- }
+ Debug("fmf-full-check") << "Combined regions " << i << " "
+ << sortsFound[sort_id] << std::endl;
+ combineRegions(sortsFound[sort_id], i);
+ recheck = true;
+ break;
}
- //If no added lemmas, force continuation via combination of regions.
- if( level==Theory::EFFORT_FULL ){
- if( !addedLemma ){
- Trace("uf-ss-debug") << "No splits added. " << d_cardinality
- << std::endl;
- Trace("uf-ss-si") << "Must combine region" << std::endl;
- bool recheck = false;
- SortInference* si = d_thss->getSortInference();
- if (si != nullptr)
- {
- //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]->valid() ){
- Node op = d_regions[i]->frontKey();
- int sort_id = si->getSortId(op);
- if( sortsFound.find( sort_id )!=sortsFound.end() ){
- Debug("fmf-full-check") << "Combined regions " << i << " " << sortsFound[sort_id] << std::endl;
- combineRegions( sortsFound[sort_id], i );
- recheck = true;
- break;
- }else{
- sortsFound[sort_id] = i;
- }
- }
- }
- }
- 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]->valid() ){
- int fcr = forceCombineRegion( i, false );
- Debug("fmf-full-check") << "Combined regions " << i << " " << fcr << std::endl;
- Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
- recheck = true;
- break;
- }
- }
- }
- if( recheck ){
- Trace("uf-ss-debug") << "Must recheck." << std::endl;
- check(level);
- }
- }
+ else
+ {
+ sortsFound[sort_id] = i;
}
}
}
}
+ if (!recheck)
+ {
+ // naive strategy, force region combination involving the first
+ // valid region
+ for (size_t i = 0; i < d_regions_index; i++)
+ {
+ if (d_regions[i]->valid())
+ {
+ int fcr = forceCombineRegion(i, false);
+ Debug("fmf-full-check")
+ << "Combined regions " << i << " " << fcr << std::endl;
+ Trace("uf-ss-debug")
+ << "Combined regions " << i << " " << fcr << std::endl;
+ recheck = true;
+ break;
+ }
+ }
+ }
+ if (recheck)
+ {
+ Trace("uf-ss-debug") << "Must recheck." << std::endl;
+ check(level);
+ }
}
void SortModel::presolve() {
int SortModel::combineRegions( int ai, int bi ){
-#ifdef COMBINE_REGIONS_SMALL_INTO_LARGE
- if( d_regions[ai]->getNumReps()<d_regions[bi]->getNumReps() ){
- return combineRegions( bi, ai );
- }
-#endif
Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl;
Assert(isValid(ai) && isValid(bi));
Region* region_bi = d_regions[bi];
}
}
-void SortModel::addTotalityAxiom(Node n, int cardinality)
-{
- if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){
- if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){
- NodeManager* nm = NodeManager::currentNM();
- d_totality_lems[n].push_back( cardinality );
- Node cardLit = d_cardinality_literal[ cardinality ];
- int sort_id = 0;
- SortInference* si = d_thss->getSortInference();
- if (si != nullptr)
- {
- sort_id = si->getSortId(n);
- }
- Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl;
- int use_cardinality = cardinality;
- if( options::ufssTotalitySymBreak() ){
- if( d_sym_break_index.find(n)!=d_sym_break_index.end() ){
- use_cardinality = d_sym_break_index[n];
- }else if( (int)d_sym_break_terms[n.getType()][sort_id].size()<cardinality-1 ){
- use_cardinality = d_sym_break_terms[n.getType()][sort_id].size() + 1;
- d_sym_break_terms[n.getType()][sort_id].push_back( n );
- d_sym_break_index[n] = use_cardinality;
- Trace("uf-ss-totality") << "Allocate symmetry breaking term " << n << ", index = " << use_cardinality << std::endl;
- if( d_sym_break_terms[n.getType()][sort_id].size()>1 ){
- //enforce canonicity
- for( int i=2; i<use_cardinality; i++ ){
- //can only be assigned to domain constant d if someone has been assigned domain constant d-1
- Node eq = n.eqNode( getTotalityLemmaTerm( cardinality, i ) );
- std::vector< Node > eqs;
- for( unsigned j=0; j<(d_sym_break_terms[n.getType()][sort_id].size()-1); j++ ){
- eqs.push_back( d_sym_break_terms[n.getType()][sort_id][j].eqNode( getTotalityLemmaTerm( cardinality, i-1 ) ) );
- }
- Node ax = eqs.size()==1 ? eqs[0] : NodeManager::currentNM()->mkNode( OR, eqs );
- Node lem = NodeManager::currentNM()->mkNode( IMPLIES, eq, ax );
- Trace("uf-ss-lemma") << "*** Add (canonicity) totality axiom " << lem << std::endl;
- d_im.lemma(lem, LemmaProperty::NONE, false);
- }
- }
- }
- }
-
- std::vector< Node > eqs;
- for( int i=0; i<use_cardinality; i++ ){
- eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
- }
- Node ax = eqs.size() == 1 ? eqs[0] : nm->mkNode(OR, eqs);
- Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax );
- Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl;
- //send as lemma to the output channel
- d_im.lemma(lem, LemmaProperty::NONE, false);
- ++( d_thss->d_statistics.d_totality_lemmas );
- }
- }
-}
-
-/** apply totality */
-bool SortModel::applyTotality( int cardinality ){
- return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
-}
-
-/** get totality lemma terms */
-Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){
- return d_totality_terms[0][i];
-}
-
void SortModel::simpleCheckCardinality() {
if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()<d_maxNegCard.get() ){
Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ),
return count;
}
-Node SortModel::getCardinalityLiteral(unsigned c)
+Node SortModel::getCardinalityLiteral(size_t c)
{
Assert(c > 0);
- std::map<int, Node>::iterator itcl = d_cardinality_literal.find(c);
+ std::map<size_t, Node>::iterator itcl = d_cardinality_literal.find(c);
if (itcl != d_cardinality_literal.end())
{
return itcl->second;
Node lit = d_c_dec_strat->getLiteral(c - 1);
d_cardinality_literal[c] = lit;
- // Since we are reasoning about cardinality c, we invoke a totality axiom
- if (!applyTotality(c))
- {
- // return if we are not using totality axioms
- return lit;
- }
-
- NodeManager* nm = NodeManager::currentNM();
- Node var;
- if (c == 1 && !options::ufssTotalitySymBreak())
- {
- // get arbitrary ground term
- var = d_cardinality_term;
- }
- else
- {
- std::stringstream ss;
- ss << "_c_" << c;
- var = nm->mkSkolem(ss.str(), d_type, "is a cardinality lemma term");
- }
- if ((c - 1) < d_totality_terms[0].size())
- {
- d_totality_terms[0][c - 1] = var;
- }
- else
- {
- d_totality_terms[0].push_back(var);
- }
- // must be distinct from all other cardinality terms
- for (unsigned i = 1, size = d_totality_terms[0].size(); i < size; i++)
- {
- Node lem = var.eqNode(d_totality_terms[0][i - 1]).notNode();
- Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem
- << std::endl;
- d_im.lemma(lem, LemmaProperty::NONE, false);
- }
- // 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, c);
- }
+ // return the literal
return lit;
}
{
SortModel* c = getSortModel( a );
if( c ){
-#ifdef LAZY_REL_EQC
- //do nothing
-#else
Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : "
<< a.getType() << std::endl;
c->newEqClass( a );
Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class."
<< std::endl;
-#endif
}
}
//TODO: ensure they are relevant
SortModel* c = getSortModel( a );
if( c ){
-#ifdef LAZY_REL_EQC
- ensureEqc( c, a );
- if( hasEqc( b ) ){
- Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
- << " : " << a.getType() << std::endl;
- c->merge( a, b );
- Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
- }else{
- //c->assignEqClass( b, a );
- d_rel_eqc[b] = true;
- }
-#else
Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b
<< " : " << a.getType() << std::endl;
c->merge( a, b );
Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl;
-#endif
}
}
{
SortModel* c = getSortModel( a );
if( c ){
-#ifdef LAZY_REL_EQC
- ensureEqc( c, a );
- ensureEqc( c, b );
-#endif
Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a
<< " " << b << " : " << a.getType() << std::endl;
c->assertDisequal( a, b, reason );
void CardinalityExtension::assertNode(Node n, bool isDecision)
{
Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
-#ifdef LAZY_REL_EQC
- ensureEqcRec( n );
-#endif
bool polarity = n.getKind() != kind::NOT;
TNode lit = polarity ? n : n[0];
if (options::ufssMode() == options::UfssMode::FULL)
: d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
- d_disamb_term_lemmas("CardinalityExtension::Disambiguate_Term_Lemmas", 0),
- d_totality_lemmas("CardinalityExtension::Totality_Lemmas", 0),
d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
{
smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
smtStatisticsRegistry()->registerStat(&d_split_lemmas);
- smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas);
- smtStatisticsRegistry()->registerStat(&d_totality_lemmas);
smtStatisticsRegistry()->registerStat(&d_max_model_size);
}
smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas);
smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
}
projects / cvc5.git / commitdiff