From 97aaf2ffbb542b5c097b49071fd24ae40898eeb0 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 11 Jan 2017 14:34:18 -0600 Subject: [PATCH] Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed. --- src/theory/quantifiers/bounded_integers.cpp | 106 ++++++++++++-------- src/theory/sets/theory_sets_private.cpp | 22 +++- src/theory/sets/theory_sets_private.h | 1 + src/theory/sets/theory_sets_rels.cpp | 7 +- src/theory/sets/theory_sets_rels.h | 1 + test/regress/regress0/fmf/Makefile.am | 3 +- test/regress/regress0/fmf/ko-bound-set.cvc | 10 ++ 7 files changed, 102 insertions(+), 48 deletions(-) create mode 100644 test/regress/regress0/fmf/ko-bound-set.cvc 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 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; + -- 2.30.2