summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp106
-rw-r--r--src/theory/sets/theory_sets_private.cpp22
-rw-r--r--src/theory/sets/theory_sets_private.h1
-rw-r--r--src/theory/sets/theory_sets_rels.cpp7
-rw-r--r--src/theory/sets/theory_sets_rels.h1
-rw-r--r--test/regress/regress0/fmf/Makefile.am3
-rw-r--r--test/regress/regress0/fmf/ko-bound-set.cvc10
7 files changed, 102 insertions, 48 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e9ac9b484..1e8449dbf 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -246,8 +246,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
if( success && !isBound( q, v ) ){
Trace("bound-int-debug") << "Success with variable " << v << std::endl;
bound_lit_type_map[v] = BOUND_FIXED_SET;
- bound_lit_map[0][v] = n;
- bound_lit_pol_map[0][v] = pol;
+ bound_lit_map[3][v] = n;
+ bound_lit_pol_map[3][v] = pol;
bound_fixed_set[v].clear();
bound_fixed_set[v].insert( bound_fixed_set[v].end(), v_cases.begin(), v_cases.end() );
}
@@ -260,8 +260,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
if( processEqDisjunct( q, n, v, v_cases ) ){
if( !isBound( q, v ) ){
bound_lit_type_map[v] = BOUND_FIXED_SET;
- bound_lit_map[0][v] = n;
- bound_lit_pol_map[0][v] = pol;
+ bound_lit_map[3][v] = n;
+ bound_lit_pol_map[3][v] = pol;
Assert( v_cases.size()==1 );
bound_fixed_set[v].clear();
bound_fixed_set[v].push_back( v_cases[0] );
@@ -278,32 +278,35 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" );
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){
- Node veq;
- if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
- Node n1 = veq[0];
- Node n2 = veq[1];
- if(pol){
- //flip
- n1 = veq[1];
- n2 = veq[0];
- if( n1.getKind()==BOUND_VARIABLE ){
- n2 = QuantArith::offset( n2, 1 );
+ //if not bound in another way
+ if( bound_lit_type_map.find( it->first )==bound_lit_type_map.end() || bound_lit_type_map[it->first] == BOUND_INT_RANGE ){
+ Node veq;
+ if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){
+ Node n1 = veq[0];
+ Node n2 = veq[1];
+ if(pol){
+ //flip
+ n1 = veq[1];
+ n2 = veq[0];
+ if( n1.getKind()==BOUND_VARIABLE ){
+ n2 = QuantArith::offset( n2, 1 );
+ }else{
+ n1 = QuantArith::offset( n1, -1 );
+ }
+ veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
+ }
+ Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
+ Node t = n1==it->first ? n2 : n1;
+ if( !hasNonBoundVar( q, t ) ) {
+ Trace("bound-int-debug") << "The bound is relevant." << std::endl;
+ int loru = n1==it->first ? 0 : 1;
+ bound_lit_type_map[it->first] = BOUND_INT_RANGE;
+ bound_int_range_term[loru][it->first] = t;
+ bound_lit_map[loru][it->first] = n;
+ bound_lit_pol_map[loru][it->first] = pol;
}else{
- n1 = QuantArith::offset( n1, -1 );
+ Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
}
- veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );
- }
- Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;
- Node t = n1==it->first ? n2 : n1;
- if( !hasNonBoundVar( q, t ) ) {
- Trace("bound-int-debug") << "The bound is relevant." << std::endl;
- int loru = n1==it->first ? 0 : 1;
- bound_lit_type_map[it->first] = BOUND_INT_RANGE;
- bound_int_range_term[loru][it->first] = t;
- bound_lit_map[loru][it->first] = n;
- bound_lit_pol_map[loru][it->first] = pol;
- }else{
- Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl;
}
}
}
@@ -314,8 +317,8 @@ void BoundedIntegers::process( Node q, Node n, bool pol,
if( !pol && n[0].getKind()==BOUND_VARIABLE && !isBound( q, n[0] ) && !hasNonBoundVar( q, n[1] ) ){
Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl;
bound_lit_type_map[n[0]] = BOUND_SET_MEMBER;
- bound_lit_map[0][n[0]] = n;
- bound_lit_pol_map[0][n[0]] = pol;
+ bound_lit_map[2][n[0]] = n;
+ bound_lit_pol_map[2][n[0]] = pol;
}
}else{
Assert( n.getKind()!=LEQ && n.getKind()!=LT && n.getKind()!=GT );
@@ -391,10 +394,10 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
}else if( it->second==BOUND_SET_MEMBER ){
setBoundedVar( f, v, BOUND_SET_MEMBER );
setBoundVar = true;
- d_setm_range[f][v] = bound_lit_map[0][v][1];
- d_setm_range_lit[f][v] = bound_lit_map[0][v];
+ d_setm_range[f][v] = bound_lit_map[2][v][1];
+ d_setm_range_lit[f][v] = bound_lit_map[2][v];
d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] );
- Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl;
+ Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[2][v] << std::endl;
}else if( it->second==BOUND_FIXED_SET ){
setBoundedVar( f, v, BOUND_FIXED_SET );
setBoundVar = true;
@@ -406,7 +409,7 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
d_fixed_set_gr_range[f][v].push_back( t );
}
}
- Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[0][v] << std::endl;
+ Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[3][v] << std::endl;
}
if( setBoundVar ){
success = true;
@@ -438,13 +441,34 @@ void BoundedIntegers::preRegisterQuantifier( Node f ) {
}
}while( success );
- Trace("bound-int") << "Bounds are : " << std::endl;
- for( unsigned i=0; i<d_set[f].size(); i++) {
- Node v = d_set[f][i];
- if( d_bound_type[f][v]==BOUND_INT_RANGE ){
- Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
- }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
- Trace("bound-int") << " " << v << " in " << d_setm_range[f][v] << std::endl;
+ if( Trace.isOn("bound-int") ){
+ Trace("bound-int") << "Bounds are : " << std::endl;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++) {
+ Node v = f[0][i];
+ if( std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end() ){
+ Assert( d_bound_type[f].find( v )!=d_bound_type[f].end() );
+ if( d_bound_type[f][v]==BOUND_INT_RANGE ){
+ Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;
+ }else if( d_bound_type[f][v]==BOUND_SET_MEMBER ){
+ Trace("bound-int") << " " << v << " in " << d_setm_range[f][v] << std::endl;
+ }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){
+ Trace("bound-int") << " " << v << " in { ";
+ for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){
+ Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " ";
+ }
+ for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){
+ Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " ";
+ }
+ Trace("bound-int") << "}" << std::endl;
+ }else if( d_bound_type[f][v]==BOUND_FINITE ){
+ Trace("bound-int") << " " << v << " has small finite type." << std::endl;
+ }else{
+ Trace("bound-int") << " " << v << " has unknown bound." << std::endl;
+ Assert( false );
+ }
+ }else{
+ Trace("bound-int") << " " << "*** " << v << " is unbounded." << std::endl;
+ }
}
}
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 6880a995d..40da5d7d0 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -72,6 +72,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
d_equalityEngine.addFunctionKind(kind::CARD);
d_card_enabled = false;
+ d_rels_enabled = false;
}/* TheorySetsPrivate::TheorySetsPrivate() */
@@ -513,6 +514,7 @@ void TheorySetsPrivate::fullEffortCheck(){
d_bop_index.clear();
d_op_list.clear();
d_card_enabled = false;
+ d_rels_enabled = false;
d_eqc_to_card_term.clear();
std::vector< Node > lemmas;
@@ -559,7 +561,9 @@ void TheorySetsPrivate::fullEffortCheck(){
}else{
d_congruent[n] = d_singleton_index[r];
}
- }else if( n.getKind()!=kind::EMPTYSET ){
+ }else if( n.getKind()==kind::EMPTYSET ){
+ d_eqc_emptyset[tn] = eqc;
+ }else{
Node r1 = d_equalityEngine.getRepresentative( n[0] );
Node r2 = d_equalityEngine.getRepresentative( n[1] );
if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){
@@ -568,8 +572,6 @@ void TheorySetsPrivate::fullEffortCheck(){
}else{
d_congruent[n] = d_bop_index[n.getKind()][r1][r2];
}
- }else{
- d_eqc_emptyset[tn] = eqc;
}
d_nvar_sets[eqc].push_back( n );
Trace("sets-debug2") << "Non-var-set[" << eqc << "] : " << n << std::endl;
@@ -588,8 +590,13 @@ void TheorySetsPrivate::fullEffortCheck(){
d_eqc_to_card_term[ r ] = n;
registerCardinalityTerm( n[0], lemmas );
}
- }else if( isSet ){
- d_set_eqc_list[eqc].push_back( n );
+ }else{
+ if( d_rels->isRelationKind( n.getKind() ) ){
+ d_rels_enabled = true;
+ }
+ if( isSet ){
+ d_set_eqc_list[eqc].push_back( n );
+ }
}
++eqc_i;
}
@@ -1527,6 +1534,11 @@ void TheorySetsPrivate::check(Theory::Effort level) {
// invoke the relational solver
if( !d_conflict && !d_sentLemma ){
d_rels->check(level);
+ //incomplete if we have both cardinality constraints and relational operators?
+ // TODO: should internally check model, return unknown if fail
+ if( level == Theory::EFFORT_FULL && d_card_enabled && d_rels_enabled ){
+ d_external.d_out->setIncomplete();
+ }
}
Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
}/* TheorySetsPrivate::check() */
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 8a6eaac2f..0a3745654 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -130,6 +130,7 @@ private:
//cardinality
private:
bool d_card_enabled;
+ bool d_rels_enabled;
std::map< Node, Node > d_eqc_to_card_term;
NodeSet d_card_processed;
std::map< Node, std::vector< Node > > d_card_parent;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 97e67a423..bd4ee5de0 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -824,7 +824,9 @@ int TheorySetsRels::EqcInfo::counter = 0;
d_tcr_tcGraph.clear();
d_tc_lemmas_last.clear();
}
-
+ bool TheorySetsRels::isRelationKind( Kind k ) {
+ return k == kind::TRANSPOSE || k == kind::PRODUCT || k == kind::JOIN || k == kind::TCLOSURE;
+ }
void TheorySetsRels::doTCLemmas() {
Trace("rels-debug") << "[Theory::Rels] **************** Start doTCLemmas !" << std::endl;
std::map< Node, std::vector< Node > >::iterator tc_lemma_it = d_tc_lemmas_last.begin();
@@ -1387,6 +1389,7 @@ int TheorySetsRels::EqcInfo::counter = 0;
NodeSet::const_iterator mem_it = t2_ei->d_mem.begin();
while(mem_it != t2_ei->d_mem.end()) {
+ Assert( !t2_ei->d_tc.get().isNull() );
addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*mem_it)).second);
mem_it++;
}
@@ -1397,6 +1400,7 @@ int TheorySetsRels::EqcInfo::counter = 0;
while(t1_mem_it != t1_ei->d_mem.end()) {
NodeMap::const_iterator reason_it = t1_ei->d_mem_exp.find(*t1_mem_it);
Assert(reason_it != t1_ei->d_mem_exp.end());
+ Assert( !t1_ei->d_tc.get().isNull() );
addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t1_mem_it, t1_ei->d_tc.get()), (*reason_it).second);
t1_mem_it++;
}
@@ -1404,6 +1408,7 @@ int TheorySetsRels::EqcInfo::counter = 0;
NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin();
while(t2_mem_it != t2_ei->d_mem.end()) {
+ Assert( !t2_ei->d_tc.get().isNull() );
addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t2_mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*t2_mem_it)).second);
t2_mem_it++;
}
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index b5c839a66..65a1c4164 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -64,6 +64,7 @@ public:
void check(Theory::Effort);
void doPendingLemmas();
+ bool isRelationKind( Kind k );
private:
/** equivalence class info
* d_mem tuples that are members of this equivalence class
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 218dde7d4..03fe780b8 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -63,7 +63,8 @@ TESTS = \
fmf-strange-bounds-2.smt2 \
fmf-bound-2dim.smt2 \
memory_model-R_cpp-dd.cvc \
- bug764.smt2
+ bug764.smt2 \
+ ko-bound-set.cvc
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/fmf/ko-bound-set.cvc b/test/regress/regress0/fmf/ko-bound-set.cvc
new file mode 100644
index 000000000..eebcbc2f8
--- /dev/null
+++ b/test/regress/regress0/fmf/ko-bound-set.cvc
@@ -0,0 +1,10 @@
+% EXPECT: invalid
+OPTION "finite-model-find";
+OPTION "fmf-bound-int";
+OPTION "produce-models";
+
+X, Y : SET OF INT;
+
+ASSERT FORALL(x : INT): x IS_IN X => x > 0;
+QUERY ||X|| = 5 AND Y = X | {9} => ||Y|| <= 4;
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback