summaryrefslogtreecommitdiff
path: root/src/theory/uf/cardinality_extension.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/cardinality_extension.cpp')
-rw-r--r--src/theory/uf/cardinality_extension.cpp1884
1 files changed, 1884 insertions, 0 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
new file mode 100644
index 000000000..94e5f67c1
--- /dev/null
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -0,0 +1,1884 @@
+/********************* */
+/*! \file cardinality_extension.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of theory of UF with cardinality.
+ **/
+
+#include "theory/uf/cardinality_extension.h"
+
+#include "options/uf_options.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers_engine.h"
+#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 {
+
+/* These are names are unambigious are we use abbreviations. */
+typedef CardinalityExtension::SortModel SortModel;
+typedef SortModel::Region Region;
+typedef Region::RegionNodeInfo RegionNodeInfo;
+typedef RegionNodeInfo::DiseqList DiseqList;
+
+Region::Region(SortModel* cf, context::Context* c)
+ : d_cf( cf )
+ , d_testCliqueSize( c, 0 )
+ , d_splitsSize( c, 0 )
+ , d_testClique( c )
+ , d_splits( c )
+ , d_reps_size( c, 0 )
+ , d_total_diseq_external( c, 0 )
+ , d_total_diseq_internal( c, 0 )
+ , d_valid( c, true ) {}
+
+Region::~Region() {
+ for(iterator i = begin(), iend = end(); i != iend; ++i) {
+ RegionNodeInfo* regionNodeInfo = (*i).second;
+ delete regionNodeInfo;
+ }
+ d_nodes.clear();
+}
+
+void Region::addRep( Node n ) {
+ setRep( n, true );
+}
+
+void Region::takeNode( Region* r, Node n ){
+ Assert( !hasRep( n ) );
+ Assert( r->hasRep( n ) );
+ //add representative
+ setRep( n, true );
+ //take disequalities from r
+ RegionNodeInfo* rni = r->d_nodes[n];
+ for( int t=0; t<2; t++ ){
+ DiseqList* del = rni->get(t);
+ for(DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
+ if( (*it).second ){
+ r->setDisequal( n, (*it).first, t, false );
+ if( t==0 ){
+ if( hasRep( (*it).first ) ){
+ setDisequal( (*it).first, n, 0, false );
+ setDisequal( (*it).first, n, 1, true );
+ setDisequal( n, (*it).first, 1, true );
+ }else{
+ setDisequal( n, (*it).first, 0, true );
+ }
+ }else{
+ r->setDisequal( (*it).first, n, 1, false );
+ r->setDisequal( (*it).first, n, 0, true );
+ setDisequal( n, (*it).first, 0, true );
+ }
+ }
+ }
+ }
+ //remove representative
+ r->setRep( n, false );
+}
+
+void Region::combine( Region* r ){
+ //take all nodes from r
+ for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it) {
+ if( it->second->valid() ){
+ setRep( it->first, true );
+ }
+ }
+ for(Region::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it){
+ if( it->second->valid() ){
+ //take disequalities from r
+ Node n = it->first;
+ RegionNodeInfo* rni = it->second;
+ for( int t=0; t<2; t++ ){
+ RegionNodeInfo::DiseqList* del = rni->get(t);
+ for( RegionNodeInfo::DiseqList::iterator it2 = del->begin(),
+ it2end = del->end(); it2 != it2end; ++it2 ){
+ if( (*it2).second ){
+ if( t==0 && hasRep( (*it2).first ) ){
+ setDisequal( (*it2).first, n, 0, false );
+ setDisequal( (*it2).first, n, 1, true );
+ setDisequal( n, (*it2).first, 1, true );
+ }else{
+ setDisequal( n, (*it2).first, t, true );
+ }
+ }
+ }
+ }
+ }
+ }
+ r->d_valid = false;
+}
+
+/** setEqual */
+void Region::setEqual( Node a, Node b ){
+ Assert( hasRep( a ) && hasRep( b ) );
+ //move disequalities of b over to a
+ for( int t=0; t<2; t++ ){
+ DiseqList* del = d_nodes[b]->get(t);
+ for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
+ if( (*it).second ){
+ Node n = (*it).first;
+ //get the region that contains the endpoint of the disequality b != ...
+ Region* nr = d_cf->d_regions[ d_cf->d_regions_map[ n ] ];
+ if( !isDisequal( a, n, t ) ){
+ setDisequal( a, n, t, true );
+ nr->setDisequal( n, a, t, true );
+ }
+ setDisequal( b, n, t, false );
+ nr->setDisequal( n, b, t, false );
+ }
+ }
+ }
+ //remove b from representatives
+ setRep( b, false );
+}
+
+void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
+ //Debug("uf-ss-region-debug") << "set disequal " << n1 << " " << n2 << " "
+ // << type << " " << valid << std::endl;
+ //debugPrint("uf-ss-region-debug");
+ //Assert( isDisequal( n1, n2, type )!=valid );
+ if( isDisequal( n1, n2, type )!=valid ){ //DO_THIS: make assertion
+ d_nodes[ n1 ]->get(type)->setDisequal( n2, valid );
+ if( type==0 ){
+ d_total_diseq_external = d_total_diseq_external + ( valid ? 1 : -1 );
+ }else{
+ d_total_diseq_internal = d_total_diseq_internal + ( valid ? 1 : -1 );
+ if( valid ){
+ //if they are both a part of testClique, then remove split
+ if( d_testClique.find( n1 )!=d_testClique.end() && d_testClique[n1] &&
+ d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){
+ Node eq = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 );
+ if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){
+ Debug("uf-ss-debug") << "removing split for " << n1 << " " << n2
+ << std::endl;
+ d_splits[ eq ] = false;
+ d_splitsSize = d_splitsSize - 1;
+ }
+ }
+ }
+ }
+ }
+}
+
+void Region::setRep( Node n, bool valid ) {
+ Assert( hasRep( n )!=valid );
+ if( valid && d_nodes.find( n )==d_nodes.end() ){
+ d_nodes[n] = new RegionNodeInfo( d_cf->d_thss->getSatContext() );
+ }
+ d_nodes[n]->setValid(valid);
+ d_reps_size = d_reps_size + ( valid ? 1 : -1 );
+ //removing a member of the test clique from this region
+ if( d_testClique.find( n ) != d_testClique.end() && d_testClique[n] ){
+ Assert( !valid );
+ d_testClique[n] = false;
+ d_testCliqueSize = d_testCliqueSize - 1;
+ //remove all splits involving n
+ for( split_iterator it = begin_splits(); it != end_splits(); ++it ){
+ if( (*it).second ){
+ if( (*it).first[0]==n || (*it).first[1]==n ){
+ d_splits[ (*it).first ] = false;
+ d_splitsSize = d_splitsSize - 1;
+ }
+ }
+ }
+ }
+}
+
+bool Region::isDisequal( Node n1, Node n2, int type ) {
+ RegionNodeInfo::DiseqList* del = d_nodes[ n1 ]->get(type);
+ return del->isSet(n2) && del->getDisequalityValue(n2);
+}
+
+struct sortInternalDegree {
+ Region* r;
+ bool operator() (Node i, Node j) {
+ return (r->getRegionInfo(i)->getNumInternalDisequalities() >
+ r->getRegionInfo(j)->getNumInternalDisequalities());
+ }
+};
+
+struct sortExternalDegree {
+ Region* r;
+ bool operator() (Node i,Node j) {
+ return (r->getRegionInfo(i)->getNumExternalDisequalities() >
+ r->getRegionInfo(j)->getNumExternalDisequalities());
+ }
+};
+
+int gmcCount = 0;
+
+bool Region::getMustCombine( int cardinality ){
+ if (d_total_diseq_external >= static_cast<unsigned>(cardinality))
+ {
+ //The number of external disequalities is greater than or equal to
+ //cardinality. Thus, a clique of size cardinality+1 may exist
+ //between nodes in d_regions[i] and other regions Check if this is
+ //actually the case: must have n nodes with outgoing degree
+ //(cardinality+1-n) for some n>0
+ std::vector< int > degrees;
+ for( Region::iterator it = begin(); it != end(); ++it ){
+ RegionNodeInfo* rni = it->second;
+ if( rni->valid() ){
+ if( rni->getNumDisequalities() >= cardinality ){
+ int outDeg = rni->getNumExternalDisequalities();
+ if( outDeg>=cardinality ){
+ //we have 1 node of degree greater than (cardinality)
+ return true;
+ }else if( outDeg>=1 ){
+ degrees.push_back( outDeg );
+ if( (int)degrees.size()>=cardinality ){
+ //we have (cardinality) nodes of degree 1
+ return true;
+ }
+ }
+ }
+ }
+ }
+ gmcCount++;
+ if( gmcCount%100==0 ){
+ Trace("gmc-count") << gmcCount << " " << cardinality
+ << " sample : " << degrees.size() << std::endl;
+ }
+ //this should happen relatively infrequently....
+ std::sort( degrees.begin(), degrees.end() );
+ for( int i=0; i<(int)degrees.size(); i++ ){
+ if( degrees[i]>=cardinality+1-((int)degrees.size()-i) ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool Region::check( Theory::Effort level, int cardinality,
+ std::vector< Node >& clique ) {
+ if( d_reps_size>unsigned(cardinality) ){
+ if( d_total_diseq_internal==d_reps_size*( d_reps_size - 1 ) ){
+ if( d_reps_size>1 ){
+ //quick clique check, all reps form a clique
+ for( iterator it = begin(); it != end(); ++it ){
+ if( it->second->valid() ){
+ clique.push_back( it->first );
+ }
+ }
+ Trace("quick-clique") << "Found quick clique" << std::endl;
+ return true;
+ }else{
+ return false;
+ }
+ }
+ else if (level==Theory::EFFORT_FULL)
+ {
+ //build test clique, up to size cardinality+1
+ if( d_testCliqueSize<=unsigned(cardinality) ){
+ std::vector< Node > newClique;
+ if( d_testCliqueSize<unsigned(cardinality) ){
+ for( iterator it = begin(); it != end(); ++it ){
+ //if not in the test clique, add it to the set of new members
+ if( it->second->valid() &&
+ ( d_testClique.find( it->first ) == d_testClique.end() ||
+ !d_testClique[ it->first ] ) ){
+ //if( it->second->getNumInternalDisequalities()>cardinality ||
+ // level==Theory::EFFORT_FULL ){
+ newClique.push_back( it->first );
+ //}
+ }
+ }
+ //choose remaining nodes with the highest degrees
+ sortInternalDegree sidObj;
+ sidObj.r = this;
+ std::sort( newClique.begin(), newClique.end(), sidObj );
+ int offset = ( cardinality - d_testCliqueSize ) + 1;
+ newClique.erase( newClique.begin() + offset, newClique.end() );
+ }else{
+ //scan for the highest degree
+ int maxDeg = -1;
+ Node maxNode;
+ for( std::map< Node, RegionNodeInfo* >::iterator
+ it = d_nodes.begin(); it != d_nodes.end(); ++it ){
+ //if not in the test clique, add it to the set of new members
+ if( it->second->valid() &&
+ ( d_testClique.find( it->first )==d_testClique.end() ||
+ !d_testClique[ it->first ] ) ){
+ if( it->second->getNumInternalDisequalities()>maxDeg ){
+ maxDeg = it->second->getNumInternalDisequalities();
+ maxNode = it->first;
+ }
+ }
+ }
+ Assert( maxNode!=Node::null() );
+ newClique.push_back( maxNode );
+ }
+ //check splits internal to new members
+ for( int j=0; j<(int)newClique.size(); j++ ){
+ Debug("uf-ss-debug") << "Choose to add clique member "
+ << newClique[j] << std::endl;
+ for( int k=(j+1); k<(int)newClique.size(); k++ ){
+ if( !isDisequal( newClique[j], newClique[k], 1 ) ){
+ Node at_j = newClique[j];
+ Node at_k = newClique[k];
+ Node j_eq_k =
+ NodeManager::currentNM()->mkNode( EQUAL, at_j, at_k );
+ d_splits[ j_eq_k ] = true;
+ d_splitsSize = d_splitsSize + 1;
+ }
+ }
+ //check disequalities with old members
+ for( NodeBoolMap::iterator it = d_testClique.begin();
+ it != d_testClique.end(); ++it ){
+ if( (*it).second ){
+ if( !isDisequal( (*it).first, newClique[j], 1 ) ){
+ Node at_it = (*it).first;
+ Node at_j = newClique[j];
+ Node it_eq_j = at_it.eqNode(at_j);
+ d_splits[ it_eq_j ] = true;
+ d_splitsSize = d_splitsSize + 1;
+ }
+ }
+ }
+ }
+ //add new clique members to test clique
+ for( int j=0; j<(int)newClique.size(); j++ ){
+ d_testClique[ newClique[j] ] = true;
+ d_testCliqueSize = d_testCliqueSize + 1;
+ }
+ }
+ // Check if test clique has larger size than cardinality, and
+ // forms a clique.
+ if( d_testCliqueSize >= unsigned(cardinality+1) && d_splitsSize==0 ){
+ //test clique is a clique
+ for( NodeBoolMap::iterator it = d_testClique.begin();
+ it != d_testClique.end(); ++it ){
+ if( (*it).second ){
+ clique.push_back( (*it).first );
+ }
+ }
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+void Region::getNumExternalDisequalities(
+ std::map< Node, int >& num_ext_disequalities ){
+ for( Region::iterator it = begin(); it != end(); ++it ){
+ RegionNodeInfo* rni = it->second;
+ if( rni->valid() ){
+ DiseqList* del = rni->get(0);
+ for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
+ if( (*it2).second ){
+ num_ext_disequalities[ (*it2).first ]++;
+ }
+ }
+ }
+ }
+}
+
+void Region::debugPrint( const char* c, bool incClique ) {
+ Debug( c ) << "Num reps: " << d_reps_size << std::endl;
+ for( Region::iterator it = begin(); it != end(); ++it ){
+ RegionNodeInfo* rni = it->second;
+ if( rni->valid() ){
+ Node n = it->first;
+ Debug( c ) << " " << n << std::endl;
+ for( int i=0; i<2; i++ ){
+ Debug( c ) << " " << ( i==0 ? "Ext" : "Int" ) << " disequal:";
+ DiseqList* del = rni->get(i);
+ for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
+ if( (*it2).second ){
+ Debug( c ) << " " << (*it2).first;
+ }
+ }
+ Debug( c ) << ", total = " << del->size() << std::endl;
+ }
+ }
+ }
+ Debug( c ) << "Total disequal: " << d_total_diseq_external << " external,";
+ Debug( c ) << " " << d_total_diseq_internal << " internal." << std::endl;
+
+ if( incClique ){
+ if( !d_testClique.empty() ){
+ Debug( c ) << "Candidate clique members: " << std::endl;
+ Debug( c ) << " ";
+ for( NodeBoolMap::iterator it = d_testClique.begin();
+ it != d_testClique.end(); ++ it ){
+ if( (*it).second ){
+ Debug( c ) << (*it).first << " ";
+ }
+ }
+ Debug( c ) << ", size = " << d_testCliqueSize << std::endl;
+ }
+ if( !d_splits.empty() ){
+ Debug( c ) << "Required splits: " << std::endl;
+ Debug( c ) << " ";
+ for( NodeBoolMap::iterator it = d_splits.begin(); it != d_splits.end();
+ ++ it ){
+ if( (*it).second ){
+ Debug( c ) << (*it).first << " ";
+ }
+ }
+ Debug( c ) << ", size = " << d_splitsSize << std::endl;
+ }
+ }
+}
+
+SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
+ Node t, context::Context* satContext, Valuation valuation)
+ : DecisionStrategyFmf(satContext, valuation), d_cardinality_term(t)
+{
+}
+Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ return nm->mkNode(
+ CARDINALITY_CONSTRAINT, d_cardinality_term, nm->mkConst(Rational(i + 1)));
+}
+std::string SortModel::CardinalityDecisionStrategy::identify() const
+{
+ return std::string("uf_card");
+}
+
+SortModel::SortModel(Node n,
+ context::Context* c,
+ context::UserContext* u,
+ CardinalityExtension* thss)
+ : d_type(n.getType()),
+ d_thss(thss),
+ d_regions_index(c, 0),
+ d_regions_map(c),
+ d_split_score(c),
+ d_disequalities_index(c, 0),
+ d_reps(c, 0),
+ d_conflict(c, false),
+ d_cardinality(c, 1),
+ d_hasCard(c, false),
+ d_maxNegCard(c, 0),
+ d_initialized(u, false),
+ d_lemma_cache(u),
+ d_c_dec_strat(nullptr)
+{
+ d_cardinality_term = n;
+
+ if (options::ufssMode() == UF_SS_FULL)
+ {
+ // Register the strategy with the decision manager of the theory.
+ // We are guaranteed that the decision manager is ready since we
+ // construct this module during TheoryUF::finishInit.
+ d_c_dec_strat.reset(new CardinalityDecisionStrategy(
+ n, c, thss->getTheory()->getValuation()));
+ }
+}
+
+SortModel::~SortModel() {
+ for(std::vector<Region*>::iterator i = d_regions.begin();
+ i != d_regions.end(); ++i) {
+ Region* region = *i;
+ delete region;
+ }
+ d_regions.clear();
+}
+
+/** initialize */
+void SortModel::initialize( OutputChannel* out ){
+ if (d_c_dec_strat.get() != nullptr && !d_initialized)
+ {
+ d_initialized = true;
+ d_thss->getTheory()->getDecisionManager()->registerStrategy(
+ DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get());
+ }
+}
+
+/** new node */
+void SortModel::newEqClass( Node n ){
+ if( !d_conflict ){
+ 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, &d_thss->getOutputChannel() );
+ }
+ }
+ 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;
+ }
+ }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_thss->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_conflict ){
+ if( options::ufssTotality() ){
+ if( d_regions_map[b]==-1 ){
+ d_regions_map[a] = -1;
+ }
+ 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{
+ 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_conflict ){
+ 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 );
+ }
+ }
+ }
+ }
+}
+
+bool SortModel::areDisequal( Node a, Node b ) {
+ Assert(a == d_thss->getTheory()->getEqualityEngine()->getRepresentative(a));
+ Assert(b == d_thss->getTheory()->getEqualityEngine()->getRepresentative(b));
+ if( d_regions_map.find( a )!=d_regions_map.end() &&
+ d_regions_map.find( b )!=d_regions_map.end() ){
+ int ai = d_regions_map[a];
+ int bi = d_regions_map[b];
+ return d_regions[ai]->isDisequal(a, b, ai==bi ? 1 : 0);
+ }else{
+ return false;
+ }
+}
+
+/** check */
+void SortModel::check( Theory::Effort level, OutputChannel* out ){
+ Assert( options::ufssMode()==UF_SS_FULL );
+ if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
+ 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("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;
+ }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, out );
+ return;
+ }else{
+ Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
+ }
+ }
+ }
+ }
+ if( !applyTotality( d_cardinality ) ){
+ //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( 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], out );
+ if( sp==1 ){
+ addedLemma = true;
+#ifdef ONE_SPLIT_REGION
+ break;
+#endif
+ }else if( sp==-1 ){
+ check( level, out );
+ return;
+ }
+ }
+ }
+ }
+ //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;
+ 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]->valid() ){
+ Node op = d_regions[i]->frontKey();
+ int sort_id = d_thss->getSortInference()->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, out );
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+void SortModel::presolve() {
+ d_initialized = false;
+}
+
+void SortModel::propagate( Theory::Effort level, OutputChannel* out ){
+
+}
+
+int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
+ int ni = d_regions_map[n];
+ int counter = 0;
+ DiseqList* del = d_regions[ni]->getRegionInfo(n)->get(0);
+ for( DiseqList::iterator it = del->begin(); it != del->end(); ++it ){
+ if( (*it).second ){
+ if( d_regions_map[ (*it).first ]==ri ){
+ counter++;
+ }
+ }
+ }
+ return counter;
+}
+
+void SortModel::getDisequalitiesToRegions(int ri,
+ std::map< int, int >& regions_diseq)
+{
+ Region* region = d_regions[ri];
+ for(Region::iterator it = region->begin(); it != region->end(); ++it ){
+ if( it->second->valid() ){
+ DiseqList* del = it->second->get(0);
+ for( DiseqList::iterator it2 = del->begin(); it2 != del->end(); ++it2 ){
+ if( (*it2).second ){
+ Assert( isValid( d_regions_map[ (*it2).first ] ) );
+ //Notice() << "Found disequality with " << (*it2).first << ", region = " << d_regions_map[ (*it2).first ] << std::endl;
+ regions_diseq[ d_regions_map[ (*it2).first ] ]++;
+ }
+ }
+ }
+ }
+}
+
+void SortModel::setSplitScore( Node n, int s ){
+ if( d_split_score.find( n )!=d_split_score.end() ){
+ int ss = d_split_score[ n ];
+ d_split_score[ n ] = s>ss ? s : ss;
+ }else{
+ d_split_score[ n ] = s;
+ }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ setSplitScore( n[i], s+1 );
+ }
+}
+
+void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
+ if( !d_conflict ){
+ Trace("uf-ss-assert")
+ << "Assert cardinality " << d_type << " " << c << " " << val
+ << " level = "
+ << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl;
+ Assert( c>0 );
+ Node cl = getCardinalityLiteral( c );
+ if( val ){
+ bool doCheckRegions = !d_hasCard;
+ bool prevHasCard = d_hasCard;
+ d_hasCard = true;
+ if( !prevHasCard || c<d_cardinality ){
+ d_cardinality = c;
+ simpleCheckCardinality();
+ if( d_thss->d_conflict.get() ){
+ return;
+ }
+ }
+ //should check all regions now
+ if( doCheckRegions ){
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->valid() ){
+ checkRegion( i );
+ if( d_conflict ){
+ return;
+ }
+ }
+ }
+ }
+ // we assert it positively, if its beyond the bound, abort
+ if (options::ufssAbortCardinality() != -1
+ && c >= options::ufssAbortCardinality())
+ {
+ std::stringstream ss;
+ ss << "Maximum cardinality (" << options::ufssAbortCardinality()
+ << ") for finite model finding exceeded." << std::endl;
+ throw LogicException(ss.str());
+ }
+ }
+ else
+ {
+ if( c>d_maxNegCard.get() ){
+ Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type << " is now " << c << std::endl;
+ d_maxNegCard.set( c );
+ simpleCheckCardinality();
+ }
+ }
+ }
+}
+
+void SortModel::checkRegion( int ri, bool checkCombine ){
+ if( isValid(ri) && d_hasCard ){
+ Assert( d_cardinality>0 );
+ if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
+ ////alternatively, check if we can reduce the number of external disequalities by moving single nodes
+ //for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
+ // if( it->second ){
+ // int inDeg = d_regions[i]->d_disequalities_size[1][ it-> first ];
+ // int outDeg = d_regions[i]->d_disequalities_size[0][ it-> first ];
+ // if( inDeg<outDeg ){
+ // }
+ // }
+ //}
+ int riNew = forceCombineRegion( ri, true );
+ if( riNew>=0 ){
+ checkRegion( riNew, checkCombine );
+ }
+ }
+ //now check if region is in conflict
+ std::vector< Node > clique;
+ if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
+ //explain clique
+ addCliqueLemma( clique, &d_thss->getOutputChannel() );
+ }
+ }
+}
+
+int SortModel::forceCombineRegion( int ri, bool useDensity ){
+ if( !useDensity ){
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( ri!=i && d_regions[i]->valid() ){
+ return combineRegions( ri, i );
+ }
+ }
+ return -1;
+ }else{
+ //this region must merge with another
+ if( Debug.isOn("uf-ss-check-region") ){
+ Debug("uf-ss-check-region") << "We must combine Region #" << ri << ". " << std::endl;
+ d_regions[ri]->debugPrint("uf-ss-check-region");
+ }
+ //take region with maximum disequality density
+ double maxScore = 0;
+ int maxRegion = -1;
+ std::map< int, int > regions_diseq;
+ getDisequalitiesToRegions( ri, regions_diseq );
+ for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
+ Debug("uf-ss-check-region") << it->first << " : " << it->second << std::endl;
+ }
+ for( std::map< int, int >::iterator it = regions_diseq.begin(); it != regions_diseq.end(); ++it ){
+ Assert( it->first!=ri );
+ Assert( isValid( it->first ) );
+ Assert( d_regions[ it->first ]->getNumReps()>0 );
+ double tempScore = double(it->second)/double(d_regions[it->first]->getNumReps() );
+ if( tempScore>maxScore ){
+ maxRegion = it->first;
+ maxScore = tempScore;
+ }
+ }
+ if( maxRegion!=-1 ){
+ if( Debug.isOn("uf-ss-check-region") ){
+ Debug("uf-ss-check-region") << "Combine with region #" << maxRegion << ":" << std::endl;
+ d_regions[maxRegion]->debugPrint("uf-ss-check-region");
+ }
+ return combineRegions( ri, maxRegion );
+ }
+ return -1;
+ }
+}
+
+
+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];
+ for(Region::iterator it = region_bi->begin(); it != region_bi->end(); ++it){
+ Region::RegionNodeInfo* rni = it->second;
+ if( rni->valid() ){
+ d_regions_map[ it->first ] = ai;
+ }
+ }
+ //update regions disequal DO_THIS?
+ d_regions[ai]->combine( d_regions[bi] );
+ d_regions[bi]->setValid( false );
+ return ai;
+}
+
+void SortModel::moveNode( Node n, int ri ){
+ Debug("uf-ss-region") << "uf-ss: Move node " << n << " to Region #" << ri << std::endl;
+ Assert( isValid( d_regions_map[ n ] ) );
+ Assert( isValid( ri ) );
+ //move node to region ri
+ d_regions[ri]->takeNode( d_regions[ d_regions_map[n] ], n );
+ d_regions_map[n] = ri;
+}
+
+int SortModel::addSplit( Region* r, OutputChannel* out ){
+ Node s;
+ if( r->hasSplits() ){
+ //take the first split you find
+ for( Region::split_iterator it = r->begin_splits();
+ it != r->end_splits(); ++it ){
+ if( (*it).second ){
+ s = (*it).first;
+ break;
+ }
+ }
+ Assert( s!=Node::null() );
+ }
+ if (!s.isNull() ){
+ //add lemma to output channel
+ Assert( s.getKind()==EQUAL );
+ Node ss = Rewriter::rewrite( s );
+ if( ss.getKind()!=EQUAL ){
+ Node b_t = NodeManager::currentNM()->mkConst( true );
+ Node b_f = NodeManager::currentNM()->mkConst( false );
+ if( ss==b_f ){
+ Trace("uf-ss-lemma") << "....Assert disequal directly : "
+ << s[0] << " " << s[1] << std::endl;
+ assertDisequal( s[0], s[1], b_t );
+ return -1;
+ }else{
+ Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl;
+ }
+ if( ss==b_t ){
+ Message() << "Bad split " << s << std::endl;
+ AlwaysAssert(false);
+ }
+ }
+ if( options::sortInference()) {
+ for( int i=0; i<2; i++ ){
+ int si = d_thss->getSortInference()->getSortId( ss[i] );
+ Trace("uf-ss-split-si") << si << " ";
+ }
+ Trace("uf-ss-split-si") << std::endl;
+ }
+ //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
+ //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
+ //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
+ //Notice() << "*** Split on " << s << std::endl;
+ //split on the equality s
+ Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
+ if( doSendLemma( lem ) ){
+ Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
+ //tell the sat solver to explore the equals branch first
+ out->requirePhase( ss, true );
+ ++( d_thss->d_statistics.d_split_lemmas );
+ }
+ return 1;
+ }else{
+ return 0;
+ }
+}
+
+
+void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
+ Assert( d_hasCard );
+ Assert( d_cardinality>0 );
+ while( clique.size()>size_t(d_cardinality+1) ){
+ clique.pop_back();
+ }
+ // add as lemma
+ std::vector<Node> eqs;
+ for (unsigned i = 0, size = clique.size(); i < size; i++)
+ {
+ for (unsigned j = 0; j < i; j++)
+ {
+ eqs.push_back(clique[i].eqNode(clique[j]));
+ }
+ }
+ eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
+ Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
+ if (doSendLemma(lem))
+ {
+ Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl;
+ ++(d_thss->d_statistics.d_clique_lemmas);
+ }
+}
+
+void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
+ 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() ){
+ d_totality_lems[n].push_back( cardinality );
+ Node cardLit = d_cardinality_literal[ cardinality ];
+ int sort_id = 0;
+ if( options::sortInference() ){
+ sort_id = d_thss->getSortInference()->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_thss->getOutputChannel().lemma( lem );
+ }
+ }
+ }
+ }
+
+ std::vector< Node > eqs;
+ for( int i=0; i<use_cardinality; i++ ){
+ eqs.push_back( n.eqNode( getTotalityLemmaTerm( cardinality, i ) ) );
+ }
+ Node ax = NodeManager::currentNM()->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_thss->getOutputChannel().lemma( lem );
+ ++( 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() ),
+ getCardinalityLiteral( d_maxNegCard.get() ).negate() );
+ Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl;
+ d_thss->getOutputChannel().conflict( lem );
+ d_thss->d_conflict.set( true );
+ }
+}
+
+bool SortModel::doSendLemma( Node lem ) {
+ if( d_lemma_cache.find( lem )==d_lemma_cache.end() ){
+ d_lemma_cache[lem] = true;
+ d_thss->getOutputChannel().lemma( lem );
+ return true;
+ }else{
+ return false;
+ }
+}
+
+void SortModel::debugPrint( const char* c ){
+ if( Debug.isOn( c ) ){
+ Debug( c ) << "Number of reps = " << d_reps << std::endl;
+ Debug( c ) << "Cardinality req = " << d_cardinality << std::endl;
+ unsigned debugReps = 0;
+ for( unsigned i=0; i<d_regions_index; i++ ){
+ Region* region = d_regions[i];
+ if( region->valid() ){
+ Debug( c ) << "Region #" << i << ": " << std::endl;
+ region->debugPrint( c, true );
+ Debug( c ) << std::endl;
+ for( Region::iterator it = region->begin(); it != region->end(); ++it ){
+ if( it->second->valid() ){
+ if( d_regions_map[ it->first ]!=(int)i ){
+ Debug( c ) << "***Bad regions map : " << it->first
+ << " " << d_regions_map[ it->first ].get() << std::endl;
+ }
+ }
+ }
+ debugReps += region->getNumReps();
+ }
+ }
+
+ if( debugReps!=d_reps ){
+ Debug( c ) << "***Bad reps: " << d_reps << ", "
+ << "actual = " << debugReps << std::endl;
+ }
+ }
+}
+
+bool SortModel::debugModel( TheoryModel* m ){
+ if( Trace.isOn("uf-ss-warn") ){
+ std::vector< Node > eqcs;
+ eq::EqClassesIterator eqcs_i =
+ eq::EqClassesIterator(m->getEqualityEngine());
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ if( eqc.getType()==d_type ){
+ if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
+ eqcs.push_back( eqc );
+ //we must ensure that this equivalence class has been accounted for
+ if( d_regions_map.find( eqc )==d_regions_map.end() ){
+ Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
+ Trace("uf-ss-warn") << " type : " << d_type << std::endl;
+ Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl;
+ }
+ }
+ }
+ ++eqcs_i;
+ }
+ }
+ RepSet* rs = m->getRepSetPtr();
+ int nReps = (int)rs->getNumRepresentatives(d_type);
+ if( nReps!=(d_maxNegCard+1) ){
+ Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
+ Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard << std::endl;
+ Trace("uf-ss-warn") << " # Reps : " << nReps << std::endl;
+ if( d_maxNegCard>=nReps ){
+ while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){
+ std::stringstream ss;
+ ss << "r_" << d_type << "_";
+ Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" );
+ d_fresh_aloc_reps.push_back( nn );
+ }
+ if( d_maxNegCard==0 ){
+ rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]);
+ }else{
+ //must add lemma
+ std::vector< Node > force_cl;
+ for( int i=0; i<=d_maxNegCard; i++ ){
+ for( int j=(i+1); j<=d_maxNegCard; j++ ){
+ force_cl.push_back( d_fresh_aloc_reps[i].eqNode( d_fresh_aloc_reps[j] ).negate() );
+ }
+ }
+ Node cl = getCardinalityLiteral( d_maxNegCard );
+ Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkNode( AND, force_cl ) );
+ Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl;
+ d_thss->getOutputChannel().lemma( lem );
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+int SortModel::getNumRegions(){
+ int count = 0;
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->valid() ){
+ count++;
+ }
+ }
+ return count;
+}
+
+Node SortModel::getCardinalityLiteral(unsigned c)
+{
+ Assert(c > 0);
+ std::map<int, Node>::iterator itcl = d_cardinality_literal.find(c);
+ if (itcl != d_cardinality_literal.end())
+ {
+ return itcl->second;
+ }
+ // get the literal from the decision strategy
+ 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_thss->getOutputChannel().lemma(lem);
+ }
+ // 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, &d_thss->getOutputChannel());
+ }
+ return lit;
+}
+
+CardinalityExtension::CardinalityExtension(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ TheoryUF* th)
+ : d_out(&out),
+ d_th(th),
+ d_conflict(c, false),
+ d_rep_model(),
+ d_min_pos_com_card(c, -1),
+ d_cc_dec_strat(nullptr),
+ d_initializedCombinedCardinality(u, false),
+ d_card_assertions_eqv_lemma(u),
+ d_min_pos_tn_master_card(c, -1),
+ d_rel_eqc(c)
+{
+ if (options::ufssMode() == UF_SS_FULL && options::ufssFairness())
+ {
+ // Register the strategy with the decision manager of the theory.
+ // We are guaranteed that the decision manager is ready since we
+ // construct this module during TheoryUF::finishInit.
+ d_cc_dec_strat.reset(
+ new CombinedCardinalityDecisionStrategy(c, th->getValuation()));
+ }
+}
+
+CardinalityExtension::~CardinalityExtension()
+{
+ for (std::map<TypeNode, SortModel*>::iterator it = d_rep_model.begin();
+ it != d_rep_model.end(); ++it) {
+ delete it->second;
+ }
+}
+
+SortInference* CardinalityExtension::getSortInference()
+{
+ return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference();
+}
+
+/** get default sat context */
+context::Context* CardinalityExtension::getSatContext()
+{
+ return d_th->getSatContext();
+}
+
+/** get default output channel */
+OutputChannel& CardinalityExtension::getOutputChannel()
+{
+ return d_th->getOutputChannel();
+}
+
+/** ensure eqc */
+void CardinalityExtension::ensureEqc(SortModel* c, Node a)
+{
+ if( !hasEqc( a ) ){
+ d_rel_eqc[a] = true;
+ 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;
+ }
+}
+
+void CardinalityExtension::ensureEqcRec(Node n)
+{
+ if( !hasEqc( n ) ){
+ SortModel* c = getSortModel( n );
+ if( c ){
+ ensureEqc( c, n );
+ }
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ ensureEqcRec( n[i] );
+ }
+ }
+}
+
+/** has eqc */
+bool CardinalityExtension::hasEqc(Node a)
+{
+ NodeBoolMap::iterator it = d_rel_eqc.find( a );
+ return it!=d_rel_eqc.end() && (*it).second;
+}
+
+/** new node */
+void CardinalityExtension::newEqClass(Node a)
+{
+ 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
+ }
+}
+
+/** merge */
+void CardinalityExtension::merge(Node a, Node b)
+{
+ //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
+ }
+}
+
+/** assert terms are disequal */
+void CardinalityExtension::assertDisequal(Node a, Node b, Node reason)
+{
+ 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 );
+ Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal."
+ << std::endl;
+ }
+}
+
+/** assert a node */
+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()==UF_SS_FULL ){
+ if( lit.getKind()==CARDINALITY_CONSTRAINT ){
+ TypeNode tn = lit[0].getType();
+ Assert( tn.isSort() );
+ Assert( d_rep_model[tn] );
+ int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt();
+ Node ct = d_rep_model[tn]->getCardinalityTerm();
+ Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
+ if( lit[0]==ct ){
+ if( options::ufssFairnessMonotone() ){
+ Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
+ if( tn!=d_tn_mono_master ){
+ std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
+ if( it==d_tn_mono_slave.end() ){
+ bool isMonotonic;
+ if( d_th->getQuantifiersEngine() ){
+ isMonotonic = getSortInference()->isMonotonic( tn );
+ }else{
+ //if ground, everything is monotonic
+ isMonotonic = true;
+ }
+ if( isMonotonic ){
+ if( d_tn_mono_master.isNull() ){
+ Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
+ d_tn_mono_master = tn;
+ }else{
+ Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
+ d_tn_mono_slave[tn] = true;
+ }
+ }else{
+ Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl;
+ d_tn_mono_slave[tn] = false;
+ }
+ }
+ }
+ //set the minimum positive cardinality for master if necessary
+ if( polarity && tn==d_tn_mono_master ){
+ Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
+ if( d_min_pos_tn_master_card.get()==-1 || nCard<d_min_pos_tn_master_card.get() ){
+ d_min_pos_tn_master_card.set( nCard );
+ }
+ }
+ }
+ Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
+ d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
+ //check if combined cardinality is violated
+ checkCombinedCardinality();
+ }else{
+ //otherwise, make equal via lemma
+ if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
+ Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
+ eqv_lit = lit.eqNode( eqv_lit );
+ Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
+ getOutputChannel().lemma( eqv_lit );
+ d_card_assertions_eqv_lemma[lit] = true;
+ }
+ }
+ }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
+ if( polarity ){
+ //safe to assume int here
+ int nCard = lit[0].getConst<Rational>().getNumerator().getSignedInt();
+ if( d_min_pos_com_card.get()==-1 || nCard<d_min_pos_com_card.get() ){
+ d_min_pos_com_card.set( nCard );
+ checkCombinedCardinality();
+ }
+ }
+ }else{
+ if( Trace.isOn("uf-ss-warn") ){
+ ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
+ //// a theory propagation is not a decision.
+ if( isDecision ){
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ if( !it->second->hasCardinalityAsserted() ){
+ Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
+ //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
+ //Unimplemented();
+ }
+ }
+ }
+ }
+ }
+ }else{
+ if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
+ // cardinality constraint from user input, set incomplete
+ Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
+ d_out->setIncomplete();
+ }
+ }
+ Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
+}
+
+bool CardinalityExtension::areDisequal(Node a, Node b)
+{
+ if( a==b ){
+ return false;
+ }
+ eq::EqualityEngine* ee = d_th->getEqualityEngine();
+ a = ee->getRepresentative(a);
+ b = ee->getRepresentative(b);
+ if (ee->areDisequal(a, b, false))
+ {
+ return true;
+ }
+ SortModel* c = getSortModel(a);
+ if (c)
+ {
+ return c->areDisequal(a, b);
+ }
+ return false;
+}
+
+/** check */
+void CardinalityExtension::check(Theory::Effort level)
+{
+ if( !d_conflict ){
+ if( options::ufssMode()==UF_SS_FULL ){
+ Trace("uf-ss-solver")
+ << "CardinalityExtension: check " << level << std::endl;
+ if (level == Theory::EFFORT_FULL)
+ {
+ if (Debug.isOn("uf-ss-debug"))
+ {
+ debugPrint("uf-ss-debug");
+ }
+ if (Trace.isOn("uf-ss-state"))
+ {
+ Trace("uf-ss-state")
+ << "CardinalityExtension::check " << level << std::endl;
+ for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model)
+ {
+ Trace("uf-ss-state") << " " << rm.first << " has cardinality "
+ << rm.second->getCardinality() << std::endl;
+ }
+ }
+ }
+ 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() ){
+ d_conflict = true;
+ break;
+ }
+ }
+ }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){
+ if( level==Theory::EFFORT_FULL ){
+ // split on an equality between two equivalence classes (at most one per type)
+ std::map< TypeNode, std::vector< Node > > eqc_list;
+ std::map< TypeNode, bool > type_proc;
+ eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine());
+ while( !eqcs_i.isFinished() ){
+ Node a = *eqcs_i;
+ TypeNode tn = a.getType();
+ if( tn.isSort() ){
+ if( type_proc.find( tn )==type_proc.end() ){
+ std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn );
+ if( itel!=eqc_list.end() ){
+ for( unsigned j=0; j<itel->second.size(); j++ ){
+ Node b = itel->second[j];
+ if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){
+ Node eq = Rewriter::rewrite( a.eqNode( b ) );
+ Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
+ Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
+ d_out->lemma( lem );
+ d_out->requirePhase( eq, true );
+ type_proc[tn] = true;
+ break;
+ }
+ }
+ }
+ eqc_list[tn].push_back( a );
+ }
+ }
+ ++eqcs_i;
+ }
+ }
+ }else{
+ // unhandled uf ss mode
+ Assert( false );
+ }
+ Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level
+ << std::endl;
+ }
+}
+
+void CardinalityExtension::presolve()
+{
+ d_initializedCombinedCardinality = false;
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ it->second->presolve();
+ it->second->initialize( d_out );
+ }
+}
+
+CardinalityExtension::CombinedCardinalityDecisionStrategy::
+ CombinedCardinalityDecisionStrategy(context::Context* satContext,
+ Valuation valuation)
+ : DecisionStrategyFmf(satContext, valuation)
+{
+}
+Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
+ unsigned i)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ return nm->mkNode(COMBINED_CARDINALITY_CONSTRAINT, nm->mkConst(Rational(i)));
+}
+
+std::string
+CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
+{
+ return std::string("uf_combined_card");
+}
+
+void CardinalityExtension::preRegisterTerm(TNode n)
+{
+ if( options::ufssMode()==UF_SS_FULL ){
+ //initialize combined cardinality
+ initializeCombinedCardinality();
+
+ Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
+ //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
+ TypeNode tn = n.getType();
+ std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
+ if( it==d_rep_model.end() ){
+ SortModel* rm = NULL;
+ if( tn.isSort() ){
+ Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
+ rm = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
+ //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
+ }else{
+ /*
+ if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+ Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
+ Debug("uf-ss-na") << " (" << f << ")";
+ Debug("uf-ss-na") << std::endl;
+ Unimplemented("Cannot perform finite model finding on arithmetic quantifier");
+ }else if( tn.isDatatype() ){
+ Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
+ Debug("uf-ss-na") << " (" << f << ")";
+ Debug("uf-ss-na") << std::endl;
+ Unimplemented("Cannot perform finite model finding on datatype quantifier");
+ }
+ */
+ }
+ if( rm ){
+ rm->initialize( d_out );
+ d_rep_model[tn] = rm;
+ //d_rep_model_init[tn] = true;
+ }
+ }else{
+ //ensure sort model is initialized
+ it->second->initialize( d_out );
+ }
+ }
+}
+
+SortModel* CardinalityExtension::getSortModel(Node n)
+{
+ TypeNode tn = n.getType();
+ std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
+ //pre-register the type if not done already
+ if( it==d_rep_model.end() ){
+ preRegisterTerm( n );
+ it = d_rep_model.find( tn );
+ }
+ if( it!=d_rep_model.end() ){
+ return it->second;
+ }else{
+ return NULL;
+ }
+}
+
+/** get cardinality for sort */
+int CardinalityExtension::getCardinality(Node n)
+{
+ SortModel* c = getSortModel( n );
+ if( c ){
+ return c->getCardinality();
+ }else{
+ return -1;
+ }
+}
+
+int CardinalityExtension::getCardinality(TypeNode tn)
+{
+ std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
+ if( it!=d_rep_model.end() && it->second ){
+ return it->second->getCardinality();
+ }
+ return -1;
+}
+
+//print debug
+void CardinalityExtension::debugPrint(const char* c)
+{
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl;
+ it->second->debugPrint( c );
+ Debug( c ) << std::endl;
+ }
+}
+
+bool CardinalityExtension::debugModel(TheoryModel* m)
+{
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ if( !it->second->debugModel( m ) ){
+ return false;
+ }
+ }
+ return true;
+}
+
+/** initialize */
+void CardinalityExtension::initializeCombinedCardinality()
+{
+ if (d_cc_dec_strat.get() != nullptr
+ && !d_initializedCombinedCardinality.get())
+ {
+ d_initializedCombinedCardinality = true;
+ d_th->getDecisionManager()->registerStrategy(
+ DecisionManager::STRAT_UF_COMBINED_CARD, d_cc_dec_strat.get());
+ }
+}
+
+/** check */
+void CardinalityExtension::checkCombinedCardinality()
+{
+ Assert( options::ufssMode()==UF_SS_FULL );
+ if( options::ufssFairness() ){
+ Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
+ int totalCombinedCard = 0;
+ int maxMonoSlave = 0;
+ TypeNode maxSlaveType;
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+ int max_neg = it->second->getMaximumNegativeCardinality();
+ if( !options::ufssFairnessMonotone() ){
+ totalCombinedCard += max_neg;
+ }else{
+ std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
+ if( its==d_tn_mono_slave.end() || !its->second ){
+ totalCombinedCard += max_neg;
+ }else{
+ if( max_neg>maxMonoSlave ){
+ maxMonoSlave = max_neg;
+ maxSlaveType = it->first;
+ }
+ }
+ }
+ }
+ Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl;
+ if( options::ufssFairnessMonotone() ){
+ Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl;
+ if( d_min_pos_tn_master_card.get()!=-1 && maxMonoSlave>d_min_pos_tn_master_card.get() ){
+ int mc = d_min_pos_tn_master_card.get();
+ std::vector< Node > conf;
+ conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) );
+ conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() );
+ Node cf = NodeManager::currentNM()->mkNode( AND, conf );
+ Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict"
+ << " : " << cf << std::endl;
+ Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
+ << " : " << cf << std::endl;
+ getOutputChannel().conflict( cf );
+ d_conflict.set( true );
+ return;
+ }
+ }
+ int cc = d_min_pos_com_card.get();
+ if( cc !=-1 && totalCombinedCard > cc ){
+ //conflict
+ Node com_lit = d_cc_dec_strat->getLiteral(cc);
+ std::vector< Node > conf;
+ conf.push_back( com_lit );
+ int totalAdded = 0;
+ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin();
+ it != d_rep_model.end(); ++it ){
+ bool doAdd = true;
+ if( options::ufssFairnessMonotone() ){
+ std::map< TypeNode, bool >::iterator its =
+ d_tn_mono_slave.find( it->first );
+ if( its!=d_tn_mono_slave.end() && its->second ){
+ doAdd = false;
+ }
+ }
+ if( doAdd ){
+ int c = it->second->getMaximumNegativeCardinality();
+ if( c>0 ){
+ conf.push_back( it->second->getCardinalityLiteral( c ).negate() );
+ totalAdded += c;
+ }
+ if( totalAdded>cc ){
+ break;
+ }
+ }
+ }
+ Node cf = NodeManager::currentNM()->mkNode( AND, conf );
+ Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf
+ << std::endl;
+ Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
+ << std::endl;
+ getOutputChannel().conflict( cf );
+ d_conflict.set( true );
+ }
+ }
+}
+
+CardinalityExtension::Statistics::Statistics()
+ : 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);
+}
+
+CardinalityExtension::Statistics::~Statistics()
+{
+ 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);
+}
+
+}/* CVC4::theory namespace::uf */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback