From a983ec175a7b7a2c247274735b9740c417114d94 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Sep 2019 22:15:38 -0500 Subject: [PATCH] Avoid computing cardinality when constructing models (#3268) --- src/expr/datatype.cpp | 3 +- src/expr/type.cpp | 12 ++ src/expr/type.h | 13 ++ src/expr/type_node.cpp | 111 +++++++++++++----- src/expr/type_node.h | 21 +++- src/theory/theory_model_builder.cpp | 3 +- test/regress/CMakeLists.txt | 1 + .../regress1/datatypes/issue3266-small.smt2 | 37 ++++++ 8 files changed, 165 insertions(+), 36 deletions(-) create mode 100644 test/regress/regress1/datatypes/issue3266-small.smt2 diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index cd78728b1..4ec6ac36a 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -1031,7 +1031,8 @@ bool DatatypeConstructor::isFinite(Type t) const if( DatatypeType(t).isParametric() ){ tc = tc.substitute( paramTypes, instTypes ); } - if(! tc.getCardinality().isFinite()) { + if (!tc.isFinite()) + { self.setAttribute(DatatypeFiniteComputedAttr(), true); self.setAttribute(DatatypeFiniteAttr(), false); return false; diff --git a/src/expr/type.cpp b/src/expr/type.cpp index f2b5945dd..76c318b2e 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -67,6 +67,18 @@ Cardinality Type::getCardinality() const { return d_typeNode->getCardinality(); } +bool Type::isFinite() const +{ + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isFinite(); +} + +bool Type::isInterpretedFinite() const +{ + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isInterpretedFinite(); +} + bool Type::isWellFounded() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isWellFounded(); diff --git a/src/expr/type.h b/src/expr/type.h index 2c68c9e73..587df07ee 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -139,6 +139,19 @@ protected: */ Cardinality getCardinality() const; + /** + * Is this type finite? This assumes uninterpreted sorts have infinite + * cardinality. + */ + bool isFinite() const; + + /** + * Is this type interpreted as being finite. + * If finite model finding is enabled, this assumes all uninterpreted sorts + * are interpreted as finite. + */ + bool isInterpretedFinite() const; + /** * Is this a well-founded type? */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b093e596e..9db29f115 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -66,103 +66,156 @@ Cardinality TypeNode::getCardinality() const { return kind::getCardinality(*this); } +/** Attribute true for types that are finite */ +struct IsFiniteTag +{ +}; +typedef expr::Attribute IsFiniteAttr; +/** Attribute true for types which we have computed the above attribute */ +struct IsFiniteComputedTag +{ +}; +typedef expr::Attribute IsFiniteComputedAttr; + /** Attribute true for types that are interpreted as finite */ struct IsInterpretedFiniteTag { }; +typedef expr::Attribute IsInterpretedFiniteAttr; +/** Attribute true for types which we have computed the above attribute */ struct IsInterpretedFiniteComputedTag { }; -typedef expr::Attribute IsInterpretedFiniteAttr; typedef expr::Attribute IsInterpretedFiniteComputedAttr; +bool TypeNode::isFinite() { return isFiniteInternal(false); } + bool TypeNode::isInterpretedFinite() +{ + return isFiniteInternal(options::finiteModelFind()); +} + +bool TypeNode::isFiniteInternal(bool usortFinite) { // check it is already cached - if (!getAttribute(IsInterpretedFiniteComputedAttr())) + if (usortFinite) { - bool isInterpretedFinite = false; - if (isSort()) + if (getAttribute(IsInterpretedFiniteComputedAttr())) { - // 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(); + return getAttribute(IsInterpretedFiniteAttr()); } - else if (isBitVector() || isFloatingPoint()) + } + else if (getAttribute(IsFiniteComputedAttr())) + { + return getAttribute(IsFiniteAttr()); + } + bool ret = false; + if (isSort()) + { + ret = usortFinite; + } + else if (isBoolean() || isBitVector() || isFloatingPoint()) + { + ret = true; + } + else if (isString() || isRegExp() || isReal()) + { + ret = false; + } + else + { + // recursive case (this may be a parametric sort), we assume infinite for + // the moment here to prevent infinite loops + if (usortFinite) { - isInterpretedFinite = true; + setAttribute(IsInterpretedFiniteAttr(), false); + setAttribute(IsInterpretedFiniteComputedAttr(), true); } - else if (isDatatype()) + else + { + setAttribute(IsFiniteAttr(), false); + setAttribute(IsFiniteComputedAttr(), true); + } + if (isDatatype()) { TypeNode tn = *this; const Datatype& dt = getDatatype(); - isInterpretedFinite = dt.isInterpretedFinite(tn.toType()); + ret = usortFinite ? dt.isInterpretedFinite(tn.toType()) + : dt.isFinite(tn.toType()); } else if (isArray()) { TypeNode tnc = getArrayConstituentType(); - if (!tnc.isInterpretedFinite()) + if (!tnc.isFiniteInternal(usortFinite)) { // arrays with consistuent type that is infinite are infinite - isInterpretedFinite = false; + ret = false; } - else if (getArrayIndexType().isInterpretedFinite()) + else if (getArrayIndexType().isFiniteInternal(usortFinite)) { // arrays with both finite consistuent and index types are finite - isInterpretedFinite = true; + ret = true; } 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(); + ret = tnc.getCardinality().isOne(); } } else if (isSet()) { - isInterpretedFinite = getSetElementType().isInterpretedFinite(); + ret = getSetElementType().isFiniteInternal(usortFinite); } else if (isFunction()) { - isInterpretedFinite = true; + ret = true; TypeNode tnr = getRangeType(); - if (!tnr.isInterpretedFinite()) + if (!tnr.isFiniteInternal(usortFinite)) { - isInterpretedFinite = false; + ret = false; } else { std::vector argTypes = getArgTypes(); for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++) { - if (!argTypes[i].isInterpretedFinite()) + if (!argTypes[i].isFiniteInternal(usortFinite)) { - isInterpretedFinite = false; + ret = false; break; } } - if (!isInterpretedFinite) + if (!ret) { // similar to arrays, functions are finite if their range type // has cardinality one, regardless of the arguments. - isInterpretedFinite = tnr.getCardinality().isOne(); + ret = tnr.getCardinality().isOne(); } } } else { + // all types should be handled above + Assert(false); // 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(); + ret = getCardinality().isFinite(); } - setAttribute(IsInterpretedFiniteAttr(), isInterpretedFinite); + } + if (usortFinite) + { + setAttribute(IsInterpretedFiniteAttr(), ret); setAttribute(IsInterpretedFiniteComputedAttr(), true); - return isInterpretedFinite; } - return getAttribute(IsInterpretedFiniteAttr()); + else + { + setAttribute(IsFiniteAttr(), ret); + setAttribute(IsFiniteComputedAttr(), true); + } + return ret; } /** Attribute true for types that are closed enumerable */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 8ed26596b..c5e1f400c 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -421,10 +421,16 @@ public: * @return a finite or infinite cardinality */ Cardinality getCardinality() const; - + /** - * Is this type interpreted as being finite. - * If finite model finding is enabled, this assumes all uninterpreted sorts + * Is this type finite? This assumes uninterpreted sorts have infinite + * cardinality. + */ + bool isFinite(); + + /** + * Is this type interpreted as finite. + * If finite model finding is enabled, this assumes all uninterpreted sorts * are interpreted as finite. */ bool isInterpretedFinite(); @@ -665,7 +671,14 @@ public: static Node getEnsureTypeCondition( Node n, TypeNode tn ); private: static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast); - + + /** + * Is this type interpreted as finite. + * If the flag usortFinite is true, this assumes all uninterpreted sorts + * are interpreted as finite. + */ + bool isFiniteInternal(bool usortFinite); + /** * Indents the given stream a given amount of spaces. * diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 0aa6ea5cc..d3fde58a7 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -683,9 +683,8 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) Assert(!t.isBoolean() || (*i2).isVar() || (*i2).getKind() == kind::APPLY_UF); Node n; - if (t.getCardinality().isInfinite()) + if (!t.isFinite()) { - // if (!t.isInterpretedFinite()) { bool success; do { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 607e1a568..c456ed2e8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1135,6 +1135,7 @@ set(regress_1_tests regress1/datatypes/dt-color-2.6.smt2 regress1/datatypes/dt-param-card4-unsat.smt2 regress1/datatypes/error.cvc + regress1/datatypes/issue3266-small.smt2 regress1/datatypes/manos-model.smt2 regress1/decision/error3.smtv1.smt2 regress1/decision/quant-Arrays_Q1-noinfer.smt2 diff --git a/test/regress/regress1/datatypes/issue3266-small.smt2 b/test/regress/regress1/datatypes/issue3266-small.smt2 new file mode 100644 index 000000000..c57268cc9 --- /dev/null +++ b/test/regress/regress1/datatypes/issue3266-small.smt2 @@ -0,0 +1,37 @@ +; COMMAND-LINE: --incremental +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes () ((a0(c0$0)(c0$1)(c0$2)(c0$3(c0$3$0 a8)(c0$3$1 Int))(c0$4(c0$4$0 a5)(c0$4$1 a6))(c0$5)(c0$6)(c0$7)(c0$8))(a1(c1$0)(c1$1(c1$1$0 a4)(c1$1$1 Bool)(c1$1$2 a6)(c1$1$3 a4)(c1$1$4 ab)(c1$1$5 Int)(c1$1$6 a0))(c1$2)(c1$3)(c1$4)(c1$5(c1$5$0 a7))(c1$6(c1$6$0 String)(c1$6$1 a4)(c1$6$2 a4)(c1$6$3 a0))(c1$7))(a2(c2$0)(c2$1(c2$1$0 aa)(c2$1$1 aa)(c2$1$2 a1)(c2$1$3 a0)(c2$1$4 a0)(c2$1$5 a0)(c2$1$6 a9))(c2$2(c2$2$0 a5)(c2$2$1 ab))(c2$3(c2$3$0 Bool)(c2$3$1 a7)(c2$3$2 a3)(c2$3$3 Bool)(c2$3$4 a0)(c2$3$5 String))(c2$4))(a3(c3$0(c3$0$0 a7))(c3$1)(c3$2)(c3$3)(c3$4)(c3$5)(c3$6)(c3$7)(c3$8)(c3$9)(c3$a)(c3$b)(c3$c))(a4(c4$0(c4$0$0 a2)(c4$0$1 a1)(c4$0$2 Bool)(c4$0$3 String)(c4$0$4 a3)(c4$0$5 Int)(c4$0$6 a2)))(a5(c5$0)(c5$1)(c5$2(c5$2$0 String))(c5$3)(c5$4)(c5$5)(c5$6(c5$6$0 a0)(c5$6$1 a6)(c5$6$2 a3)(c5$6$3 a3)(c5$6$4 a9))(c5$7))(a6(c6$0)(c6$1(c6$1$0 a7))(c6$2)(c6$3)(c6$4(c6$4$0 a7)(c6$4$1 a3)(c6$4$2 a4))(c6$5(c6$5$0 a9)(c6$5$1 a9)(c6$5$2 a7)(c6$5$3 a6)(c6$5$4 ab)(c6$5$5 a5)(c6$5$6 a3)(c6$5$7 aa))(c6$6)(c6$7)(c6$8)(c6$9)(c6$a)(c6$b)(c6$c))(a7(c7$0)(c7$1)(c7$2)(c7$3(c7$3$0 a8)(c7$3$1 Bool)(c7$3$2 Int)(c7$3$3 a5)(c7$3$4 a8))(c7$4)(c7$5)(c7$6)(c7$7)(c7$8(c7$8$0 a5)(c7$8$1 a1)))(a8(c8$0(c8$0$0 a6)(c8$0$1 ab)(c8$0$2 ab)(c8$0$3 a1)(c8$0$4 Bool))(c8$1(c8$1$0 a4)(c8$1$1 Bool)(c8$1$2 a2)(c8$1$3 String)(c8$1$4 Bool)))(a9(c9$0(c9$0$0 String))(c9$1(c9$1$0 String)(c9$1$1 ab))(c9$2(c9$2$0 a5)(c9$2$1 a9))(c9$3(c9$3$0 String)(c9$3$1 a8)(c9$3$2 a6))(c9$4)(c9$5))(aa(ca$0(ca$0$0 String)(ca$0$1 a3)(ca$0$2 a9)(ca$0$3 a3)(ca$0$4 Bool)(ca$0$5 a1)(ca$0$6 a1)(ca$0$7 a4))(ca$1)(ca$2(ca$2$0 a4)(ca$2$1 String)(ca$2$2 aa)(ca$2$3 ab)))(ab(cb$0(cb$0$0 a5)(cb$0$1 a2)(cb$0$2 a3)(cb$0$3 aa)(cb$0$4 Bool))(cb$1(cb$1$0 a0))(cb$2)(cb$3)(cb$4)(cb$5)(cb$6)(cb$7(cb$7$0 String)(cb$7$1 a0)(cb$7$2 a7)(cb$7$3 ab)(cb$7$4 aa)(cb$7$5 a8))(cb$8)))) +(push 1) +(declare-fun v0() a0) +(push 1) +(assert (is-c0$0 v0)) +(check-sat) +(pop 1) +(push 1) +(assert (is-c0$1 v0)) +(check-sat) +(pop 1) +(push 1) +(assert (is-c0$2 v0)) +(check-sat) +(pop 1) +(push 1) +(assert (is-c0$3 v0)) +(check-sat) +(pop 1) +(push 1) +(assert (is-c0$4 v0)) +(check-sat) +(pop 1) +(push 1) +(assert (is-c0$5 v0)) +(check-sat) + -- 2.30.2