From b13d2f7921a65b8921ef37b38a2d4579f7c911a2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 23 May 2016 14:28:29 -0500 Subject: [PATCH] Fix related to parametric sorts whose interpretation is finite due to uninterpreted sorts + FMF. Generalizes previous fix in term registration visitor. --- src/expr/datatype.cpp | 19 +++------ src/expr/datatype.h | 4 +- src/expr/type_node.cpp | 21 ++++++++++ src/expr/type_node.h | 7 ++++ src/theory/datatypes/theory_datatypes.cpp | 6 +-- src/theory/datatypes/type_enumerator.cpp | 2 +- src/theory/datatypes/type_enumerator.h | 2 +- src/theory/quantifiers/quant_split.cpp | 6 +-- src/theory/term_registration_visitor.cpp | 40 +++---------------- src/theory/theory_model.cpp | 1 + test/regress/regress0/fmf/Makefile.am | 3 +- .../regress/regress0/fmf/sc-crash-052316.smt2 | 35 ++++++++++++++++ 12 files changed, 86 insertions(+), 60 deletions(-) create mode 100644 test/regress/regress0/fmf/sc-crash-052316.smt2 diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index d14ac26d4..001f38a79 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -297,7 +297,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { return true; } -bool Datatype::isUFinite() const throw(IllegalArgumentException) { +bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); @@ -310,7 +310,7 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) { self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - if(! (*i).isUFinite()) { + if(! (*i).isInterpretedFinite()) { return false; } } @@ -850,7 +850,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return true; } -bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { +bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); @@ -859,18 +859,9 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { if(self.getAttribute(DatatypeUFiniteComputedAttr())) { return self.getAttribute(DatatypeUFiniteAttr()); } - bool success = true; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { - Type t = (*i).getRangeType(); - if( t.isDatatype() ){ - const Datatype& dt = ((DatatypeType)t).getDatatype(); - if( !dt.isUFinite() ){ - success = false; - } - }else if(!t.isSort() && !t.getCardinality().isFinite()) { - success = false; - } - if(!success ){ + TypeNode t = TypeNode::fromType( (*i).getRangeType() ); + if(!t.isInterpretedFinite()) { self.setAttribute(DatatypeUFiniteComputedAttr(), true); self.setAttribute(DatatypeUFiniteAttr(), false); return false; diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 1197b4a3b..dfd893fe8 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -342,7 +342,7 @@ public: * uninterpreted sorts are finite. This function can * only be called for resolved constructors. */ - bool isUFinite() const throw(IllegalArgumentException); + bool isInterpretedFinite() const throw(IllegalArgumentException); /** * Returns true iff this Datatype constructor has already been @@ -634,7 +634,7 @@ public: * datatype is not well-founded, this function returns false. The * Datatype must be resolved or an exception is thrown. */ - bool isUFinite() const throw(IllegalArgumentException); + bool isInterpretedFinite() const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 5d672e6ac..dc2370bea 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -21,6 +21,7 @@ #include "expr/type_properties.h" #include "options/base_options.h" #include "options/expr_options.h" +#include "options/quantifiers_options.h" using namespace std; @@ -64,6 +65,26 @@ Cardinality TypeNode::getCardinality() const { return kind::getCardinality(*this); } +bool TypeNode::isInterpretedFinite() const { + if( getCardinality().isFinite() ){ + return true; + }else{ + if( options::finiteModelFind() ){ + if( isSort() ){ + return true; + }else if( isDatatype() || isParametricDatatype() ){ + const Datatype& dt = getDatatype(); + return dt.isInterpretedFinite(); + }else if( isArray() ){ + return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite(); + }else if( isSet() ) { + return getSetElementType().isInterpretedFinite(); + } + } + return false; + } +} + bool TypeNode::isWellFounded() const { return kind::isWellFounded(*this); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index cfb61a085..46fdaa143 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -419,6 +419,13 @@ 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 + * are interpreted as finite. + */ + bool isInterpretedFinite() const; /** * Returns whether this type is well-founded. diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0100f1833..95d704a0e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -191,7 +191,7 @@ void TheoryDatatypes::check(Effort e) { if( !hasLabel( eqc, n ) ){ Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isUFinite() << " " << dt.isRecursiveSingleton() << std::endl; + Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isInterpretedFinite() << " " << dt.isRecursiveSingleton() << std::endl; bool continueProc = true; if( dt.isRecursiveSingleton() ){ Trace("datatypes-debug") << "Check recursive singleton..." << std::endl; @@ -252,7 +252,7 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( options::finiteModelFind() ? !dt[ j ].isUFinite() : !dt[ j ].isFinite() ) { + if( !dt[ j ].isInterpretedFinite() ) { if( !eqc || !eqc->d_selectors ){ needSplit = false; } @@ -1497,7 +1497,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( neqc.isNull() ){ for( unsigned i=0; i=d_has_debruijn+d_datatype.getNumConstructors() ){ //try next size limit as long as new terms were generated at last size, or other cases - if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || ( options::finiteModelFind() ? !d_datatype.isUFinite() : !d_datatype.isFinite() ) ){ + if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite() ){ d_size_limit++; d_ctor = d_zeroCtor; for( unsigned i=0; imax_score ){ max_index = i; max_score = score; diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 830e7f809..6b268805a 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -64,14 +64,8 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -130,14 +124,8 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -222,14 +210,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -244,14 +226,8 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } @@ -297,14 +273,8 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) { TypeNode type = current.getType(); typeTheoryId = Theory::theoryOf(type); if (typeTheoryId != currentTheoryId) { - if (options::finiteModelFind() && type.isSort()) { - // We're looking for finite models + if (type.isInterpretedFinite()) { useType = true; - } else { - Cardinality card = type.getCardinality(); - if (card.isFinite()) { - useType = true; - } } } } diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index fa7e497e2..6889d1002 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -832,6 +832,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF); Node n; if (t.getCardinality().isInfinite()) { + // if (!t.isInterpretedFinite()) { bool success; do{ Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl; diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 575aa4159..6e1c6e918 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -55,7 +55,8 @@ TESTS = \ datatypes-ufinite-nested.smt2 \ ForElimination-scala-9.smt2 \ agree466.smt2 \ - LeftistHeap.scala-8-ncm.smt2 + LeftistHeap.scala-8-ncm.smt2 \ + sc-crash-052316.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/sc-crash-052316.smt2 b/test/regress/regress0/fmf/sc-crash-052316.smt2 new file mode 100644 index 000000000..2fc86cbed --- /dev/null +++ b/test/regress/regress0/fmf/sc-crash-052316.smt2 @@ -0,0 +1,35 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat + (set-logic ALL_SUPPORTED) + (set-info :status unsat) + (declare-sort g_ 0) + (declare-fun __nun_card_witness_0_ () g_) + (declare-sort f_ 0) + (declare-fun __nun_card_witness_1_ () f_) + (declare-sort e_ 0) + (declare-fun __nun_card_witness_2_ () e_) +(declare-datatypes () + ((prod1_ (Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_))))) + (declare-sort d_ 0) + (declare-fun __nun_card_witness_3_ () d_) + (declare-sort c_ 0) + (declare-fun __nun_card_witness_4_ () c_) + (declare-sort b_ 0) + (declare-fun __nun_card_witness_5_ () b_) + (declare-sort a_ 0) + (declare-fun __nun_card_witness_6_ () a_) +(declare-datatypes () + ((prod_ (Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_))))) + (declare-fun f1_ (prod_ c_ d_ prod1_) g_) + (declare-fun g1_ (prod_) c_) + (declare-fun h_ (prod_ d_) prod1_) + (declare-fun nun_sk_0_ () prod_) +(declare-fun nun_sk_1_ (c_) d_) + (assert + (not + (exists ((v/72 c_)) + (exists ((x/73 prod1_)) + (= (f1_ nun_sk_0_ v/72 (nun_sk_1_ v/72) x/73) + (f1_ nun_sk_0_ (g1_ nun_sk_0_) (nun_sk_1_ v/72) + (h_ nun_sk_0_ (nun_sk_1_ v/72)))))))) +(check-sat) -- 2.30.2