From e600773f0e189d22c5f28ee1d443ba38e5fa72e8 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 15 Dec 2015 12:37:23 +0100 Subject: [PATCH] Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference. --- src/options/uf_options | 2 + src/smt/smt_engine.cpp | 10 +- src/theory/sort_inference.cpp | 317 ++++++++++++---------- src/theory/sort_inference.h | 11 +- src/theory/uf/theory_uf_strong_solver.cpp | 154 ++++++++--- src/theory/uf/theory_uf_strong_solver.h | 6 + src/theory/uf/theory_uf_type_rules.h | 8 + 7 files changed, 321 insertions(+), 187 deletions(-) diff --git a/src/options/uf_options b/src/options/uf_options index baea1cb41..e7df9a2db 100644 --- a/src/options/uf_options +++ b/src/options/uf_options @@ -38,5 +38,7 @@ option ufssSymBreak --uf-ss-sym-break bool :default false finite model finding symmetry breaking techniques option ufssFairness --uf-ss-fair bool :default true use fair strategy for finite model finding multiple sorts +option ufssFairnessMonotone --uf-ss-fair-monotone bool :read-write :default false + group monotone sorts when enforcing fairness for finite model finding endmodule diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 21d190d0e..f3724b432 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1337,9 +1337,13 @@ void SmtEngine::setDefaults() { options::decisionMode.set(decMode); options::decisionStopOnly.set(stoponly); } + if( options::incrementalSolving() ){ + //disable modes not supported by incremental + options::sortInference.set( false ); + options::ufssFairnessMonotone.set( false ); + } //local theory extensions if( options::localTheoryExt() ){ - //no E-matching? if( !options::instMaxLevel.wasSetByUser() ){ options::instMaxLevel.set( 0 ); } @@ -3392,10 +3396,10 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-quant-preprocess" << endl; } - if( options::sortInference() ){ + if( options::sortInference() || options::ufssFairnessMonotone() ){ //sort inference technique SortInference * si = d_smt.d_theoryEngine->getSortInference(); - si->simplify( d_assertions.ref() ); + si->simplify( d_assertions.ref(), options::sortInference(), options::ufssFairnessMonotone() ); for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){ d_smt.setPrintFuncInModel( it->first.toExpr(), false ); d_smt.setPrintFuncInModel( it->second.toExpr(), true ); diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index a26c0e9d7..c4c24612d 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -26,7 +26,9 @@ #include "options/uf_options.h" #include "proof/proof_manager.h" #include "theory/rewriter.h" +#include "theory/quantifiers/quant_util.h" +using namespace CVC4; using namespace std; namespace CVC4 { @@ -40,7 +42,6 @@ void SortInference::UnionFind::print(const char * c){ } Trace(c) << std::endl; } - void SortInference::UnionFind::set( UnionFind& c ) { clear(); for( std::map< int, int >::iterator it = c.d_eqc.begin(); it != c.d_eqc.end(); ++it ){ @@ -48,7 +49,6 @@ void SortInference::UnionFind::set( UnionFind& c ) { } d_deq.insert( d_deq.end(), c.d_deq.begin(), c.d_deq.end() ); } - int SortInference::UnionFind::getRepresentative( int t ){ std::map< int, int >::iterator it = d_eqc.find( t ); if( it==d_eqc.end() || it->second==t ){ @@ -59,7 +59,6 @@ int SortInference::UnionFind::getRepresentative( int t ){ return rt; } } - void SortInference::UnionFind::setEqual( int t1, int t2 ){ if( t1!=t2 ){ int rt1 = getRepresentative( t1 ); @@ -71,7 +70,6 @@ void SortInference::UnionFind::setEqual( int t1, int t2 ){ } } } - bool SortInference::UnionFind::isValid() { for( unsigned i=0; i& assertions ){ - Trace("sort-inference") << "Calculating sort inference..." << std::endl; - //process all assertions - for( unsigned i=0; i var_bound; - process( assertions[i], var_bound ); - } - for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ - Trace("sort-inference") << it->first << " : "; - TypeNode retTn = it->first.getType(); - if( !d_op_arg_types[ it->first ].empty() ){ - Trace("sort-inference") << "( "; - for( size_t i=0; ifirst ].size(); i++ ){ - recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] ); - printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); - Trace("sort-inference") << " "; - } - Trace("sort-inference") << ") -> "; - retTn = retTn[(int)retTn.getNumChildren()-1]; - } - recordSubsort( retTn, it->second ); - printSort( "sort-inference", it->second ); - Trace("sort-inference") << std::endl; - } - for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ - Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl; - for( unsigned i=0; ifirst[0].getNumChildren(); i++ ){ - recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] ); - printSort( "sort-inference", it->second[it->first[0][i]] ); - Trace("sort-inference") << std::endl; - } - Trace("sort-inference") << std::endl; - } - - if( !options::ufssSymBreak() ){ - bool rewritten = false; - //determine monotonicity of sorts +void SortInference::simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ){ + if( doSortInference ){ + Trace("sort-inference") << "Calculating sort inference..." << std::endl; + //process all assertions for( unsigned i=0; i var_bound; - processMonotonic( assertions[i], true, true, var_bound ); + process( assertions[i], var_bound ); } - - Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl; - for( unsigned i=0; i::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + Trace("sort-inference") << it->first << " : "; + TypeNode retTn = it->first.getType(); + if( !d_op_arg_types[ it->first ].empty() ){ + Trace("sort-inference") << "( "; + for( size_t i=0; ifirst ].size(); i++ ){ + recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] ); + printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); + Trace("sort-inference") << " "; + } + Trace("sort-inference") << ") -> "; + retTn = retTn[(int)retTn.getNumChildren()-1]; } + recordSubsort( retTn, it->second ); + printSort( "sort-inference", it->second ); + Trace("sort-inference") << std::endl; } - - //simplify all assertions by introducing new symbols wherever necessary - for( unsigned i=0; i var_bound; - Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl; - Node curr = simplify( assertions[i], var_bound ); - Trace("sort-inference-debug") << "Done." << std::endl; - if( curr!=assertions[i] ){ - curr = theory::Rewriter::rewrite( curr ); - rewritten = true; - Trace("sort-inference-rewrite") << assertions << std::endl; - Trace("sort-inference-rewrite") << " --> " << curr << std::endl; - PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); - assertions[i] = curr; + for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ + Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl; + for( unsigned i=0; ifirst[0].getNumChildren(); i++ ){ + recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] ); + printSort( "sort-inference", it->second[it->first[0][i]] ); + Trace("sort-inference") << std::endl; } + Trace("sort-inference") << std::endl; } - //now, ensure constants are distinct - for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){ - std::vector< Node > consts; - for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - consts.push_back( it2->second ); + + if( !options::ufssSymBreak() ){ + bool rewritten = false; + //determine monotonicity of sorts + for( unsigned i=0; i var_bound; + processMonotonic( assertions[i], true, true, var_bound ); + } + //doMonotonicyInference = false; + + Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl; + for( unsigned i=0; i >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){ - int nmonSort = -1; - for( unsigned i=0; isecond.size(); i++ ){ - if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ - nmonSort = it->second[i]; - break; + //simplify all assertions by introducing new symbols wherever necessary + for( unsigned i=0; i var_bound; + Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl; + Node curr = simplify( assertions[i], var_bound ); + Trace("sort-inference-debug") << "Done." << std::endl; + if( curr!=assertions[i] ){ + curr = theory::Rewriter::rewrite( curr ); + rewritten = true; + Trace("sort-inference-rewrite") << assertions << std::endl; + Trace("sort-inference-rewrite") << " --> " << curr << std::endl; + PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); + assertions[i] = curr; } } - if( nmonSort!=-1 ){ - std::vector< Node > injections; - TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first ); + //now, ensure constants are distinct + for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){ + std::vector< Node > consts; + for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + consts.push_back( it2->second ); + } + //TODO: add lemma enforcing introduced constants to be distinct + } + + //enforce constraints based on monotonicity + for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){ + int nmonSort = -1; for( unsigned i=0; isecond.size(); i++ ){ - if( it->second[i]!=nmonSort ){ - TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first ); - //make injection to nmonSort - Node a1 = mkInjection( new_tn, base_tn ); - injections.push_back( a1 ); - if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ - //also must make injection from nmonSort to this - Node a2 = mkInjection( base_tn, new_tn ); - injections.push_back( a2 ); - } + if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ + nmonSort = it->second[i]; + break; } } - Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl; - for( unsigned j=0; j injections; + TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first ); + for( unsigned i=0; isecond.size(); i++ ){ + if( it->second[i]!=nmonSort ){ + TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first ); + //make injection to nmonSort + Node a1 = mkInjection( new_tn, base_tn ); + injections.push_back( a1 ); + if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ + //also must make injection from nmonSort to this + Node a2 = mkInjection( base_tn, new_tn ); + injections.push_back( a2 ); + } + } + } + Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl; + for( unsigned j=0; j > constants; - for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ - int rt = d_type_union_find.getRepresentative( it->second ); - if( d_op_arg_types[ it->first ].empty() ){ - TypeNode tn = it->first.getType(); - if( constants[ tn ].find( rt )==constants[ tn ].end() ){ - constants[ tn ][ rt ] = it->first; + //no sub-sort information is stored + reset(); + Trace("sort-inference-debug") << "Finished sort inference, rewritten = " << rewritten << std::endl; + } + /* + else if( !options::ufssSymBreak() ){ + //just add the unit lemmas between constants + std::map< TypeNode, std::map< int, Node > > constants; + for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + int rt = d_type_union_find.getRepresentative( it->second ); + if( d_op_arg_types[ it->first ].empty() ){ + TypeNode tn = it->first.getType(); + if( constants[ tn ].find( rt )==constants[ tn ].end() ){ + constants[ tn ][ rt ] = it->first; + } } } - } - //add unit lemmas for each constant - for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){ - Node first_const; - for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - if( first_const.isNull() ){ - first_const = it2->second; - }else{ - Node eq = first_const.eqNode( it2->second ); - //eq = Rewriter::rewrite( eq ); - Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl; - assertions.push_back( eq ); + //add unit lemmas for each constant + for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){ + Node first_const; + for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( first_const.isNull() ){ + first_const = it2->second; + }else{ + Node eq = first_const.eqNode( it2->second ); + //eq = Rewriter::rewrite( eq ); + Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl; + assertions.push_back( eq ); + } } } } + */ + initialSortCount = sortCount; + } + if( doMonotonicyInference ){ + for( unsigned i=0; i var_bound; + processMonotonic( assertions[i], true, true, var_bound, true ); + } } - */ - initialSortCount = sortCount; - return false; } void SortInference::setEqual( int t1, int t2 ){ @@ -455,37 +462,42 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ return retType; } -void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) { +void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, bool typeMode ) { Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl; if( n.getKind()==kind::FORALL ){ - for( unsigned i=0; i& var_bound ); //for monotonicity inference private: - void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ); + void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound, bool typeMode = false ); //for rewriting private: @@ -93,7 +93,7 @@ public: SortInference() : sortCount( 1 ){} ~SortInference(){} - bool simplify( std::vector< Node >& assertions ); + void simplify( std::vector< Node >& assertions, bool doSortInference, bool doMonotonicyInference ); //get sort id for term n int getSortId( Node n ); //get sort id for variable of quantified formula f @@ -109,6 +109,13 @@ public: public: //list of all functions and the uninterpreted symbols they were replaced with std::map< Node, Node > d_model_replace_f; + +private: + // store monotonicity for original sorts as well + std::map< TypeNode, bool > d_non_monotonic_sorts_orig; +public: + //is monotonic + bool isMonotonic( TypeNode tn ); }; } diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index d617207cf..d261d0007 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1501,8 +1501,8 @@ Node StrongSolverTheoryUF::SortModel::getCardinalityLiteral( int c ) { } StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) : -d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ), -d_card_assertions_eqv_lemma( u ), d_rel_eqc( c ) +d_out( &out ), d_th( th ), d_conflict( c, false ), d_rep_model(), d_aloc_com_card( u, 0 ), d_com_card_assertions( c ), d_min_pos_com_card( c, -1 ), +d_card_assertions_eqv_lemma( u ), d_min_pos_tn_master_card( c, -1 ), d_rel_eqc( c ) { if( options::ufssDiseqPropagation() ){ d_deq_prop = new DisequalityPropagator( th->getQuantifiersEngine(), this ); @@ -1618,9 +1618,45 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ TypeNode tn = lit[0].getType(); Assert( tn.isSort() ); Assert( d_rep_model[tn] ); - long nCard = lit[1].getConst().getNumerator().getLong(); + int nCard = lit[1].getConst().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 || nCardassertCardinality( d_out, nCard, polarity ); //check if combined cardinality is violated checkCombinedCardinality(); @@ -1636,14 +1672,28 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ d_com_card_assertions[lit] = polarity; if( polarity ){ - checkCombinedCardinality(); + //safe to assume int here + int nCard = lit[0].getConst().getNumerator().getSignedInt(); + if( d_min_pos_com_card.get()==-1 || nCard::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){ - if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() || d_com_card_assertions[it->second] ){ - needsCard = false; - break; + if( d_min_pos_com_card.get()==-1 ){ + //check if all current combined cardinality constraints are asserted negatively + for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){ + if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){ + Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl; + needsCard = false; + break; + }else{ + Assert( !d_com_card_assertions[it->second] ); + } } + }else{ + Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : positive assertion : " << d_min_pos_com_card.get() << std::endl; + needsCard = false; } if( needsCard ){ allocateCombinedCardinality(); @@ -1892,8 +1942,8 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){ /** initialize */ void StrongSolverTheoryUF::initializeCombinedCardinality() { if( options::ufssFairness() ){ - Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl; if( d_aloc_com_card.get()==0 ){ + Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl; allocateCombinedCardinality(); } } @@ -1902,36 +1952,76 @@ void StrongSolverTheoryUF::initializeCombinedCardinality() { /** check */ void StrongSolverTheoryUF::checkCombinedCardinality() { 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 ){ - totalCombinedCard += it->second->getMaximumNegativeCardinality(); + 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; - for( int i=0; i 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 ){ - int c = it->second->getMaximumNegativeCardinality(); - if( c>0 ){ - conf.push_back( it->second->getCardinalityLiteral( c ).negate() ); - totalAdded += c; - } - if( totalAdded>i ){ - break; - } + 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; + } + } + if( d_min_pos_com_card.get()!=-1 && totalCombinedCard>d_min_pos_com_card.get() ){ + //conflict + int cc = d_min_pos_com_card.get(); + Assert( d_com_card_literal.find( cc )!=d_com_card_literal.end() ); + Node com_lit = d_com_card_literal[cc]; + Assert( d_com_card_assertions.find( com_lit )!=d_com_card_assertions.end() ); + Assert( d_com_card_assertions[com_lit] ); + 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 cc = NodeManager::currentNM()->mkNode( AND, conf ); - Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cc << std::endl; - Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cc << std::endl; - getOutputChannel().conflict( cc ); - d_conflict.set( true ); } } + 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 ); } } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index dd32154d9..45d7fc3cc 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -314,8 +314,14 @@ private: std::map< int, Node > d_com_card_literal; /** combined cardinality assertions (indexed by cardinality literals ) */ NodeBoolMap d_com_card_assertions; + /** minimum positive combined cardinality */ + context::CDO< int > d_min_pos_com_card; /** cardinality literals for which we have added */ NodeBoolMap d_card_assertions_eqv_lemma; + /** the master monotone type (if ufssFairnessMonotone enabled) */ + TypeNode d_tn_mono_master; + std::map< TypeNode, bool > d_tn_mono_slave; + context::CDO< int > d_min_pos_tn_master_card; /** initialize */ void initializeCombinedCardinality(); /** allocateCombinedCardinality */ diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 0040a38c3..6faab8517 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -71,6 +71,10 @@ public: if( n[1].getKind()!=kind::CONST_RATIONAL ){ throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be a constant"); } + CVC4::Rational r(INT_MAX); + if( n[1].getConst()>r ){ + throw TypeCheckingExceptionPrivate(n, "Exceeded INT_MAX in cardinality constraint"); + } if( n[1].getConst().getNumerator().sgn()!=1 ){ throw TypeCheckingExceptionPrivate(n, "cardinality constraint must be positive"); } @@ -91,6 +95,10 @@ public: if( n[0].getKind()!=kind::CONST_RATIONAL ){ throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be a constant"); } + CVC4::Rational r(INT_MAX); + if( n[0].getConst()>r ){ + throw TypeCheckingExceptionPrivate(n, "Exceeded INT_MAX in combined cardinality constraint"); + } if( n[0].getConst().getNumerator().sgn()==-1 ){ throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be non-negative"); } -- 2.30.2