From fafb7f90f35941a72957dcc9ca5e45afd066cf04 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 12 Dec 2014 12:03:26 +0100 Subject: Add cvc parsing support for cardinality constraints. Bug fix for enumerating elements to meet cardinality lower bounds. --- src/theory/uf/theory_uf_strong_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/theory/uf') diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 28ea995d9..05fea6b5e 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1417,11 +1417,11 @@ bool StrongSolverTheoryUF::SortModel::debugModel( TheoryModel* m ){ } } int nReps = m->d_rep_set.d_type_reps.find( d_type )==m->d_rep_set.d_type_reps.end() ? 0 : (int)m->d_rep_set.d_type_reps[d_type].size(); - if( nReps!=d_maxNegCard ){ + 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 ){ + if( d_maxNegCard>=nReps ){ /* for( unsigned i=0; i0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){ -- cgit v1.2.3