From: ajreynol Date: Tue, 22 Dec 2015 12:44:05 +0000 (+0100) Subject: Always split on constructor types for datatypes involving uninterpreted sorts when... X-Git-Tag: cvc5-1.0.0~6133 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75003d97ad485f8840310e652a74872f5950538d;p=cvc5.git Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions. --- diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 09fe2cdc3..4ebc5071f 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -39,6 +39,8 @@ namespace expr { struct DatatypeConsIndexTag {}; struct DatatypeFiniteTag {}; struct DatatypeFiniteComputedTag {}; + struct DatatypeUFiniteTag {}; + struct DatatypeUFiniteComputedTag {}; }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ @@ -46,6 +48,8 @@ typedef expr::Attribute DatatypeIndexAtt typedef expr::Attribute DatatypeConsIndexAttr; typedef expr::Attribute DatatypeFiniteAttr; typedef expr::Attribute DatatypeFiniteComputedAttr; +typedef expr::Attribute DatatypeUFiniteAttr; +typedef expr::Attribute DatatypeUFiniteComputedAttr; const Datatype& Datatype::datatypeOf(Expr item) { ExprManagerScope ems(item); @@ -120,10 +124,13 @@ void Datatype::resolve(ExprManager* em, d_self = self; d_involvesExt = false; + d_involvesUt = false; for(const_iterator i = begin(); i != end(); ++i) { if( (*i).involvesExternalType() ){ d_involvesExt = true; - break; + } + if( (*i).involvesUninterpretedType() ){ + d_involvesUt = true; } } } @@ -245,18 +252,13 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, bool Datatype::isFinite() const throw(IllegalArgumentException) { CheckArgument(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); - TypeNode self = TypeNode::fromType(d_self); - // is this already in the cache ? if(self.getAttribute(DatatypeFiniteComputedAttr())) { return self.getAttribute(DatatypeFiniteAttr()); } - - Cardinality c = 0; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { if(! (*i).isFinite()) { self.setAttribute(DatatypeFiniteComputedAttr(), true); @@ -269,6 +271,27 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { return true; } +bool Datatype::isUFinite() const throw(IllegalArgumentException) { + CheckArgument(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); + TypeNode self = TypeNode::fromType(d_self); + // is this already in the cache ? + if(self.getAttribute(DatatypeUFiniteComputedAttr())) { + return self.getAttribute(DatatypeUFiniteAttr()); + } + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! (*i).isUFinite()) { + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), false); + return false; + } + } + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), true); + return true; +} + bool Datatype::isWellFounded() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( d_well_founded==0 ){ @@ -505,6 +528,10 @@ bool Datatype::involvesExternalType() const{ return d_involvesExt; } +bool Datatype::involvesUninterpretedType() const{ + return d_involvesUt; +} + void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::map& resolutions, const std::vector& placeholders, @@ -722,7 +749,7 @@ unsigned DatatypeConstructor::getNumSygusLetArgs() const { Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_args[i]; -} +} unsigned DatatypeConstructor::getNumSygusLetInputArgs() const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); @@ -733,7 +760,7 @@ bool DatatypeConstructor::isSygusIdFunc() const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body; } - + Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); @@ -777,17 +804,13 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { CheckArgument(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); - TNode self = Node::fromExpr(d_constructor); - // is this already in the cache ? if(self.getAttribute(DatatypeFiniteComputedAttr())) { return self.getAttribute(DatatypeFiniteAttr()); } - for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) { self.setAttribute(DatatypeFiniteComputedAttr(), true); @@ -795,11 +818,31 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return false; } } - self.setAttribute(DatatypeFiniteComputedAttr(), true); self.setAttribute(DatatypeFiniteAttr(), true); return true; } +bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { + CheckArgument(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); + TNode self = Node::fromExpr(d_constructor); + // is this already in the cache ? + if(self.getAttribute(DatatypeUFiniteComputedAttr())) { + return self.getAttribute(DatatypeUFiniteAttr()); + } + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type t = SelectorType((*i).getSelector().getType()).getRangeType(); + if(!t.isSort() && !t.getCardinality().isFinite()) { + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), false); + return false; + } + } + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), true); + return true; +} Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) { // we're using some internals, so we have to set up this library context @@ -882,6 +925,15 @@ bool DatatypeConstructor::involvesExternalType() const{ return false; } +bool DatatypeConstructor::involvesUninterpretedType() const{ + for(const_iterator i = begin(); i != end(); ++i) { + if(SelectorType((*i).getSelector().getType()).getRangeType().isSort()) { + return true; + } + } + return false; +} + DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) : d_name(name), d_selector(selector), diff --git a/src/expr/datatype.h b/src/expr/datatype.h index c1ec475e5..1ea9fd6be 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -213,7 +213,7 @@ private: Type doParametricSubstitution(Type range, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements); - + /** compute the cardinality of this datatype */ Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute whether this datatype is well-founded */ @@ -236,7 +236,7 @@ public: * constructor and tester aren't created until resolution time. */ DatatypeConstructor(std::string name, std::string tester); - + /** set sygus */ void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); @@ -284,7 +284,7 @@ public: * Datatype must be resolved. */ Expr getTester() const; - + /** get sygus op */ Expr getSygusOp() const; /** get sygus let body */ @@ -297,7 +297,7 @@ public: unsigned getNumSygusLetInputArgs() const; /** is this a sygus identity function */ bool isSygusIdFunc() const; - + /** * Get the tester name for this Datatype constructor. */ @@ -334,6 +334,13 @@ public: * only be called for resolved constructors. */ bool isFinite() const throw(IllegalArgumentException); + /** + * Return true iff this constructor is finite (it is nullary or + * each of its argument types are finite) under assumption + * uninterpreted sorts are finite. This function can + * only be called for resolved constructors. + */ + bool isUFinite() const throw(IllegalArgumentException); /** * Returns true iff this Datatype constructor has already been @@ -373,6 +380,7 @@ public: * then we will pose additional requirements for sharing. */ bool involvesExternalType() const; + bool involvesUninterpretedType() const; };/* class DatatypeConstructor */ @@ -469,16 +477,17 @@ private: bool d_resolved; Type d_self; bool d_involvesExt; + bool d_involvesUt; /** information for sygus */ Type d_sygus_type; - Expr d_sygus_bvl; + Expr d_sygus_bvl; bool d_sygus_allow_const; bool d_sygus_allow_all; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache mutable Cardinality d_card; - + // is this type a recursive singleton type mutable int d_card_rec_singleton; // if d_card_rec_singleton is true, @@ -555,7 +564,7 @@ public: * allow_const : whether all constants are (implicitly) included in the grammar */ void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); - + /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -576,7 +585,7 @@ public: /** is this a co-datatype? */ inline bool isCodatatype() const; - + /** is this a sygus datatype? */ inline bool isSygus() const; @@ -594,6 +603,14 @@ public: * Datatype must be resolved or an exception is thrown. */ bool isFinite() const throw(IllegalArgumentException); + /** + * Return true iff this Datatype is finite (all constructors are + * finite, i.e., there are finitely many ground terms) under the + * assumption unintepreted sorts are finite. If the + * datatype is not well-founded, this function returns false. The + * Datatype must be resolved or an exception is thrown. + */ + bool isUFinite() const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground @@ -601,16 +618,16 @@ public: */ bool isWellFounded() const throw(IllegalArgumentException); - /** + /** * Return true iff this datatype is a recursive singleton */ bool isRecursiveSingleton() const throw(IllegalArgumentException); - - + + /** get number of recursive singleton argument types */ unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException); Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException); - + /** * Construct and return a ground term of this Datatype. The * Datatype must be both resolved and well-founded, or else an @@ -678,7 +695,7 @@ public: * This Datatype must be resolved. */ Expr getConstructor(std::string name) const; - + /** get sygus type */ Type getSygusType() const; /** get sygus var list */ @@ -693,6 +710,7 @@ public: * then we will pose additional requirements for sharing. */ bool involvesExternalType() const; + bool involvesUninterpretedType() const; };/* class Datatype */ @@ -743,6 +761,7 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_resolved(false), d_self(), d_involvesExt(false), + d_involvesUt(false), d_card(CardinalityUnknown()), d_card_rec_singleton(0), d_well_founded(0) { @@ -756,6 +775,7 @@ inline Datatype::Datatype(std::string name, const std::vector& params, boo d_resolved(false), d_self(), d_involvesExt(false), + d_involvesUt(false), d_card(CardinalityUnknown()), d_card_rec_singleton(0), d_well_founded(0) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1962d2e31..77733904d 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -244,7 +244,7 @@ void TheoryDatatypes::check(Effort e) { if( consIndex==-1 ){ consIndex = j; } - if( !dt[ j ].isFinite() ) { + if( !dt[ j ].isFinite() && ( !options::finiteModelFind() || !dt.involvesUninterpretedType() ) ) { if( !eqc || !eqc->d_selectors ){ needSplit = false; } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 095e7868e..027a4573b 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -688,6 +688,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { }else{ //make the condition Node cond = d_models[op]->d_cond[i]; + Trace("fmc-model-func") << "...cond : " << cond << std::endl; std::vector< Node > children; for( unsigned j=0; j::iterator it = d_typ_closed_enum.find( tn ); if( it==d_typ_closed_enum.end() ){ - d_typ_closed_enum[tn] = false; + d_typ_closed_enum[tn] = true; bool ret = true; if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){ ret = false; diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index bb85e62b3..bca9f2e4f 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -41,7 +41,9 @@ TESTS = \ fore19-exp2-core.smt2 \ with-ind-104-core.smt2 \ syn002-si-real-int.smt2 \ - krs-sat.smt2 + krs-sat.smt2 \ + forall_unit_data2.smt2 \ + sc_bad_model_1221.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/forall_unit_data.smt2 b/test/regress/regress0/fmf/forall_unit_data.smt2 index 7e0897d14..26ef66522 100755 --- a/test/regress/regress0/fmf/forall_unit_data.smt2 +++ b/test/regress/regress0/fmf/forall_unit_data.smt2 @@ -1,13 +1,10 @@ -; cvc4 --lang smt - -; This problem returns "unsat", but it is in fact "sat", by interpreting "a" with a domain of -; cardinality 1. The issue arises irrespective of the "--finite-model-find" option. - -(set-option :produce-models true) -(set-option :interactive-mode true) -(set-logic ALL_SUPPORTED) -(declare-sort a 0) -(declare-datatypes () ((w (Wrap (unw a))))) -(declare-fun x () w) -(assert (forall ((y w)) (= x y))) -(check-sat) +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-option :produce-models true) +(set-option :interactive-mode true) +(set-logic ALL_SUPPORTED) +(declare-sort a 0) +(declare-datatypes () ((w (Wrap (unw a))))) +(declare-fun x () w) +(assert (forall ((y w)) (= x y))) +(check-sat) diff --git a/test/regress/regress0/fmf/forall_unit_data2.smt2 b/test/regress/regress0/fmf/forall_unit_data2.smt2 new file mode 100755 index 000000000..64847d6d2 --- /dev/null +++ b/test/regress/regress0/fmf/forall_unit_data2.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(declare-sort a 0) +(declare-datatypes () ((prod (Pair (gx a) (gy a))))) +(declare-fun p () prod) +(assert (forall ((x a) (y a)) (not (= p (Pair x y))))) +(check-sat) diff --git a/test/regress/regress0/fmf/sc_bad_model_1221.smt2 b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 new file mode 100755 index 000000000..a083e418d --- /dev/null +++ b/test/regress/regress0/fmf/sc_bad_model_1221.smt2 @@ -0,0 +1,33 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat + (set-logic ALL_SUPPORTED) + (set-info :status sat) + (declare-sort a 0) + (declare-fun __nun_card_witness_0 () a) + (declare-datatypes () ((prod (Pair (_select_Pair_0 a) (_select_Pair_1 a))))) + (declare-sort G_snd 0) + (declare-fun __nun_card_witness_1 () G_snd) + (declare-fun snd (prod) a) + (declare-fun proj_G_snd_0 (G_snd) prod) + (assert + (forall ((a/32 G_snd)) + (and + (= (snd (proj_G_snd_0 a/32)) (_select_Pair_1 (proj_G_snd_0 a/32))) + true))) + (declare-fun p () prod) + (declare-datatypes () ((pd (Pd (_select_Pd_0 prod))))) + (declare-sort G_fs 0) + (declare-fun __nun_card_witness_2 () G_fs) + (declare-fun fs (pd) a) + (declare-fun proj_G_fs_0 (G_fs) pd) + (assert + (forall ((a/33 G_fs)) + (and + (= (fs (proj_G_fs_0 a/33)) + (_select_Pair_0 (_select_Pd_0 (proj_G_fs_0 a/33)))) + true))) + (assert + (and (not (= (fs (Pd p)) (snd p))) + (exists ((a/34 G_fs)) (= (Pd p) (proj_G_fs_0 a/34))) + (exists ((a/35 G_snd)) (= p (proj_G_snd_0 a/35))))) + (check-sat)