summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/datatype.cpp78
-rw-r--r--src/expr/datatype.h46
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp2
-rw-r--r--src/theory/quantifiers/first_order_model.cpp1
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--test/regress/regress0/fmf/Makefile.am4
-rwxr-xr-xtest/regress/regress0/fmf/forall_unit_data.smt223
-rwxr-xr-xtest/regress/regress0/fmf/forall_unit_data2.smt28
-rwxr-xr-xtest/regress/regress0/fmf/sc_bad_model_1221.smt233
9 files changed, 155 insertions, 42 deletions
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<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAtt
typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
+typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
+typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> 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<std::string, DatatypeType>& resolutions,
const std::vector<Type>& 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<Type>& 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<cond.getNumChildren(); j++) {
TypeNode tn = vars[j].getType();
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5ccb794f7..36b24c51b 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1029,7 +1029,7 @@ Node TermDb::getEnumerateTerm( TypeNode tn, unsigned index ) {
bool TermDb::isClosedEnumerableType( TypeNode tn ) {
std::map< TypeNode, bool >::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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback