#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 {
}
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 ){
}
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 ){
return rt;
}
}
-
void SortInference::UnionFind::setEqual( int t1, int t2 ){
if( t1!=t2 ){
int rt1 = getRepresentative( t1 );
}
}
}
-
bool SortInference::UnionFind::isValid() {
for( unsigned i=0; i<d_deq.size(); i++ ){
if( areEqual( d_deq[i].first, d_deq[i].second ) ){
d_const_map.clear();
}
-bool SortInference::simplify( std::vector< Node >& assertions ){
- Trace("sort-inference") << "Calculating sort inference..." << std::endl;
- //process all assertions
- for( unsigned i=0; i<assertions.size(); i++ ){
- Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
- std::map< Node, Node > 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; i<d_op_arg_types[ it->first ].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; i<it->first[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<assertions.size(); i++ ){
- Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+ Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl;
std::map< Node, Node > 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<d_sub_sorts.size(); i++ ){
- printSort( "sort-inference", d_sub_sorts[i] );
- if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
- Trace("sort-inference") << " is interpreted." << std::endl;
- }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
- Trace("sort-inference") << " is monotonic." << std::endl;
- }else{
- Trace("sort-inference") << " is not monotonic." << std::endl;
+ 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; i<d_op_arg_types[ it->first ].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<assertions.size(); i++ ){
- Node prev = assertions[i];
- std::map< Node, Node > 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; i<it->first[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<assertions.size(); i++ ){
+ Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl;
+ std::map< Node, Node > 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<d_sub_sorts.size(); i++ ){
+ printSort( "sort-inference", d_sub_sorts[i] );
+ if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){
+ Trace("sort-inference") << " is interpreted." << std::endl;
+ }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){
+ Trace("sort-inference") << " is monotonic." << std::endl;
+ }else{
+ Trace("sort-inference") << " is not monotonic." << std::endl;
+ }
}
- //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; i<it->second.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<assertions.size(); i++ ){
+ Node prev = assertions[i];
+ std::map< Node, Node > 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; i<it->second.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.size(); j++ ){
- Trace("sort-inference-rewrite") << " " << injections[j] << std::endl;
- }
- assertions.insert( assertions.end(), injections.begin(), injections.end() );
- if( !injections.empty() ){
- rewritten = true;
+ if( nmonSort!=-1 ){
+ std::vector< Node > injections;
+ TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first );
+ for( unsigned i=0; i<it->second.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<injections.size(); j++ ){
+ Trace("sort-inference-rewrite") << " " << injections[j] << std::endl;
+ }
+ assertions.insert( assertions.end(), injections.begin(), injections.end() );
+ if( !injections.empty() ){
+ rewritten = true;
+ }
}
}
- }
- //no sub-sort information is stored
- reset();
- return rewritten;
- }
- /*
- 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;
+ //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<assertions.size(); i++ ){
+ Trace("sort-inference-debug") << "Process type monotonicity for " << assertions[i] << std::endl;
+ std::map< Node, Node > var_bound;
+ processMonotonic( assertions[i], true, true, var_bound, true );
+ }
}
- */
- initialSortCount = sortCount;
- return false;
}
void SortInference::setEqual( int t1, int t2 ){
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<n[0].getNumChildren(); i++ ){
- var_bound[n[0][i]] = n;
+ //only consider variables universally if it is possible this quantified formula is asserted positively
+ if( !hasPol || pol ){
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound[n[0][i]] = n;
+ }
}
- processMonotonic( n[1], pol, hasPol, var_bound );
- for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
- var_bound.erase( n[0][i] );
+ processMonotonic( n[1], pol, hasPol, var_bound, typeMode );
+ if( !hasPol || pol ){
+ for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+ var_bound.erase( n[0][i] );
+ }
}
+ return;
}else if( n.getKind()==kind::EQUAL ){
if( !hasPol || pol ){
for( unsigned i=0; i<2; i++ ){
if( var_bound.find( n[i] )!=var_bound.end() ){
- int sid = getSortId( var_bound[n[i]], n[i] );
- d_non_monotonic_sorts[sid] = true;
+ if( !typeMode ){
+ int sid = getSortId( var_bound[n[i]], n[i] );
+ d_non_monotonic_sorts[sid] = true;
+ }else{
+ d_non_monotonic_sorts_orig[n[i].getType()] = true;
+ }
break;
}
}
}
}
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool npol = pol;
- bool nhasPol = hasPol;
- if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){
- npol = !npol;
- }
- if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){
- nhasPol = false;
- }
- processMonotonic( n[i], npol, nhasPol, var_bound );
+ bool npol;
+ bool nhasPol;
+ theory::QuantPhaseReq::getPolarity( n, i, hasPol, pol, nhasPol, npol );
+ processMonotonic( n[i], npol, nhasPol, var_bound, typeMode );
}
}
}
}
+bool SortInference::isMonotonic( TypeNode tn ) {
+ Assert( tn.isSort() );
+ return d_non_monotonic_sorts_orig.find( tn )==d_non_monotonic_sorts_orig.end();
+}
+
}/* CVC4 namespace */
}
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 );
TypeNode tn = lit[0].getType();
Assert( tn.isSort() );
Assert( d_rep_model[tn] );
- long nCard = lit[1].getConst<Rational>().getNumerator().getLong();
+ 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 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<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{
bool needsCard = true;
- 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() || 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();
/** 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();
}
}
/** 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<totalCombinedCard; i++ ){
- if( d_com_card_literal.find( i )!=d_com_card_literal.end() ){
- Node com_lit = d_com_card_literal[i];
- if( d_com_card_assertions.find( com_lit )!=d_com_card_assertions.end() && d_com_card_assertions[com_lit] ){
- //conflict
- 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 ){
- 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 );
}
}
}
projects / cvc5.git / commitdiff