summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/theory_inference_manager.cpp2
-rw-r--r--src/theory/theory_inference_manager.h5
-rw-r--r--src/theory/uf/cardinality_extension.cpp204
-rw-r--r--src/theory/uf/cardinality_extension.h51
-rw-r--r--src/theory/uf/theory_uf.cpp10
5 files changed, 115 insertions, 157 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index ff6f0ebc7..81f5c45e6 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -464,5 +464,7 @@ void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
d_out.safePoint(r);
}
+void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); }
+
} // namespace theory
} // namespace CVC4
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 496a7f0f1..e63d55366 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -341,6 +341,11 @@ class TheoryInferenceManager
* Forward to OutputChannel::safePoint() to spend resources.
*/
void safePoint(ResourceManager::Resource r);
+ /**
+ * Notification from a theory that it realizes it is incomplete at
+ * this context level.
+ */
+ void setIncomplete();
protected:
/**
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 1f83c94d6..b35efc23a 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -183,7 +183,7 @@ void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
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] = new RegionNodeInfo(d_cf->d_state.getSatContext());
}
d_nodes[n]->setValid(valid);
d_reps_size = d_reps_size + ( valid ? 1 : -1 );
@@ -460,22 +460,22 @@ std::string SortModel::CardinalityDecisionStrategy::identify() const
}
SortModel::SortModel(Node n,
- context::Context* c,
- context::UserContext* u,
+ TheoryState& state,
+ TheoryInferenceManager& im,
CardinalityExtension* thss)
: d_type(n.getType()),
+ d_state(state),
+ d_im(im),
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_regions_index(d_state.getSatContext(), 0),
+ d_regions_map(d_state.getSatContext()),
+ d_split_score(d_state.getSatContext()),
+ d_disequalities_index(d_state.getSatContext(), 0),
+ d_reps(d_state.getSatContext(), 0),
+ d_cardinality(d_state.getSatContext(), 1),
+ d_hasCard(d_state.getSatContext(), false),
+ d_maxNegCard(d_state.getSatContext(), 0),
+ d_initialized(d_state.getUserContext(), false),
d_c_dec_strat(nullptr)
{
d_cardinality_term = n;
@@ -486,7 +486,7 @@ SortModel::SortModel(Node n,
// 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()));
+ n, d_state.getSatContext(), thss->getTheory()->getValuation()));
}
}
@@ -500,7 +500,8 @@ SortModel::~SortModel() {
}
/** initialize */
-void SortModel::initialize( OutputChannel* out ){
+void SortModel::initialize()
+{
if (d_c_dec_strat.get() != nullptr && !d_initialized)
{
d_initialized = true;
@@ -513,14 +514,15 @@ void SortModel::initialize( OutputChannel* out ){
/** new node */
void SortModel::newEqClass( Node n ){
- if( !d_conflict ){
+ 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, &d_thss->getOutputChannel() );
+ addTotalityAxiom(n, it->first);
}
}
if( options::ufssTotality() ){
@@ -542,7 +544,7 @@ void SortModel::newEqClass( Node n ){
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.push_back(new Region(this, d_state.getSatContext()));
}
d_regions[ d_regions_index ]->addRep( n );
d_regions_index = d_regions_index + 1;
@@ -554,7 +556,8 @@ void SortModel::newEqClass( Node n ){
/** merge */
void SortModel::merge( Node a, Node b ){
- if( !d_conflict ){
+ if (!d_state.isInConflict())
+ {
if( options::ufssTotality() ){
if( d_regions_map[b]==-1 ){
d_regions_map[a] = -1;
@@ -611,7 +614,8 @@ void SortModel::merge( Node a, Node b ){
/** assert terms are disequal */
void SortModel::assertDisequal( Node a, Node b, Node reason ){
- if( !d_conflict ){
+ if (!d_state.isInConflict())
+ {
if( options::ufssTotality() ){
//do nothing
}else{
@@ -670,9 +674,11 @@ bool SortModel::areDisequal( Node a, Node b ) {
}
/** check */
-void SortModel::check( Theory::Effort level, OutputChannel* out ){
+void SortModel::check(Theory::Effort level)
+{
Assert(options::ufssMode() == options::UfssMode::FULL);
- if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
+ if (level >= Theory::EFFORT_STANDARD && d_hasCard && !d_state.isInConflict())
+ {
Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
<< std::endl;
if( level==Theory::EFFORT_FULL ){
@@ -699,7 +705,7 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
std::vector< Node > clique;
if( d_regions[i]->check( level, d_cardinality, clique ) ){
//add clique lemma
- addCliqueLemma( clique, out );
+ addCliqueLemma(clique);
return;
}else{
Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
@@ -716,15 +722,14 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
//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 );
+ int sp = addSplit(d_regions[i]);
if( sp==1 ){
addedLemma = true;
#ifdef ONE_SPLIT_REGION
break;
#endif
}else if( sp==-1 ){
- check( level, out );
+ check(level);
return;
}
}
@@ -771,7 +776,7 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
}
if( recheck ){
Trace("uf-ss-debug") << "Must recheck." << std::endl;
- check( level, out );
+ check(level);
}
}
}
@@ -784,10 +789,6 @@ 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;
@@ -832,8 +833,10 @@ void SortModel::setSplitScore( Node n, int s ){
}
}
-void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
- if( !d_conflict ){
+void SortModel::assertCardinality(int c, bool val)
+{
+ if (!d_state.isInConflict())
+ {
Trace("uf-ss-assert")
<< "Assert cardinality " << d_type << " " << c << " " << val
<< " level = "
@@ -847,7 +850,8 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
if( !prevHasCard || c<d_cardinality ){
d_cardinality = c;
simpleCheckCardinality();
- if( d_thss->d_conflict.get() ){
+ if (d_state.isInConflict())
+ {
return;
}
}
@@ -856,7 +860,8 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
for( int i=0; i<(int)d_regions_index; i++ ){
if( d_regions[i]->valid() ){
checkRegion( i );
- if( d_conflict ){
+ if (d_state.isInConflict())
+ {
return;
}
}
@@ -905,7 +910,7 @@ void SortModel::checkRegion( int ri, bool checkCombine ){
std::vector< Node > clique;
if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
//explain clique
- addCliqueLemma( clique, &d_thss->getOutputChannel() );
+ addCliqueLemma(clique);
}
}
}
@@ -984,7 +989,8 @@ void SortModel::moveNode( Node n, int ri ){
d_regions_map[n] = ri;
}
-int SortModel::addSplit( Region* r, OutputChannel* out ){
+int SortModel::addSplit(Region* r)
+{
Node s;
if( r->hasSplits() ){
//take the first split you find
@@ -1032,10 +1038,12 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
//Notice() << "*** Split on " << s << std::endl;
//split on the equality s
Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() );
- if( doSendLemma( lem ) ){
+ // send lemma, with caching
+ if (d_im.lemma(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_im.requirePhase(ss, true);
++( d_thss->d_statistics.d_split_lemmas );
}
return 1;
@@ -1044,8 +1052,8 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
}
}
-
-void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ){
+void SortModel::addCliqueLemma(std::vector<Node>& clique)
+{
Assert(d_hasCard);
Assert(d_cardinality > 0);
while( clique.size()>size_t(d_cardinality+1) ){
@@ -1062,14 +1070,16 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out
}
eqs.push_back(d_cardinality_literal[d_cardinality].notNode());
Node lem = NodeManager::currentNM()->mkNode(OR, eqs);
- if (doSendLemma(lem))
+ // send lemma, with caching
+ if (d_im.lemma(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 ){
+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();
@@ -1103,7 +1113,7 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
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 );
+ d_im.lemma(lem, LemmaProperty::NONE, false);
}
}
}
@@ -1117,7 +1127,7 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
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_im.lemma(lem, LemmaProperty::NONE, false);
++( d_thss->d_statistics.d_totality_lemmas );
}
}
@@ -1138,18 +1148,7 @@ void SortModel::simpleCheckCardinality() {
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;
+ d_im.conflict(lem);
}
}
@@ -1230,7 +1229,7 @@ bool SortModel::debugModel( TheoryModel* m ){
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 );
+ d_im.lemma(lem, LemmaProperty::NONE, false);
return false;
}
}
@@ -1294,40 +1293,39 @@ Node SortModel::getCardinalityLiteral(unsigned c)
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);
+ 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, &d_thss->getOutputChannel());
+ addTotalityAxiom((*it).first, c);
}
return lit;
}
-CardinalityExtension::CardinalityExtension(context::Context* c,
- context::UserContext* u,
- OutputChannel& out,
+CardinalityExtension::CardinalityExtension(TheoryState& state,
+ TheoryInferenceManager& im,
TheoryUF* th)
- : d_out(&out),
+ : d_state(state),
+ d_im(im),
d_th(th),
- d_conflict(c, false),
d_rep_model(),
- d_min_pos_com_card(c, -1),
+ d_min_pos_com_card(state.getSatContext(), -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)
+ d_initializedCombinedCardinality(state.getUserContext(), false),
+ d_card_assertions_eqv_lemma(state.getUserContext()),
+ d_min_pos_tn_master_card(state.getSatContext(), -1),
+ d_rel_eqc(state.getSatContext())
{
if (options::ufssMode() == options::UfssMode::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()));
+ d_cc_dec_strat.reset(new CombinedCardinalityDecisionStrategy(
+ state.getSatContext(), th->getValuation()));
}
}
@@ -1353,18 +1351,6 @@ SortInference* CardinalityExtension::getSortInference()
return nullptr;
}
-/** 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)
{
@@ -1514,7 +1500,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
}
}
Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
- d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
+ d_rep_model[tn]->assertCardinality(nCard, polarity);
//check if combined cardinality is violated
checkCombinedCardinality();
}else{
@@ -1523,7 +1509,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
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_im.lemma(eqv_lit, LemmaProperty::NONE, false);
d_card_assertions_eqv_lemma[lit] = true;
}
}
@@ -1557,7 +1543,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
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();
+ d_im.setIncomplete();
}
}
Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
@@ -1586,7 +1572,8 @@ bool CardinalityExtension::areDisequal(Node a, Node b)
/** check */
void CardinalityExtension::check(Theory::Effort level)
{
- if( !d_conflict ){
+ if (!d_state.isInConflict())
+ {
if (options::ufssMode() == options::UfssMode::FULL)
{
Trace("uf-ss-solver")
@@ -1609,9 +1596,9 @@ void CardinalityExtension::check(Theory::Effort level)
}
}
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;
+ it->second->check(level);
+ if (d_state.isInConflict())
+ {
break;
}
}
@@ -1636,8 +1623,8 @@ void CardinalityExtension::check(Theory::Effort level)
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 );
+ d_im.lemma(lem, LemmaProperty::NONE, false);
+ d_im.requirePhase(eq, true);
type_proc[tn] = true;
break;
}
@@ -1665,7 +1652,7 @@ 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 );
+ it->second->initialize();
}
}
@@ -1703,31 +1690,16 @@ void CardinalityExtension::preRegisterTerm(TNode n)
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";
- }
- */
+ rm = new SortModel(n, d_state, d_im, this);
}
if( rm ){
- rm->initialize( d_out );
+ rm->initialize();
d_rep_model[tn] = rm;
//d_rep_model_init[tn] = true;
}
}else{
//ensure sort model is initialized
- it->second->initialize( d_out );
+ it->second->initialize();
}
}
}
@@ -1838,8 +1810,7 @@ void CardinalityExtension::checkCombinedCardinality()
<< " : " << cf << std::endl;
Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict"
<< " : " << cf << std::endl;
- getOutputChannel().conflict( cf );
- d_conflict.set( true );
+ d_im.conflict(cf);
return;
}
}
@@ -1876,8 +1847,7 @@ void CardinalityExtension::checkCombinedCardinality()
<< std::endl;
Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf
<< std::endl;
- getOutputChannel().conflict( cf );
- d_conflict.set( true );
+ d_im.conflict(cf);
}
}
}
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index e1ca46bfb..4c2707c17 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -215,6 +215,10 @@ class CardinalityExtension
private:
/** the type this model is for */
TypeNode d_type;
+ /** Reference to the state object */
+ TheoryState& d_state;
+ /** Reference to the inference manager */
+ TheoryInferenceManager& d_im;
/** Pointer to the cardinality extension that owns this. */
CardinalityExtension* d_thss;
/** regions used to d_region_index */
@@ -251,20 +255,18 @@ class CardinalityExtension
/** move node n to region ri */
void moveNode( Node n, int ri );
/** allocate cardinality */
- void allocateCardinality( OutputChannel* out );
+ void allocateCardinality();
/**
* Add splits. Returns
* 0 = no split,
* -1 = entailed disequality added, or
* 1 = split added.
*/
- int addSplit( Region* r, OutputChannel* out );
+ int addSplit(Region* r);
/** add clique lemma */
- void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
+ void addCliqueLemma(std::vector<Node>& clique);
/** add totality axiom */
- void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
- /** Are we in conflict */
- context::CDO<bool> d_conflict;
+ void addTotalityAxiom(Node n, int cardinality);
/** cardinality */
context::CDO< int > d_cardinality;
/** cardinality lemma term */
@@ -283,8 +285,6 @@ class CardinalityExtension
std::vector< Node > d_fresh_aloc_reps;
/** whether we are initialized */
context::CDO< bool > d_initialized;
- /** cache for lemmas */
- NodeBoolMap d_lemma_cache;
/** apply totality */
bool applyTotality( int cardinality );
@@ -293,16 +293,14 @@ class CardinalityExtension
/** simple check cardinality */
void simpleCheckCardinality();
- bool doSendLemma( Node lem );
-
public:
SortModel(Node n,
- context::Context* c,
- context::UserContext* u,
+ TheoryState& state,
+ TheoryInferenceManager& im,
CardinalityExtension* thss);
virtual ~SortModel();
/** initialize */
- void initialize( OutputChannel* out );
+ void initialize();
/** new node */
void newEqClass( Node n );
/** merge */
@@ -312,15 +310,11 @@ class CardinalityExtension
/** are disequal */
bool areDisequal( Node a, Node b );
/** check */
- void check( Theory::Effort level, OutputChannel* out );
+ void check(Theory::Effort level);
/** presolve */
void presolve();
- /** propagate */
- void propagate( Theory::Effort level, OutputChannel* out );
/** assert cardinality */
- void assertCardinality( OutputChannel* out, int c, bool val );
- /** is in conflict */
- bool isConflict() { return d_conflict; }
+ void assertCardinality(int c, bool val);
/** get cardinality */
int getCardinality() { return d_cardinality; }
/** has cardinality */
@@ -365,19 +359,14 @@ class CardinalityExtension
}; /** class SortModel */
public:
- CardinalityExtension(context::Context* c,
- context::UserContext* u,
- OutputChannel& out,
+ CardinalityExtension(TheoryState& state,
+ TheoryInferenceManager& im,
TheoryUF* th);
~CardinalityExtension();
/** get theory */
TheoryUF* getTheory() { return d_th; }
/** get sort inference module */
SortInference* getSortInference();
- /** get default sat context */
- context::Context* getSatContext();
- /** get default output channel */
- OutputChannel& getOutputChannel();
/** new node */
void newEqClass( Node n );
/** merge */
@@ -400,8 +389,6 @@ class CardinalityExtension
void debugPrint( const char* c );
/** debug a model */
bool debugModel( TheoryModel* m );
- /** get is in conflict */
- bool isConflict() { return d_conflict; }
/** get cardinality for node */
int getCardinality( Node n );
/** get cardinality for type */
@@ -435,12 +422,12 @@ class CardinalityExtension
/** ensure eqc for all subterms of n */
void ensureEqcRec(Node n);
- /** The output channel used by this class. */
- OutputChannel* d_out;
+ /** Reference to the state object */
+ TheoryState& d_state;
+ /** Reference to the inference manager */
+ TheoryInferenceManager& d_im;
/** theory uf pointer */
TheoryUF* d_th;
- /** Are we in conflict */
- context::CDO<bool> d_conflict;
/** rep model structure, one for each type */
std::map<TypeNode, SortModel*> d_rep_model;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index a58834891..0a48d4c71 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -90,8 +90,7 @@ void TheoryUF::finishInit() {
if (options::finiteModelFind()
&& options::ufssMode() != options::UfssMode::NONE)
{
- d_thss.reset(new CardinalityExtension(
- getSatContext(), getUserContext(), *d_out, this));
+ d_thss.reset(new CardinalityExtension(d_state, d_im, this));
}
// The kinds we are treating as function application in congruence
d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
@@ -136,10 +135,6 @@ void TheoryUF::postCheck(Effort level)
if (d_thss != nullptr)
{
d_thss->check(level);
- if (d_thss->isConflict())
- {
- d_state.notifyInConflict();
- }
}
// check with the higher-order extension
if (!d_state.isInConflict() && fullEffort(level))
@@ -159,9 +154,8 @@ bool TheoryUF::preNotifyFact(
bool isDecision =
d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
d_thss->assertNode(fact, isDecision);
- if (d_thss->isConflict())
+ if (d_state.isInConflict())
{
- d_state.notifyInConflict();
return true;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback