From 22916321f5c26fdc632df24f3c1fef45beaeb918 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 24 Jul 2018 17:01:38 -0500 Subject: [PATCH] Improvements to sets + cardinality + quantifiers (#2200) --- src/options/options_handler.cpp | 37 ---- src/options/options_handler.h | 2 - src/options/quantifiers_modes.h | 11 -- src/options/quantifiers_options.toml | 11 -- .../quantifiers/fmf/bounded_integers.cpp | 165 ++++++++++-------- src/theory/quantifiers/fmf/bounded_integers.h | 8 + src/theory/sets/theory_sets_private.cpp | 32 ++-- src/theory/sets/theory_sets_private.h | 2 + test/regress/Makefile.tests | 2 + test/regress/regress1/fmf/radu-quant-set.smt2 | 18 ++ .../quantifiers/set-choice-koikonomou.cvc | 10 ++ 11 files changed, 153 insertions(+), 145 deletions(-) create mode 100644 test/regress/regress1/fmf/radu-quant-set.smt2 create mode 100644 test/regress/regress1/quantifiers/set-choice-koikonomou.cvc diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 6f9d31024..b48647116 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -582,23 +582,6 @@ depth \n\ \n\ "; -const std::string OptionsHandler::s_fmfBoundMinModeModeHelp = "\ -Modes for finite model finding bound minimization, supported by --fmf-bound-min-mode:\n\ -\n\ -none \n\ -+ Do not minimize inferred bounds.\n\ -\n\ -int (default) \n\ -+ Minimize integer ranges only.\n\ -\n\ -setc \n\ -+ Minimize cardinality of set membership ranges only.\n\ -\n\ -all \n\ -+ Minimize all inferred bounds.\n\ -\n\ -"; - theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode( std::string option, std::string optarg) { @@ -1038,26 +1021,6 @@ theory::quantifiers::QuantRepMode OptionsHandler::stringToQuantRepMode( } } -theory::quantifiers::FmfBoundMinMode OptionsHandler::stringToFmfBoundMinMode( - std::string option, std::string optarg) -{ - if(optarg == "none" ) { - return theory::quantifiers::FMF_BOUND_MIN_NONE; - } else if(optarg == "int" || optarg == "default") { - return theory::quantifiers::FMF_BOUND_MIN_INT_RANGE; - } else if(optarg == "setc" || optarg == "default") { - return theory::quantifiers::FMF_BOUND_MIN_SET_CARD; - } else if(optarg == "all") { - return theory::quantifiers::FMF_BOUND_MIN_ALL; - } else if(optarg == "help") { - puts(s_fmfBoundMinModeModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --fmf-bound-min-mode: `") + - optarg + "'. Try --fmf-bound-min-mode help."); - } -} - // theory/bv/options_handlers.h void OptionsHandler::abcEnabledBuild(std::string option, bool value) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index ab107ae78..6e2044957 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -120,8 +120,6 @@ public: std::string option, std::string optarg); theory::quantifiers::QuantRepMode stringToQuantRepMode(std::string option, std::string optarg); - theory::quantifiers::FmfBoundMinMode stringToFmfBoundMinMode( - std::string option, std::string optarg); theory::SygusFairMode stringToSygusFairMode(std::string option, std::string optarg); diff --git a/src/options/quantifiers_modes.h b/src/options/quantifiers_modes.h index afb54002c..1fd29340d 100644 --- a/src/options/quantifiers_modes.h +++ b/src/options/quantifiers_modes.h @@ -289,17 +289,6 @@ enum QuantRepMode { QUANT_REP_MODE_DEPTH, }; -enum FmfBoundMinMode { - /** do not minimize bounds */ - FMF_BOUND_MIN_NONE, - /** default, minimize integer ranges */ - FMF_BOUND_MIN_INT_RANGE, - /** minimize set cardinality ranges */ - FMF_BOUND_MIN_SET_CARD, - /** minimize all bounds */ - FMF_BOUND_MIN_ALL, -}; - }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 3c0438d95..eb74592f9 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -626,17 +626,6 @@ header = "options/quantifiers_options.h" default = "false" help = "enforce bounds for bounded quantification lazily via use of proxy variables" -[[option]] - name = "fmfBoundMinMode" - category = "regular" - long = "fmf-bound-min-mode=MODE" - type = "CVC4::theory::quantifiers::FmfBoundMinMode" - default = "CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE" - handler = "stringToFmfBoundMinMode" - includes = ["options/quantifiers_modes.h"] - read_only = true - help = "mode for which types of bounds to minimize via first decision heuristics" - [[option]] name = "fmfTypeCompletionThresh" category = "regular" diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index ae1e3df32..7094ad541 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -388,6 +388,7 @@ void BoundedIntegers::checkOwnership(Node f) { //this needs to be done at preregister since it affects e.g. QuantDSplit's preregister Trace("bound-int") << "check ownership quantifier " << f << std::endl; + NodeManager* nm = NodeManager::currentNM(); bool success; do{ @@ -413,21 +414,26 @@ void BoundedIntegers::checkOwnership(Node f) Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() ); d_bounds[b][f][v] = bound_int_range_term[b][v]; } - if( options::fmfBoundMinMode()==FMF_BOUND_MIN_ALL || options::fmfBoundMinMode()==FMF_BOUND_MIN_INT_RANGE ){ - Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] ); - d_range[f][v] = Rewriter::rewrite( r ); - } + Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]); + d_range[f][v] = Rewriter::rewrite(r); Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl; } }else if( it->second==BOUND_SET_MEMBER ){ - setBoundedVar( f, v, BOUND_SET_MEMBER ); - setBoundVar = true; - d_setm_range[f][v] = bound_lit_map[2][v][1]; - d_setm_range_lit[f][v] = bound_lit_map[2][v]; - if( options::fmfBoundMinMode()==FMF_BOUND_MIN_ALL || options::fmfBoundMinMode()==FMF_BOUND_MIN_SET_CARD ){ - d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] ); + // only handles infinite element types currently (cardinality is not + // supported for finite element types #1123). Regardless, this is + // typically not a limitation since this variable can be bound in a + // standard way below since its type is finite. + if (!v.getType().isInterpretedFinite()) + { + setBoundedVar(f, v, BOUND_SET_MEMBER); + setBoundVar = true; + 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] = nm->mkNode(CARD, d_setm_range[f][v]); + Trace("bound-int") << "Variable " << v + << " is bound because of set membership literal " + << bound_lit_map[2][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; @@ -644,10 +650,14 @@ bool BoundedIntegers::isGroundRange( Node q, Node v ) { Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) { Node sr = d_setm_range[q][v]; if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){ + Trace("bound-int-rsi-debug") + << sr << " is non-ground, apply substitution..." << std::endl; //get the substitution std::vector< Node > vars; std::vector< Node > subs; if( getRsiSubsitution( q, v, vars, subs, rsi ) ){ + Trace("bound-int-rsi-debug") + << " apply " << vars << " -> " << subs << std::endl; sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); }else{ sr = Node::null(); @@ -658,73 +668,80 @@ Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) { Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { Node sr = getSetRange( q, v, rsi ); - if( !sr.isNull() ){ - Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; - sr = d_quantEngine->getModel()->getValue( sr ); - //if non-constant, then sr does not occur in the model, we fail - if( !sr.isConst() ){ - return Node::null(); - } - Trace("bound-int-rsi") << "Value is " << sr << std::endl; - //as heuristic, map to term model - if( sr.getKind()!=EMPTYSET ){ - std::map< Node, Node > val_to_term; - while( sr.getKind()==UNION ){ - Assert( sr[1].getKind()==kind::SINGLETON ); - val_to_term[ sr[1][0] ] = sr[1][0]; - sr = sr[0]; - } - Assert( sr.getKind()==kind::SINGLETON ); - val_to_term[ sr[0] ] = sr[0]; - //must look back at assertions, not term database (theory of sets introduces extraneous terms internally) - Theory* theory = d_quantEngine->getTheoryEngine()->theoryOf( THEORY_SETS ); - if( theory ){ - context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for( unsigned i = 0; it != it_end; ++ it, ++i ){ - Node lit = (*it).assertion; - if( lit.getKind()==kind::MEMBER ){ - Node vr = d_quantEngine->getModel()->getValue( lit[0] ); - Trace("bound-int-rsi-debug") << "....membership for " << lit << " ==> " << vr << std::endl; - Trace("bound-int-rsi-debug") << " " << (val_to_term.find( vr )!=val_to_term.end()) << " " << d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) << std::endl; - if( val_to_term.find( vr )!=val_to_term.end() ){ - if( d_quantEngine->getEqualityQuery()->areEqual( d_setm_range_lit[q][v][1], lit[1] ) ){ - Trace("bound-int-rsi") << " Map value to term : " << vr << " -> " << lit[0] << std::endl; - val_to_term[ vr ] = lit[0]; - } - } - } - } - } - //rebuild value - Node nsr; - for( std::map< Node, Node >::iterator it = val_to_term.begin(); it != val_to_term.end(); ++it ){ - Node nv = NodeManager::currentNM()->mkNode( kind::SINGLETON, it->second ); - if( nsr.isNull() ){ - nsr = nv; - }else{ - nsr = NodeManager::currentNM()->mkNode( kind::UNION, nsr, nv ); - } - } - Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl; - return nsr; - - /* - Node lit = d_setm_range_lit[q][v]; - Trace("bound-int-rsi-debug") << "Bounded from lit " << lit << std::endl; - Node f = d_quantEngine->getTermDatabase()->getMatchOperator( lit ); - TermArgTrie * ta = d_quantEngine->getTermDatabase()->getTermArgTrie( f ); - if( ta ){ - Trace("bound-int-rsi-debug") << "Got term index for " << f << std::endl; - for( std::map< TNode, TermArgTrie >::iterator it = ta->d_data.begin(); it != ta->d_data.end(); ++it ){ - - } + if (sr.isNull()) + { + return sr; + } + Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; + Assert(!sr.hasFreeVar()); + Node sro = sr; + sr = d_quantEngine->getModel()->getValue(sr); + // if non-constant, then sr does not occur in the model, we fail + if (!sr.isConst()) + { + return Node::null(); + } + Trace("bound-int-rsi") << "Value is " << sr << std::endl; + if (sr.getKind() == EMPTYSET) + { + return sr; + } + NodeManager* nm = NodeManager::currentNM(); + Node nsr; + TypeNode tne = sr.getType().getSetElementType(); + // we can use choice functions for canonical symbolic instantiations + unsigned srCard = 0; + while (sr.getKind() == UNION) + { + srCard++; + sr = sr[0]; + } + Assert(sr.getKind() == SINGLETON); + srCard++; + // choices[i] stores the canonical symbolic representation of the (i+1)^th + // element of sro + std::vector choices; + Node srCardN = nm->mkNode(CARD, sro); + Node choice_i; + for (unsigned i = 0; i < srCard; i++) + { + if (i == d_setm_choice[sro].size()) + { + choice_i = nm->mkBoundVar(tne); + choices.push_back(choice_i); + Node cBody = nm->mkNode(MEMBER, choice_i, sro); + if (choices.size() > 1) + { + cBody = nm->mkNode(AND, cBody, nm->mkNode(DISTINCT, choices)); } - */ + choices.pop_back(); + Node bvl = nm->mkNode(BOUND_VAR_LIST, choice_i); + Node cMinCard = nm->mkNode(LEQ, srCardN, nm->mkConst(Rational(i))); + choice_i = nm->mkNode(CHOICE, bvl, nm->mkNode(OR, cMinCard, cBody)); + d_setm_choice[sro].push_back(choice_i); + } + Assert(i < d_setm_choice[sro].size()); + choice_i = d_setm_choice[sro][i]; + choices.push_back(choice_i); + Node sChoiceI = nm->mkNode(SINGLETON, choice_i); + if (nsr.isNull()) + { + nsr = sChoiceI; + } + else + { + nsr = nm->mkNode(UNION, nsr, sChoiceI); } - } - return sr; + // turns the concrete model value of sro into a canonical representation + // e.g. + // singleton(0) union singleton(1) + // becomes + // C1 union ( choice y. card(S)<=1 OR ( y in S AND distinct( y, C1 ) ) ) + // where C1 = ( choice x. card(S)<=0 OR x in S ). + Trace("bound-int-rsi") << "...reconstructed " << nsr << std::endl; + return nsr; } bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) { diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index c6293f1fe..90928c0bc 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -62,6 +62,14 @@ private: //set membership range std::map< Node, std::map< Node, Node > > d_setm_range; std::map< Node, std::map< Node, Node > > d_setm_range_lit; + /** set membership element choice functions + * + * For each set S and integer n, d_setm_choice[S][n] is the canonical + * representation for the (n+1)^th member of set S. It is of the form: + * choice x. (|S| <= n OR ( x in S AND + * distinct( x, d_setm_choice[S][0], ..., d_setm_choice[S][n-1] ) ) ) + */ + std::map > d_setm_choice; //fixed finite set range std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range; std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 7b5244a04..49954c111 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -533,6 +533,7 @@ void TheorySetsPrivate::fullEffortCheck(){ d_bop_index.clear(); d_op_list.clear(); d_card_enabled = false; + d_t_card_enabled.clear(); d_rels_enabled = false; d_eqc_to_card_term.clear(); @@ -622,12 +623,23 @@ void TheorySetsPrivate::fullEffortCheck(){ }else if( n.getKind()==kind::CARD ){ d_card_enabled = true; TypeNode tnc = n[0].getType().getSetElementType(); + d_t_card_enabled[tnc] = true; if( tnc.isInterpretedFinite() ){ std::stringstream ss; - ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl; + ss << "ERROR: cannot use cardinality on sets with finite element " + "type (term is " + << n << ")." << std::endl; throw LogicException(ss.str()); //TODO: extend approach for this case } + // if we do not handle the kind, set incomplete + Kind nk = n[0].getKind(); + if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk)) + { + d_full_check_incomplete = true; + Trace("sets-incomplete") + << "Sets : incomplete because of " << n << "." << std::endl; + } Node r = d_equalityEngine.getRepresentative( n[0] ); if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){ d_eqc_to_card_term[ r ] = n; @@ -1037,6 +1049,12 @@ void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) { } void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){ + TypeNode tnc = n.getType().getSetElementType(); + if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end()) + { + // if no cardinality constraints for sets of this type, we can ignore + return; + } if( d_card_processed.find( n )==d_card_processed.end() ){ d_card_processed.insert( n ); Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl; @@ -1724,16 +1742,10 @@ void TheorySetsPrivate::check(Theory::Effort level) { fullEffortCheck(); if( !d_conflict && !d_sentLemma ){ //invoke relations solver - d_rels->check(level); - if( d_card_enabled && ( d_rels_enabled || options::setsExt() ) ){ - //if cardinality constraints are enabled, - // then model construction may fail in there are relational operators, or universe set. - // TODO: should internally check model, return unknown if fail - d_full_check_incomplete = true; - Trace("sets-incomplete") << "Sets : incomplete because of extended operators." << std::endl; - } + d_rels->check(level); } - if( d_full_check_incomplete ){ + if (!d_conflict && !d_sentLemma && d_full_check_incomplete) + { d_external.d_out->setIncomplete(); } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 57a7aaf65..31aec85c3 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -141,6 +141,8 @@ private: //cardinality private: bool d_card_enabled; + /** element types of sets for which cardinality is enabled */ + std::map d_t_card_enabled; bool d_rels_enabled; std::map< Node, Node > d_eqc_to_card_term; NodeSet d_card_processed; diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index cef27bc72..48b290bfe 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1104,6 +1104,7 @@ REG1_TESTS = \ regress1/fmf/nlp042+1.smt2 \ regress1/fmf/nun-0208-to.smt2 \ regress1/fmf/pow2-bool.smt2 \ + regress1/fmf/radu-quant-set.smt2 \ regress1/fmf/refcount24.cvc.smt2 \ regress1/fmf/sc-crash-052316.smt2 \ regress1/fmf/with-ind-104-core.smt2 \ @@ -1309,6 +1310,7 @@ REG1_TESTS = \ regress1/quantifiers/rew-to-0211-dd.smt2 \ regress1/quantifiers/ricart-agrawala6.smt2 \ regress1/quantifiers/set8.smt2 \ + regress1/quantifiers/set-choice-koikonomou.cvc \ regress1/quantifiers/small-pipeline-fixpoint-3.smt2 \ regress1/quantifiers/smtcomp-qbv-053118.smt2 \ regress1/quantifiers/smtlib384a03.smt2 \ diff --git a/test/regress/regress1/fmf/radu-quant-set.smt2 b/test/regress/regress1/fmf/radu-quant-set.smt2 new file mode 100644 index 000000000..09d5cc706 --- /dev/null +++ b/test/regress/regress1/fmf/radu-quant-set.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-bound +; EXPECT: unsat +(set-logic ALL_SUPPORTED) + +(declare-const A (Set Int)) +(declare-const B (Set Int)) + +(define-fun F () Bool + (exists ((i Int) (j Int)) (and (distinct i j) (member i A) (member j B))) +) + +(define-fun G () Bool + (and (>= (card (union A B)) 2) (>= (card A) 1) (>= (card B) 1)) +) + +(assert (and G (not F))) + +(check-sat) diff --git a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc new file mode 100644 index 000000000..f7407a2a5 --- /dev/null +++ b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +OPTION "finite-model-find"; +OPTION "fmf-bound-int"; + +X : SET OF INT; + +ASSERT CARD(X) = 3; +ASSERT FORALL(z: INT): z IS_IN X => (z > 0 AND z < 2); % 1 + +QUERY FORALL(z: INT): z IS_IN X => z > 0; -- 2.30.2