smt2_tokens.h
cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g
- $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@
+ $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
smt_tokens.h: @srcdir@/../parser/smt/Smt.g
- $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@
+ $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g
- $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@
+ $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@
clean-local:
rm -f $(BUILT_SOURCES)
/** Index into the head of the facts list */
context::CDO<unsigned> d_factsHead;
+ /**
+ * Whether the last retrieved fact via get() was a shared term fact
+ * or not.
+ */
+ bool d_wasSharedTermFact;
+
protected:
/**
d_context(ctxt),
d_facts(ctxt),
d_factsHead(ctxt, 0),
+ d_wasSharedTermFact(false),
d_out(&out),
d_valuation(valuation) {
}
TNode get() {
Assert( !done(), "Theory::get() called with assertion queue empty!" );
TNode fact = d_facts[d_factsHead];
+ d_wasSharedTermFact = false;
d_factsHead = d_factsHead + 1;
Debug("theory") << "Theory::get() => " << fact
<< "(" << d_facts.size() << " left)" << std::endl;
return fact;
}
+ /**
+ * Returns whether the last fact retrieved by get() was a shared
+ * term fact.
+ *
+ * @return true if the fact just retrieved via get() was a shared
+ * term fact, false if the fact just retrieved was a "normal channel"
+ * fact.
+ */
+ bool isSharedTermFact() const throw() {
+ return d_wasSharedTermFact;
+ }
+
/**
* Provides access to the facts queue, primarily intended for theory
* debugging purposes.
namespace CVC4 {
+const Integer Cardinality::s_unknownCard(0);
const Integer Cardinality::s_intCard(-1);
const Integer Cardinality::s_realCard(-2);
const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0));
const Cardinality Cardinality::REALS(Cardinality::Beth(1));
+const Cardinality Cardinality::UNKNOWN((Cardinality::Unknown()));
Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
+ if(isUnknown()) {
+ return *this;
+ } else if(c.isUnknown()) {
+ d_card = s_unknownCard;
+ return *this;
+ }
+
if(isFinite() && c.isFinite()) {
- d_card += c.d_card;
+ d_card += c.d_card - 1;
return *this;
}
if(*this >= c) {
/** Assigning multiplication of this cardinality with another. */
Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
+ if(isUnknown()) {
+ return *this;
+ } else if(c.isUnknown()) {
+ d_card = s_unknownCard;
+ return *this;
+ }
+
if(*this == 0 || c == 0) {
return *this = 0;
} else if(!isFinite() || !c.isFinite()) {
return *this = c;
}
} else {
- d_card *= c.d_card;
+ d_card -= 1;
+ d_card *= c.d_card - 1;
+ d_card += 1;
return *this;
}
}
/** Assigning exponentiation of this cardinality with another. */
Cardinality& Cardinality::operator^=(const Cardinality& c)
throw(IllegalArgumentException) {
+ if(isUnknown()) {
+ return *this;
+ } else if(c.isUnknown()) {
+ d_card = s_unknownCard;
+ return *this;
+ }
+
if(c == 0) {
// (anything) ^ 0 == 1
- d_card = 1;
+ d_card = 2;// remember +1 for finite cardinalities
return *this;
} else if(*this == 0) {
// 0 ^ (>= 1) == 0
//
// Note: can throw an assertion if c is too big for
// exponentiation
- d_card = d_card.pow(c.d_card.getUnsignedLong());
+ d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
return *this;
} else if(!isFinite() && c.isFinite()) {
// inf ^ finite == inf
}
-std::ostream& operator<<(std::ostream& out,
- Cardinality::Beth b)
- throw() {
+std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) throw() {
out << "beth[" << b.getNumber() << ']';
return out;
}
-std::ostream& operator<<(std::ostream& out, const Cardinality& c)
- throw() {
- if(c.isFinite()) {
+std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() {
+ if(c.isUnknown()) {
+ out << "Cardinality::UNKNOWN";
+ } else if(c.isFinite()) {
out << c.getFiniteCardinality();
} else {
out << Cardinality::Beth(c.getBethNumber());
/** Cardinality of the reals */
static const Integer s_realCard;
+ /** A representation for unknown cardinality */
+ static const Integer s_unknownCard;
+
/**
- * In the case of finite cardinality, this is >= 0, and is equal to
- * the cardinality. If infinite, it is < 0, and is Beth[|card|-1].
+ * In the case of finite cardinality, this is > 0, and is equal to
+ * the cardinality+1. If infinite, it is < 0, and is Beth[|card|-1].
* That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
+ * If this field is 0, the cardinality is unknown.
*/
Integer d_card;
/** The cardinality of the set of real numbers. */
static const Cardinality REALS;
+ /** The unknown cardinality */
+ static const Cardinality UNKNOWN;
+
/**
* Representation for a Beth number, used only to construct
* Cardinality objects.
*/
- class Beth {
+ class CVC4_PUBLIC Beth {
Integer d_index;
public:
}
};/* class Cardinality::Beth */
+ /**
+ * Representation for an unknown cardinality.
+ */
+ class CVC4_PUBLIC Unknown {
+ public:
+ Unknown() throw() {}
+ ~Unknown() throw() {}
+ };/* class Cardinality::Unknown */
+
/**
* Construct a finite cardinality equal to the integer argument.
* The argument must be nonnegative. If we change this to an
Cardinality(long card) : d_card(card) {
CheckArgument(card >= 0, card,
"Cardinality must be a nonnegative integer, not %ld.", card);
+ d_card += 1;
Assert(isFinite());
}
CheckArgument(card >= 0, card,
"Cardinality must be a nonnegative integer, not %s.",
card.toString().c_str());
+ d_card += 1;
Assert(isFinite());
}
Assert(!isFinite());
}
+ /**
+ * Construct an unknown cardinality.
+ */
+ Cardinality(Unknown) : d_card(0) {
+ }
+
+ /** Returns true iff this cardinality is unknown. */
+ bool isUnknown() const throw() {
+ return d_card == 0;
+ }
+
/** Returns true iff this cardinality is finite. */
bool isFinite() const throw() {
- return d_card >= 0;
+ return d_card > 0;
}
/**
* infinite.
*/
bool isCountable() const throw() {
- return d_card >= s_intCard;
+ return isFinite() || d_card == s_intCard;
}
/**
* cardinality. (If this cardinality is infinite, this function
* throws an IllegalArgumentException.)
*/
- const Integer& getFiniteCardinality() const throw(IllegalArgumentException) {
+ Integer getFiniteCardinality() const throw(IllegalArgumentException) {
CheckArgument(isFinite(), *this, "This cardinality is not finite.");
- return d_card;
+ return d_card - 1;
}
/**
* IllegalArgumentException.)
*/
Integer getBethNumber() const throw(IllegalArgumentException) {
- CheckArgument(!isFinite(), *this, "This cardinality is not infinite.");
+ CheckArgument(!isFinite() && !isUnknown(), *this,
+ "This cardinality is not infinite (or is unknown).");
return -d_card - 1;
}
/** Test for equality between cardinalities. */
bool operator==(const Cardinality& c) const throw() {
- return d_card == c.d_card;
+ return !isUnknown() && d_card == c.d_card;
}
/** Test for disequality between cardinalities. */
bool operator!=(const Cardinality& c) const throw() {
- return !(*this == c);
+ return !isUnknown() && !c.isUnknown() && d_card != c.d_card;
}
/** Test whether this cardinality is less than another. */
bool operator<(const Cardinality& c) const throw() {
return
- ( isFinite() && !c.isFinite() ) ||
- ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
- ( !isFinite() && !c.isFinite() && d_card > c.d_card );
+ !isUnknown() && !c.isUnknown() &&
+ ( ( isFinite() && !c.isFinite() ) ||
+ ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
+ ( !isFinite() && !c.isFinite() && d_card > c.d_card ) );
}
/**
* another.
*/
bool operator<=(const Cardinality& c) const throw() {
- return *this < c || *this == c;
+ return !isUnknown() && !c.isUnknown() && (*this < c || *this == c);
}
/** Test whether this cardinality is greater than another. */
bool operator>(const Cardinality& c) const throw() {
- return !(*this <= c);
+ return !isUnknown() && !c.isUnknown() && !(*this <= c);
}
/**
* another.
*/
bool operator>=(const Cardinality& c) const throw() {
- return !(*this < c);
+ return !isUnknown() && !c.isUnknown() && !(*this < c);
}
/**
}
};/* class ThreadLocal<T> */
+template <class T>
+class ThreadLocal<T*> : public ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> {
+ typedef ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> super;
+
+public:
+ ThreadLocal() : super() {}
+ ThreadLocal(T* t) : super(t) {}
+ ThreadLocal(const ThreadLocal<T*>& tl) : super(tl) {}
+
+ ThreadLocal<T*>& operator=(T* t) {
+ return static_cast< ThreadLocal<T*>& >(super::operator=(t));
+ }
+ ThreadLocal<T*>& operator=(const ThreadLocal<T*>& tl) {
+ return static_cast< ThreadLocal<T*>& >(super::operator=(tl));
+ }
+ // special operators for pointers
+ T& operator*() {
+ return *static_cast<T*>(*this);
+ }
+ const T& operator*() const {
+ return *static_cast<const T*>(*this);
+ }
+ T* operator->() {
+ return static_cast<T*>(*this);
+ }
+ const T* operator->() const {
+ return static_cast<const T*>(*this);
+ }
+ T* operator++() {
+ T* p = *this;
+ *this = ++p;
+ return p;
+ }
+ T* operator++(int) {
+ T* p = *this;
+ *this = p + 1;
+ return p;
+ }
+ T* operator--() {
+ T* p = *this;
+ *this = --p;
+ return p;
+ }
+ T* operator--(int) {
+ T* p = *this;
+ *this = p - 1;
+ return p;
+ }
+};/* class ThreadLocal<T*> */
+
}/* CVC4 namespace */
#endif /* @CVC4_TLS_SUPPORTED@ */
-% EXPECT: valid\r
-% EXIT: 20\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : nat ;\r
-x4 : nat ;\r
-x5 : nat ;\r
-x6 : nat ;\r
-x7 : nat ;\r
-x8 : nat ;\r
-x9 : nat ;\r
-x10 : nat ;\r
-x11 : list ;\r
-x12 : list ;\r
-x13 : list ;\r
-x14 : list ;\r
-x15 : list ;\r
-x16 : list ;\r
-x17 : list ;\r
-x18 : list ;\r
-x19 : list ;\r
-x20 : list ;\r
-x21 : tree ;\r
-x22 : tree ;\r
-x23 : tree ;\r
-x24 : tree ;\r
-x25 : tree ;\r
-x26 : tree ;\r
-x27 : tree ;\r
-x28 : tree ;\r
-x29 : tree ;\r
-x30 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT (((x4 = x4)\r
- AND (NOT is_leaf((LET x81 = null IN (IF is_cons(x81) THEN car(x81) ELSE leaf(zero) ENDIF)))))\r
- AND (NOT (x10 = x2))));\r
+% EXPECT: valid
+% EXIT: 20
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : nat ;
+x4 : nat ;
+x5 : nat ;
+x6 : nat ;
+x7 : nat ;
+x8 : nat ;
+x9 : nat ;
+x10 : nat ;
+x11 : list ;
+x12 : list ;
+x13 : list ;
+x14 : list ;
+x15 : list ;
+x16 : list ;
+x17 : list ;
+x18 : list ;
+x19 : list ;
+x20 : list ;
+x21 : tree ;
+x22 : tree ;
+x23 : tree ;
+x24 : tree ;
+x25 : tree ;
+x26 : tree ;
+x27 : tree ;
+x28 : tree ;
+x29 : tree ;
+x30 : tree ;
+
+QUERY
+
+(NOT (((x4 = x4)
+ AND (NOT is_leaf((LET x81 = null IN (IF is_cons(x81) THEN car(x81) ELSE leaf(zero) ENDIF)))))
+ AND (NOT (x10 = x2))));
-% EXPECT: valid\r
-% EXIT: 20\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : list ;\r
-x3 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT ((((((((NOT is_succ((LET x90 = (LET x91 = node(cons(x3,cons((LET x92 = (LET x93 = cons(node(x2),(LET x94 = node((LET x95 = null IN (IF is_cons(x95) THEN cdr(x95) ELSE null ENDIF))) IN (IF is_node(x94) THEN children(x94) ELSE null ENDIF))) IN (IF is_cons(x93) THEN cdr(x93) ELSE null ENDIF)) IN (IF is_cons(x92) THEN car(x92) ELSE leaf(zero) ENDIF)),cons(node(cons(node((LET x96 = node(x2) IN (IF is_node(x96) THEN children(x96) ELSE null ENDIF))),cons((LET x97 = (LET x98 = leaf((LET x99 = node((LET x100 = null IN (IF is_cons(x100) THEN cdr(x100) ELSE null ENDIF))) IN (IF is_leaf(x99) THEN data(x99) ELSE zero ENDIF))) IN (IF is_node(x98) THEN children(x98) ELSE null ENDIF)) IN (IF is_cons(x97) THEN car(x97) ELSE leaf(zero) ENDIF)),(LET x101 = (LET x102 = (LET x103 = node(x2) IN (IF is_node(x103) THEN children(x103) ELSE null ENDIF)) IN (IF is_cons(x102) THEN car(x102) ELSE leaf(zero) ENDIF)) IN (IF is_node(x101) THEN children(x101) ELSE null ENDIF))))),cons(leaf(succ((LET x104 = (LET x105 = (LET x106 = null IN (IF is_cons(x106) THEN car(x106) ELSE leaf(zero) ENDIF)) IN (IF is_leaf(x105) THEN data(x105) ELSE zero ENDIF)) IN (IF is_succ(x104) THEN pred(x104) ELSE zero ENDIF)))),null))))) IN (IF is_leaf(x91) THEN data(x91) ELSE zero ENDIF)) IN (IF is_succ(x90) THEN pred(x90) ELSE zero ENDIF))))\r
- AND (node((LET x87 = cons((LET x88 = null IN (IF is_cons(x88) THEN car(x88) ELSE leaf(zero) ENDIF)),(LET x89 = cons(node(cons(x3,x2)),null) IN (IF is_cons(x89) THEN cdr(x89) ELSE null ENDIF))) IN (IF is_cons(x87) THEN cdr(x87) ELSE null ENDIF))) = (LET x85 = (LET x86 = x3 IN (IF is_node(x86) THEN children(x86) ELSE null ENDIF)) IN (IF is_cons(x85) THEN car(x85) ELSE leaf(zero) ENDIF))))\r
- AND is_null((LET x83 = cons(node(null),(LET x84 = x2 IN (IF is_cons(x84) THEN cdr(x84) ELSE null ENDIF))) IN (IF is_cons(x83) THEN cdr(x83) ELSE null ENDIF))))\r
- AND is_null(cons(leaf((LET x77 = succ((LET x78 = (LET x79 = zero IN (IF is_succ(x79) THEN pred(x79) ELSE zero ENDIF)) IN (IF is_succ(x78) THEN pred(x78) ELSE zero ENDIF))) IN (IF is_succ(x77) THEN pred(x77) ELSE zero ENDIF))),(LET x80 = leaf((LET x81 = succ((LET x82 = x3 IN (IF is_leaf(x82) THEN data(x82) ELSE zero ENDIF))) IN (IF is_succ(x81) THEN pred(x81) ELSE zero ENDIF))) IN (IF is_node(x80) THEN children(x80) ELSE null ENDIF)))))\r
- AND is_node(leaf(zero)))\r
- AND (NOT (x2 = null)))\r
- AND (NOT is_zero((LET x76 = node(cons(leaf(succ(zero)),null)) IN (IF is_leaf(x76) THEN data(x76) ELSE zero ENDIF)))))\r
- AND is_null((LET x74 = (LET x75 = null IN (IF is_cons(x75) THEN cdr(x75) ELSE null ENDIF)) IN (IF is_cons(x74) THEN cdr(x74) ELSE null ENDIF)))));\r
+% EXPECT: valid
+% EXIT: 20
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : list ;
+x3 : tree ;
+
+QUERY
+
+(NOT ((((((((NOT is_succ((LET x90 = (LET x91 = node(cons(x3,cons((LET x92 = (LET x93 = cons(node(x2),(LET x94 = node((LET x95 = null IN (IF is_cons(x95) THEN cdr(x95) ELSE null ENDIF))) IN (IF is_node(x94) THEN children(x94) ELSE null ENDIF))) IN (IF is_cons(x93) THEN cdr(x93) ELSE null ENDIF)) IN (IF is_cons(x92) THEN car(x92) ELSE leaf(zero) ENDIF)),cons(node(cons(node((LET x96 = node(x2) IN (IF is_node(x96) THEN children(x96) ELSE null ENDIF))),cons((LET x97 = (LET x98 = leaf((LET x99 = node((LET x100 = null IN (IF is_cons(x100) THEN cdr(x100) ELSE null ENDIF))) IN (IF is_leaf(x99) THEN data(x99) ELSE zero ENDIF))) IN (IF is_node(x98) THEN children(x98) ELSE null ENDIF)) IN (IF is_cons(x97) THEN car(x97) ELSE leaf(zero) ENDIF)),(LET x101 = (LET x102 = (LET x103 = node(x2) IN (IF is_node(x103) THEN children(x103) ELSE null ENDIF)) IN (IF is_cons(x102) THEN car(x102) ELSE leaf(zero) ENDIF)) IN (IF is_node(x101) THEN children(x101) ELSE null ENDIF))))),cons(leaf(succ((LET x104 = (LET x105 = (LET x106 = null IN (IF is_cons(x106) THEN car(x106) ELSE leaf(zero) ENDIF)) IN (IF is_leaf(x105) THEN data(x105) ELSE zero ENDIF)) IN (IF is_succ(x104) THEN pred(x104) ELSE zero ENDIF)))),null))))) IN (IF is_leaf(x91) THEN data(x91) ELSE zero ENDIF)) IN (IF is_succ(x90) THEN pred(x90) ELSE zero ENDIF))))
+ AND (node((LET x87 = cons((LET x88 = null IN (IF is_cons(x88) THEN car(x88) ELSE leaf(zero) ENDIF)),(LET x89 = cons(node(cons(x3,x2)),null) IN (IF is_cons(x89) THEN cdr(x89) ELSE null ENDIF))) IN (IF is_cons(x87) THEN cdr(x87) ELSE null ENDIF))) = (LET x85 = (LET x86 = x3 IN (IF is_node(x86) THEN children(x86) ELSE null ENDIF)) IN (IF is_cons(x85) THEN car(x85) ELSE leaf(zero) ENDIF))))
+ AND is_null((LET x83 = cons(node(null),(LET x84 = x2 IN (IF is_cons(x84) THEN cdr(x84) ELSE null ENDIF))) IN (IF is_cons(x83) THEN cdr(x83) ELSE null ENDIF))))
+ AND is_null(cons(leaf((LET x77 = succ((LET x78 = (LET x79 = zero IN (IF is_succ(x79) THEN pred(x79) ELSE zero ENDIF)) IN (IF is_succ(x78) THEN pred(x78) ELSE zero ENDIF))) IN (IF is_succ(x77) THEN pred(x77) ELSE zero ENDIF))),(LET x80 = leaf((LET x81 = succ((LET x82 = x3 IN (IF is_leaf(x82) THEN data(x82) ELSE zero ENDIF))) IN (IF is_succ(x81) THEN pred(x81) ELSE zero ENDIF))) IN (IF is_node(x80) THEN children(x80) ELSE null ENDIF)))))
+ AND is_node(leaf(zero)))
+ AND (NOT (x2 = null)))
+ AND (NOT is_zero((LET x76 = node(cons(leaf(succ(zero)),null)) IN (IF is_leaf(x76) THEN data(x76) ELSE zero ENDIF)))))
+ AND is_null((LET x74 = (LET x75 = null IN (IF is_cons(x75) THEN cdr(x75) ELSE null ENDIF)) IN (IF is_cons(x74) THEN cdr(x74) ELSE null ENDIF)))));
-% EXPECT: invalid\r
-% EXIT: 10\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : list ;\r
-x4 : list ;\r
-x5 : tree ;\r
-x6 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT ((is_node(x6)\r
- AND (x6 = x5))\r
- AND (NOT (null = cons(x6,x3)))));\r
+% EXPECT: invalid
+% EXIT: 10
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : list ;
+x4 : list ;
+x5 : tree ;
+x6 : tree ;
+
+QUERY
+
+(NOT ((is_node(x6)
+ AND (x6 = x5))
+ AND (NOT (null = cons(x6,x3)))));
-% EXPECT: valid\r
-% EXIT: 20\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : nat ;\r
-x4 : list ;\r
-x5 : list ;\r
-x6 : list ;\r
-x7 : tree ;\r
-x8 : tree ;\r
-x9 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT (((LET x137 = x1 IN (IF is_succ(x137) THEN pred(x137) ELSE zero ENDIF)) = (LET x135 = (LET x136 = null IN (IF is_cons(x136) THEN car(x136) ELSE leaf(zero) ENDIF)) IN (IF is_leaf(x135) THEN data(x135) ELSE zero ENDIF)))\r
- AND (cons(node(x6),(LET x134 = x7 IN (IF is_node(x134) THEN children(x134) ELSE null ENDIF))) = (LET x132 = node((LET x133 = x6 IN (IF is_cons(x133) THEN cdr(x133) ELSE null ENDIF))) IN (IF is_node(x132) THEN children(x132) ELSE null ENDIF)))));\r
+% EXPECT: valid
+% EXIT: 20
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : nat ;
+x4 : list ;
+x5 : list ;
+x6 : list ;
+x7 : tree ;
+x8 : tree ;
+x9 : tree ;
+
+QUERY
+
+(NOT (((LET x137 = x1 IN (IF is_succ(x137) THEN pred(x137) ELSE zero ENDIF)) = (LET x135 = (LET x136 = null IN (IF is_cons(x136) THEN car(x136) ELSE leaf(zero) ENDIF)) IN (IF is_leaf(x135) THEN data(x135) ELSE zero ENDIF)))
+ AND (cons(node(x6),(LET x134 = x7 IN (IF is_node(x134) THEN children(x134) ELSE null ENDIF))) = (LET x132 = node((LET x133 = x6 IN (IF is_cons(x133) THEN cdr(x133) ELSE null ENDIF))) IN (IF is_node(x132) THEN children(x132) ELSE null ENDIF)))));
-% EXPECT: valid\r
-% EXIT: 20\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : nat ;\r
-x4 : nat ;\r
-x5 : nat ;\r
-x6 : list ;\r
-x7 : list ;\r
-x8 : list ;\r
-x9 : list ;\r
-x10 : list ;\r
-x11 : tree ;\r
-x12 : tree ;\r
-x13 : tree ;\r
-x14 : tree ;\r
-x15 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT ((is_cons((LET x121 = leaf((LET x122 = x13 IN (IF is_leaf(x122) THEN data(x122) ELSE zero ENDIF))) IN (IF is_node(x121) THEN children(x121) ELSE null ENDIF)))\r
- AND (x15 = node(x6)))\r
- AND (NOT is_cons(x10))));\r
+% EXPECT: valid
+% EXIT: 20
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : nat ;
+x4 : nat ;
+x5 : nat ;
+x6 : list ;
+x7 : list ;
+x8 : list ;
+x9 : list ;
+x10 : list ;
+x11 : tree ;
+x12 : tree ;
+x13 : tree ;
+x14 : tree ;
+x15 : tree ;
+
+QUERY
+
+(NOT ((is_cons((LET x121 = leaf((LET x122 = x13 IN (IF is_leaf(x122) THEN data(x122) ELSE zero ENDIF))) IN (IF is_node(x121) THEN children(x121) ELSE null ENDIF)))
+ AND (x15 = node(x6)))
+ AND (NOT is_cons(x10))));
-% EXPECT: valid\r
-% EXIT: 20\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : nat ;\r
-x4 : nat ;\r
-x5 : nat ;\r
-x6 : nat ;\r
-x7 : nat ;\r
-x8 : nat ;\r
-x9 : nat ;\r
-x10 : nat ;\r
-x11 : list ;\r
-x12 : list ;\r
-x13 : list ;\r
-x14 : list ;\r
-x15 : list ;\r
-x16 : list ;\r
-x17 : list ;\r
-x18 : list ;\r
-x19 : list ;\r
-x20 : list ;\r
-x21 : tree ;\r
-x22 : tree ;\r
-x23 : tree ;\r
-x24 : tree ;\r
-x25 : tree ;\r
-x26 : tree ;\r
-x27 : tree ;\r
-x28 : tree ;\r
-x29 : tree ;\r
-x30 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT ((((NOT is_zero(x3))\r
- AND (x8 = zero))\r
- AND (NOT (x25 = x28)))\r
- AND (NOT is_zero(x8))));\r
+% EXPECT: valid
+% EXIT: 20
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : nat ;
+x4 : nat ;
+x5 : nat ;
+x6 : nat ;
+x7 : nat ;
+x8 : nat ;
+x9 : nat ;
+x10 : nat ;
+x11 : list ;
+x12 : list ;
+x13 : list ;
+x14 : list ;
+x15 : list ;
+x16 : list ;
+x17 : list ;
+x18 : list ;
+x19 : list ;
+x20 : list ;
+x21 : tree ;
+x22 : tree ;
+x23 : tree ;
+x24 : tree ;
+x25 : tree ;
+x26 : tree ;
+x27 : tree ;
+x28 : tree ;
+x29 : tree ;
+x30 : tree ;
+
+QUERY
+
+(NOT ((((NOT is_zero(x3))
+ AND (x8 = zero))
+ AND (NOT (x25 = x28)))
+ AND (NOT is_zero(x8))));
-% EXPECT: valid\r
-% EXIT: 20\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : list ;\r
-x3 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT ((NOT is_zero(pred(succ(pred(zero)))))\r
- AND (data(x3) = succ(pred(data(leaf(succ(data(car(null))))))))));\r
+% EXPECT: valid
+% EXIT: 20
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : list ;
+x3 : tree ;
+
+QUERY
+
+(NOT ((NOT is_zero(pred(succ(pred(zero)))))
+ AND (data(x3) = succ(pred(data(leaf(succ(data(car(null))))))))));
-% EXPECT: valid\r
-% EXIT: 20\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : list ;\r
-x4 : list ;\r
-x5 : tree ;\r
-x6 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT (((is_leaf(x5)\r
- AND (NOT (x2 = x1)))\r
- AND (x2 = pred(pred(zero))))\r
- AND (NOT is_node(node(null)))));\r
+% EXPECT: valid
+% EXIT: 20
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : list ;
+x4 : list ;
+x5 : tree ;
+x6 : tree ;
+
+QUERY
+
+(NOT (((is_leaf(x5)
+ AND (NOT (x2 = x1)))
+ AND (x2 = pred(pred(zero))))
+ AND (NOT is_node(node(null)))));
-% EXPECT: invalid\r
-% EXIT: 10\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : nat ;\r
-x4 : list ;\r
-x5 : list ;\r
-x6 : list ;\r
-x7 : tree ;\r
-x8 : tree ;\r
-x9 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT ((((((NOT is_succ(pred(data(leaf(x3)))))\r
- AND (x1 = zero))\r
- AND (NOT is_zero(succ(succ(zero)))))\r
- AND (NOT (x3 = x2)))\r
- AND (x4 = cdr(x5)))\r
- AND is_cons(cons(x8,x5))));\r
+% EXPECT: invalid
+% EXIT: 10
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : nat ;
+x4 : list ;
+x5 : list ;
+x6 : list ;
+x7 : tree ;
+x8 : tree ;
+x9 : tree ;
+
+QUERY
+
+(NOT ((((((NOT is_succ(pred(data(leaf(x3)))))
+ AND (x1 = zero))
+ AND (NOT is_zero(succ(succ(zero)))))
+ AND (NOT (x3 = x2)))
+ AND (x4 = cdr(x5)))
+ AND is_cons(cons(x8,x5))));
-% EXPECT: invalid\r
-% EXIT: 10\r
-DATATYPE\r
- nat = succ(pred : nat) | zero,\r
- list = cons(car : tree, cdr : list) | null,\r
- tree = node(children : list) | leaf(data : nat)\r
-END;\r
-\r
-x1 : nat ;\r
-x2 : nat ;\r
-x3 : nat ;\r
-x4 : nat ;\r
-x5 : nat ;\r
-x6 : list ;\r
-x7 : list ;\r
-x8 : list ;\r
-x9 : list ;\r
-x10 : list ;\r
-x11 : tree ;\r
-x12 : tree ;\r
-x13 : tree ;\r
-x14 : tree ;\r
-x15 : tree ;\r
-\r
-QUERY \r
-\r
-(NOT (((NOT (node(x9) = car(x8)))\r
- AND (node(x6) = x11))\r
- AND (NOT is_node(x15))));\r
+% EXPECT: invalid
+% EXIT: 10
+DATATYPE
+ nat = succ(pred : nat) | zero,
+ list = cons(car : tree, cdr : list) | null,
+ tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : nat ;
+x3 : nat ;
+x4 : nat ;
+x5 : nat ;
+x6 : list ;
+x7 : list ;
+x8 : list ;
+x9 : list ;
+x10 : list ;
+x11 : tree ;
+x12 : tree ;
+x13 : tree ;
+x14 : tree ;
+x15 : tree ;
+
+QUERY
+
+(NOT (((NOT (node(x9) = car(x8)))
+ AND (node(x6) = x11))
+ AND (NOT is_node(x15))));
if test -e "$benchmark.expect"; then
expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
- expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,;s,\r,,'`
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
if [ -z "$expected_exit_status" ]; then
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
- expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'`
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
# old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
# this frustrates our auto-language-detection, so add explicit --lang
if test -e "$benchmark.expect"; then
expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'`
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'`
- expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,;s,\r,,'`
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'`
if [ -z "$expected_exit_status" ]; then
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then
expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
- expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'`
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
# old mktemp from coreutils 7.x is broken, can't do XXXX in the middle
# this frustrates our auto-language-detection, so add explicit --lang
error "cannot determine expected output of \`$benchmark': " \
"please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
fi
- expected_output=$(echo "$expected_output" | sed 's,^% EXPECT: ,,;s,\r,,')
- expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'`
+ expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,')
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
if [ -z "$expected_exit_status" ]; then
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
fi
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS );
TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS );
TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS );
+cout << "boolToBool " << boolToBool.getCardinality() << endl;
TS_ASSERT( boolToBool.getCardinality() == 4 );
}
projects / cvc5.git / commitdiff