From 3837f84ab251d1563726f3d13b95f541eaa331a4 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 7 Feb 2017 13:26:57 -0600 Subject: [PATCH] Generalize finite bound inference to unifiable variables in set membership literals. --- src/options/sets_options | 3 + src/theory/quantifiers/bounded_integers.cpp | 79 +++++++++++++++++-- src/theory/quantifiers/bounded_integers.h | 2 + src/theory/sets/theory_sets_private.cpp | 10 ++- test/regress/regress0/fmf/Makefile.am | 3 +- .../regress0/fmf/cons-sets-bounds.smt2 | 26 ++++++ 6 files changed, 113 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress0/fmf/cons-sets-bounds.smt2 diff --git a/src/options/sets_options b/src/options/sets_options index 52a8f78ba..1c7e12a7d 100644 --- a/src/options/sets_options +++ b/src/options/sets_options @@ -11,4 +11,7 @@ option setsProxyLemmas --sets-proxy-lemmas bool :default false option setsInferAsLemmas --sets-infer-as-lemmas bool :default true send inferences as lemmas +option setsRelEager --sets-rel-eager bool :default true + standard effort checks for relations + endmodule diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 1e8449dbf..09bb2dab3 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -212,6 +212,20 @@ bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< N return false; } +void BoundedIntegers::processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==BOUND_VARIABLE && !isBound( q, n ) ){ + bvs.push_back( n ); + //injective operators + }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){ + for( unsigned i=0; i& bound_lit_type_map, std::map< int, std::map< Node, Node > >& bound_lit_map, @@ -314,11 +328,17 @@ void BoundedIntegers::process( Node q, Node n, bool pol, } } }else if( n.getKind()==MEMBER ){ - 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[2][n[0]] = n; - bound_lit_pol_map[2][n[0]] = pol; + if( !pol && !hasNonBoundVar( q, n[1] ) ){ + std::vector< Node > bound_vars; + std::map< Node, bool > visited; + processMatchBoundVars( q, n[0], bound_vars, visited ); + for( unsigned i=0; i& va } } +Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){ + if( t==v ){ + return e; + }else if( t.getKind()==kind::APPLY_CONSTRUCTOR ){ + if( e.getKind()==kind::APPLY_CONSTRUCTOR ){ + if( t.getOperator() != e.getOperator() ) { + return Node::null(); + } + } + const Datatype& dt = Datatype::datatypeOf( t.getOperator().toExpr() ); + unsigned index = Datatype::indexOf( t.getOperator().toExpr() ); + for( unsigned i=0; imkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), e ); + u = matchBoundVar( v, t[i], se ); + } + if( !u.isNull() ){ + return u; + } + } + } + return Node::null(); +} + bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) { if( initial || !isGroundRange( q, v ) ){ elements.clear(); @@ -768,6 +819,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node }else{ Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl; if( srv.getKind()!=EMPTYSET ){ + //collect the elements while( srv.getKind()==UNION ){ Assert( srv[1].getKind()==kind::SINGLETON ); elements.push_back( srv[1][0] ); @@ -775,6 +827,21 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node } Assert( srv.getKind()==kind::SINGLETON ); elements.push_back( srv[0] ); + //check if we need to do matching, for literals like ( tuple( v ) in S ) + Node t = d_setm_range_lit[q][v][0]; + if( t!=v ){ + std::vector< Node > elements_tmp; + elements_tmp.insert( elements_tmp.end(), elements.begin(), elements.end() ); + elements.clear(); + for( unsigned i=0; i u + Node u = matchBoundVar( v, t, elements_tmp[i] ); + Trace("bound-int-rsi-debug") << " unification : " << elements_tmp[i] << " = " << t << " yields " << v << " -> " << u << std::endl; + if( !u.isNull() ){ + elements.push_back( u ); + } + } + } } return true; } diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 5c5a52855..f367b328c 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -74,6 +74,7 @@ private: std::map< int, std::map< Node, Node > >& bound_int_range_term, std::map< Node, std::vector< Node > >& bound_fixed_set ); bool processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ); + void processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ); std::vector< Node > d_bound_quants; private: class RangeModel { @@ -164,6 +165,7 @@ private: //for set range Node getSetRange( Node q, Node v, RepSetIterator * rsi ); Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi ); + Node matchBoundVar( Node v, Node t, Node e ); bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ); public: diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 40da5d7d0..d3c596664 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -90,7 +90,9 @@ void TheorySetsPrivate::eqNotifyNewClass(TNode t) { EqcInfo * e = getOrMakeEqcInfo( t, true ); e->d_singleton = t; } - d_rels->eqNotifyNewClass( t ); + if( options::setsRelEager() ){ + d_rels->eqNotifyNewClass( t ); + } } void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){ @@ -183,7 +185,9 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){ } d_members[t1] = n_members; } - d_rels->eqNotifyPostMerge( t1, t2 ); + if( options::setsRelEager() ){ + d_rels->eqNotifyPostMerge( t1, t2 ); + } } } @@ -1532,7 +1536,7 @@ void TheorySetsPrivate::check(Theory::Effort level) { fullEffortCheck(); } // invoke the relational solver - if( !d_conflict && !d_sentLemma ){ + if( !d_conflict && !d_sentLemma && ( level == Theory::EFFORT_FULL || options::setsRelEager() ) ){ d_rels->check(level); //incomplete if we have both cardinality constraints and relational operators? // TODO: should internally check model, return unknown if fail diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 03fe780b8..af8776ace 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -64,7 +64,8 @@ TESTS = \ fmf-bound-2dim.smt2 \ memory_model-R_cpp-dd.cvc \ bug764.smt2 \ - ko-bound-set.cvc + ko-bound-set.cvc \ + cons-sets-bounds.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/cons-sets-bounds.smt2 b/test/regress/regress0/fmf/cons-sets-bounds.smt2 new file mode 100644 index 000000000..db9788a61 --- /dev/null +++ b/test/regress/regress0/fmf/cons-sets-bounds.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: sat +(set-logic ALL) +(declare-datatypes () ((list (cons (head Int) (tail list)) (nil)))) + +(declare-fun P (Int) Bool) +(declare-fun S () (Set list)) + +; can use simple unification to infer bounds on x and y +(assert (forall ((x Int) (y list)) (=> (member (cons x y) S) (P x)))) + +(assert (member (cons 4 (cons 1 nil)) S)) +(assert (member (cons 2 nil) S)) + +; should construct instantiation involving selectors for l +(declare-fun l () list) +(assert (is-cons l)) +(assert (member l S)) + +; should not contribute to instantiations +(assert (member nil S)) + +(assert (not (P 1))) +(assert (not (P 0))) + +(check-sat) -- 2.30.2