From 0d12fcbb5f1c047f951a69aa6ef4ae127f499312 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 21 Jul 2018 09:19:31 -0500 Subject: [PATCH] Optimizations and fixes for computing whether a type is finite (#2179) --- src/expr/type_node.cpp | 89 +++++++---- src/options/quantifiers_options.toml | 9 ++ src/theory/datatypes/datatypes_sygus.cpp | 4 +- src/theory/datatypes/theory_datatypes.cpp | 14 +- src/theory/datatypes/type_enumerator.cpp | 1 - src/theory/quantifiers/fmf/model_engine.cpp | 3 +- src/theory/quantifiers/term_enumeration.cpp | 21 ++- src/util/cardinality.h | 3 +- test/regress/Makefile.tests | 1 + .../regress1/sygus/array_search_5-Q-easy.sy | 144 ++++++++++++++++++ 10 files changed, 245 insertions(+), 44 deletions(-) create mode 100644 test/regress/regress1/sygus/array_search_5-Q-easy.sy diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index d6cf12d41..6616f470f 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -83,46 +83,81 @@ bool TypeNode::isInterpretedFinite() if (!getAttribute(IsInterpretedFiniteComputedAttr())) { bool isInterpretedFinite = false; - if (getCardinality().isFinite()) + if (isSort()) + { + // If the finite model finding flag is set, we treat uninterpreted sorts + // as finite. If it is not set, we treat them implicitly as infinite + // sorts (that is, their cardinality is not constrained to be finite). + isInterpretedFinite = options::finiteModelFind(); + } + else if (isBitVector() || isFloatingPoint()) { isInterpretedFinite = true; } - else if (options::finiteModelFind()) + else if (isDatatype()) { - if( isSort() ){ - isInterpretedFinite = true; - }else if( isDatatype() ){ - TypeNode tn = *this; - const Datatype& dt = getDatatype(); - isInterpretedFinite = dt.isInterpretedFinite(tn.toType()); - }else if( isArray() ){ - isInterpretedFinite = - getArrayIndexType().isInterpretedFinite() - && getArrayConstituentType().isInterpretedFinite(); - }else if( isSet() ) { - isInterpretedFinite = getSetElementType().isInterpretedFinite(); + TypeNode tn = *this; + const Datatype& dt = getDatatype(); + isInterpretedFinite = dt.isInterpretedFinite(tn.toType()); + } + else if (isArray()) + { + TypeNode tnc = getArrayConstituentType(); + if (!tnc.isInterpretedFinite()) + { + // arrays with consistuent type that is infinite are infinite + isInterpretedFinite = false; } - else if (isFunction()) + else if (getArrayIndexType().isInterpretedFinite()) { + // arrays with both finite consistuent and index types are finite isInterpretedFinite = true; - if (!getRangeType().isInterpretedFinite()) - { - isInterpretedFinite = false; - } - else + } + else + { + // If the consistuent type of the array has cardinality one, then the + // array type has cardinality one, independent of the index type. + isInterpretedFinite = tnc.getCardinality().isOne(); + } + } + else if (isSet()) + { + isInterpretedFinite = getSetElementType().isInterpretedFinite(); + } + else if (isFunction()) + { + isInterpretedFinite = true; + TypeNode tnr = getRangeType(); + if (!tnr.isInterpretedFinite()) + { + isInterpretedFinite = false; + } + else + { + std::vector argTypes = getArgTypes(); + for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) { - std::vector argTypes = getArgTypes(); - for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) + if (!argTypes[i].isInterpretedFinite()) { - if (!argTypes[i].isInterpretedFinite()) - { - isInterpretedFinite = false; - break; - } + isInterpretedFinite = false; + break; } } + if (!isInterpretedFinite) + { + // similar to arrays, functions are finite if their range type + // has cardinality one, regardless of the arguments. + isInterpretedFinite = tnr.getCardinality().isOne(); + } } } + else + { + // by default, compute the exact cardinality for the type and check + // whether it is finite. This should be avoided in general, since + // computing cardinalities for types can be highly expensive. + isInterpretedFinite = getCardinality().isFinite(); + } setAttribute(IsInterpretedFiniteAttr(), isInterpretedFinite); setAttribute(IsInterpretedFiniteComputedAttr(), true); return isInterpretedFinite; diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8e954ddc0..8c7414fa7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -637,6 +637,15 @@ header = "options/quantifiers_options.h" read_only = true help = "mode for which types of bounds to minimize via first decision heuristics" +[[option]] + name = "fmfTypeCompletionThresh" + category = "regular" + long = "fmf-type-completion-thresh=N" + type = "int" + default = "1000" + read_only = true + help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted" + [[option]] name = "quantConflictFind" category = "regular" diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 49132dc46..d95a5763c 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -568,7 +568,9 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(TypeNode tn, unsigned c1 = deq_child[0][i]; unsigned c2 = deq_child[1][i]; TypeNode tnc = children[c1].getType(); - if (tnc == children[c2].getType() && !tnc.getCardinality().isOne()) + // we may only apply this symmetry breaking scheme (which introduces + // disequalities) if the types are infinite. + if (tnc == children[c2].getType() && !tnc.isInterpretedFinite()) { Node sym_lem_deq = children[c1].eqNode(children[c2]).negate(); // notice that this symmetry breaking still allows for diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index e3b48a4da..cf690af57 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -202,7 +202,9 @@ void TheoryDatatypes::check(Effort e) { Trace("datatypes-debug") << "No constructor..." << std::endl; Type tt = tn.toType(); const Datatype& dt = ((DatatypeType)tt).getDatatype(); - Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite( tt ) << " " << dt.isInterpretedFinite( tt ) << " " << dt.isRecursiveSingleton( tt ) << std::endl; + Trace("datatypes-debug") + << "Datatype " << dt << " is " << dt.isInterpretedFinite(tt) + << " " << dt.isRecursiveSingleton(tt) << std::endl; bool continueProc = true; if( dt.isRecursiveSingleton( tt ) ){ Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; @@ -263,7 +265,13 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( !dt[ j ].isInterpretedFinite( tt ) ) { + Trace("datatypes-debug") << j << " compute finite..." + << std::endl; + bool ifin = dt[j].isInterpretedFinite(tt); + Trace("datatypes-debug") << "...returned " << ifin + << std::endl; + if (!ifin) + { if( !eqc || !eqc->d_selectors ){ needSplit = false; } @@ -1752,8 +1760,6 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ tt = exp[0]; } const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); - //must be finite or have a selector - //if( eqc->d_selectors || dt[ index ].isFinite() ){ //instantiate this equivalence class eqc->d_inst = true; Node tt_cons = getInstantiateCons( tt, dt, index ); diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 4a69a9442..afe6e182f 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -171,7 +171,6 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; Debug("dt-enum") << "datatype is " << d_type << std::endl; Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() ); - Debug("dt-enum") << " " << d_datatype.isFinite( d_type.toType() ) << std::endl; Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl; if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index f05246ddb..6763a0ad3 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -136,7 +136,8 @@ void ModelEngine::registerQuantifier( Node f ){ for( unsigned i=0; imkConst( - Rational(tn.getCardinality().getFiniteCardinality())); - Node oth = NodeManager::currentNM()->mkConst(Rational(1000)); - Node eq = NodeManager::currentNM()->mkNode(LEQ, card, oth); - eq = Rewriter::rewrite(eq); - mc = eq.isConst() && eq.getConst(); + Cardinality c = tn.getCardinality(); + if (!c.isLargeFinite()) + { + NodeManager* nm = NodeManager::currentNM(); + Node card = nm->mkConst(Rational(c.getFiniteCardinality())); + // check if less than fixed upper bound, default 1000 + Node oth = nm->mkConst(Rational(options::fmfTypeCompletionThresh())); + Node eq = nm->mkNode(LEQ, card, oth); + eq = Rewriter::rewrite(eq); + mc = eq.isConst() && eq.getConst(); + } } d_may_complete[tn] = mc; return mc; diff --git a/src/util/cardinality.h b/src/util/cardinality.h index b45f6bcc2..956468e30 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -135,8 +135,7 @@ class CVC4_PUBLIC Cardinality { /** Returns true iff this cardinality is finite. */ bool isFinite() const { return d_card > 0; } /** Returns true iff this cardinality is one */ - bool isOne() const { return d_card == 1; } - + bool isOne() const { return d_card == 2; } /** * Returns true iff this cardinality is finite and large (i.e., * at the ceiling of representable finite cardinalities). diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index b005a3a67..aa896258f 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1491,6 +1491,7 @@ REG1_TESTS = \ regress1/strings/username_checker_min.smt2 \ regress1/sygus/VC22_a.sy \ regress1/sygus/array_search_2.sy \ + regress1/sygus/array_search_5-Q-easy.sy \ regress1/sygus/array_sum_2_5.sy \ regress1/sygus/cegar1.sy \ regress1/sygus/cegisunif-depth1.sy \ diff --git a/test/regress/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/regress1/sygus/array_search_5-Q-easy.sy new file mode 100644 index 000000000..e1f37d2cd --- /dev/null +++ b/test/regress/regress1/sygus/array_search_5-Q-easy.sy @@ -0,0 +1,144 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status +( set-logic LIA ) +( synth-fun findIdx ( ( y1 Int ) ( y2 Int ) ( y3 Int ) ( y4 Int ) ( y5 Int ) ( k1 Int ) ) Int ( + (Start Int ( NT1 + NT3 + NT4 + NT7 + NT8 + NT9 + NT10 + NT11 + NT13 + NT14 +)) + (NT1 Int ( y5 + k1 + 1 + y2 + 0 + y1 + 2 + 5 + y4 + 4 + y3 + 3 +)) + (NT2 Bool ( (< NT1 NT1) + (> NT1 NT1) + (>= NT1 NT1) + (<= NT1 NT1) +)) + (NT3 Int ( (ite NT2 NT1 NT1) +)) + (NT4 Int ( (ite NT5 NT1 NT1) + (ite NT2 NT3 NT1) +)) + (NT5 Bool ( (< NT3 NT1) + (<= NT3 NT1) + (>= NT3 NT1) + (> NT3 NT1) +)) + (NT6 Bool ( (<= NT4 NT1) + (> NT4 NT1) + (<= NT3 NT3) + (> NT3 NT3) + (>= NT4 NT1) + (< NT4 NT1) + (< NT3 NT3) + (>= NT3 NT3) +)) + (NT7 Int ( (ite NT6 NT1 NT1) + (ite NT2 NT4 NT1) +)) + (NT8 Int ( (ite NT2 NT7 NT1) + (ite NT5 NT4 NT1) + (ite NT15 NT1 NT1) + (ite NT5 NT1 NT4) +)) + (NT9 Int ( (ite NT2 NT8 NT1) + (ite NT12 NT1 NT1) + (ite NT6 NT1 NT4) + (ite NT6 NT4 NT1) + (ite NT5 NT7 NT1) +)) + (NT10 Int ( (ite NT5 NT8 NT1) + (ite NT16 NT1 NT1) + (ite NT2 NT9 NT1) + (ite NT6 NT7 NT1) + (ite NT5 NT4 NT4) +)) + (NT11 Int ( (ite NT6 NT8 NT1) + (ite NT2 NT10 NT1) + (ite NT5 NT9 NT1) + (ite NT17 NT1 NT1) + (ite NT6 NT4 NT4) +)) + (NT12 Bool ( (< NT4 NT4) + (> NT4 NT4) + (<= NT8 NT1) + (< NT8 NT1) + (<= NT4 NT4) + (> NT8 NT1) + (>= NT8 NT1) + (>= NT4 NT4) +)) + (NT13 Int ( (ite NT18 NT1 NT1) + (ite NT12 NT7 NT1) + (ite NT5 NT10 NT1) + (ite NT6 NT9 NT1) + (ite NT12 NT1 NT7) + (ite NT2 NT11 NT1) +)) + (NT14 Int ( (ite NT12 NT1 NT8) + (ite NT6 NT10 NT1) + (ite NT5 NT11 NT1) + (ite NT19 NT1 NT1) + (ite NT12 NT8 NT1) + (ite NT2 NT13 NT1) +)) + (NT15 Bool ( (>= NT7 NT1) + (< NT7 NT1) + (> NT7 NT1) + (<= NT7 NT1) +)) + (NT16 Bool ( (< NT9 NT1) + (>= NT9 NT1) + (> NT9 NT1) + (<= NT9 NT1) +)) + (NT17 Bool ( (< NT7 NT7) + (<= NT10 NT1) + (>= NT10 NT1) + (> NT10 NT1) + (< NT10 NT1) + (> NT7 NT7) + (>= NT7 NT7) + (<= NT7 NT7) +)) + (NT18 Bool ( (< NT11 NT1) + (> NT11 NT1) + (>= NT11 NT1) + (<= NT11 NT1) +)) + (NT19 Bool ( (>= NT13 NT1) + (>= NT8 NT8) + (< NT13 NT1) + (> NT13 NT1) + (< NT8 NT8) + (> NT8 NT8) + (<= NT8 NT8) + (<= NT13 NT1) +)) +)) + ( declare-var x1 Int ) + ( declare-var x2 Int ) + ( declare-var x3 Int ) + ( declare-var x4 Int ) + ( declare-var x5 Int ) + ( declare-var k Int ) + ( constraint ( => ( and ( < x1 x2 ) ( and ( < x2 x3 ) ( and ( < x3 x4 ) ( < x4 x5 ) ) ) ) ( => ( < k x1 ) ( = ( findIdx x1 x2 x3 x4 x5 k ) 0 ) ) ) ) + ( check-synth ) + -- 2.30.2