struct DatatypeConsIndexTag {};
struct DatatypeFiniteTag {};
struct DatatypeFiniteComputedTag {};
+ struct DatatypeUFiniteTag {};
+ struct DatatypeUFiniteComputedTag {};
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
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);
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;
}
}
}
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);
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 ){
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,
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");
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");
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);
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
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),
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 */
* 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 );
* Datatype must be resolved.
*/
Expr getTester() const;
-
+
/** get sygus op */
Expr getSygusOp() const;
/** get sygus let body */
unsigned getNumSygusLetInputArgs() const;
/** is this a sygus identity function */
bool isSygusIdFunc() const;
-
+
/**
* Get the tester name for this Datatype constructor.
*/
* 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
* then we will pose additional requirements for sharing.
*/
bool involvesExternalType() const;
+ bool involvesUninterpretedType() const;
};/* class DatatypeConstructor */
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,
* 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();
/** is this a co-datatype? */
inline bool isCodatatype() const;
-
+
/** is this a sygus datatype? */
inline bool isSygus() const;
* 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
*/
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
* This Datatype must be resolved.
*/
Expr getConstructor(std::string name) const;
-
+
/** get sygus type */
Type getSygusType() const;
/** get sygus var list */
* then we will pose additional requirements for sharing.
*/
bool involvesExternalType() const;
+ bool involvesUninterpretedType() const;
};/* class Datatype */
d_resolved(false),
d_self(),
d_involvesExt(false),
+ d_involvesUt(false),
d_card(CardinalityUnknown()),
d_card_rec_singleton(0),
d_well_founded(0) {
d_resolved(false),
d_self(),
d_involvesExt(false),
+ d_involvesUt(false),
d_card(CardinalityUnknown()),
d_card_rec_singleton(0),
d_well_founded(0) {
if( consIndex==-1 ){
consIndex = j;
}
- if( !dt[ j ].isFinite() ) {
+ if( !dt[ j ].isFinite() && ( !options::finiteModelFind() || !dt.involvesUninterpretedType() ) ) {
if( !eqc || !eqc->d_selectors ){
needSplit = false;
}
}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();
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;
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)
-; cvc4 --lang smt\r
-\r
-; This problem returns "unsat", but it is in fact "sat", by interpreting "a" with a domain of\r
-; cardinality 1. The issue arises irrespective of the "--finite-model-find" option.\r
-\r
-(set-option :produce-models true)\r
-(set-option :interactive-mode true)\r
-(set-logic ALL_SUPPORTED)\r
-(declare-sort a 0)\r
-(declare-datatypes () ((w (Wrap (unw a)))))\r
-(declare-fun x () w)\r
-(assert (forall ((y w)) (= x y)))\r
-(check-sat)\r
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff