From 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 13 May 2011 20:42:57 +0000 Subject: [PATCH] * fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio branch) * add Theory::isSharedTermFact() -- it currently always returns false, pending theory combination work * Add "unknown" cardinalities to Cardinality class * Fix run_regression script to handle CRLF line terminators on Macs (where sed is non-GNU) * Convert CRLF line terminators in datatypes regressions to LF --- src/main/Makefile.am | 6 +- src/theory/theory.h | 20 +++++ src/util/cardinality.cpp | 44 ++++++--- src/util/cardinality.h | 63 +++++++++---- src/util/tls.h.in | 50 +++++++++++ .../regress0/datatypes/typed_v10l30054.cvc | 88 +++++++++--------- .../regress0/datatypes/typed_v1l80005.cvc | 44 ++++----- .../regress0/datatypes/typed_v2l30079.cvc | 40 ++++----- .../regress0/datatypes/typed_v3l20092.cvc | 44 ++++----- .../regress0/datatypes/typed_v5l30069.cvc | 58 ++++++------ test/regress/regress0/datatypes/v10l40099.cvc | 90 +++++++++---------- test/regress/regress0/datatypes/v1l20009.cvc | 32 +++---- test/regress/regress0/datatypes/v2l40025.cvc | 42 ++++----- test/regress/regress0/datatypes/v3l60006.cvc | 52 +++++------ test/regress/regress0/datatypes/v5l30058.cvc | 58 ++++++------ test/regress/run_regression | 12 +-- test/unit/expr/type_cardinality_public.h | 3 +- 17 files changed, 436 insertions(+), 310 deletions(-) diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 669ab6fa2..42a306752 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -31,11 +31,11 @@ TOKENS_FILES = \ 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) diff --git a/src/theory/theory.h b/src/theory/theory.h index bba4c623a..e97e603e5 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -86,6 +86,12 @@ private: /** Index into the head of the facts list */ context::CDO d_factsHead; + /** + * Whether the last retrieved fact via get() was a shared term fact + * or not. + */ + bool d_wasSharedTermFact; + protected: /** @@ -96,6 +102,7 @@ protected: d_context(ctxt), d_facts(ctxt), d_factsHead(ctxt, 0), + d_wasSharedTermFact(false), d_out(&out), d_valuation(valuation) { } @@ -131,6 +138,7 @@ protected: 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; @@ -138,6 +146,18 @@ protected: 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. diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index d38be1c92..b8a79cd9e 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -20,15 +20,24 @@ 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) { @@ -40,6 +49,13 @@ Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { /** 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()) { @@ -49,7 +65,9 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() { return *this = c; } } else { - d_card *= c.d_card; + d_card -= 1; + d_card *= c.d_card - 1; + d_card += 1; return *this; } } @@ -57,9 +75,16 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() { /** 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 @@ -75,7 +100,7 @@ Cardinality& Cardinality::operator^=(const Cardinality& c) // // 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 @@ -102,18 +127,17 @@ std::string Cardinality::toString() const throw() { } -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()); diff --git a/src/util/cardinality.h b/src/util/cardinality.h index c520c2735..e7f86c80e 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -42,10 +42,14 @@ class CVC4_PUBLIC Cardinality { /** 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; @@ -57,11 +61,14 @@ public: /** 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: @@ -76,6 +83,15 @@ 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 @@ -85,6 +101,7 @@ public: Cardinality(long card) : d_card(card) { CheckArgument(card >= 0, card, "Cardinality must be a nonnegative integer, not %ld.", card); + d_card += 1; Assert(isFinite()); } @@ -96,6 +113,7 @@ public: CheckArgument(card >= 0, card, "Cardinality must be a nonnegative integer, not %s.", card.toString().c_str()); + d_card += 1; Assert(isFinite()); } @@ -106,9 +124,20 @@ public: 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; } /** @@ -116,7 +145,7 @@ public: * infinite. */ bool isCountable() const throw() { - return d_card >= s_intCard; + return isFinite() || d_card == s_intCard; } /** @@ -124,9 +153,9 @@ public: * 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; } /** @@ -135,7 +164,8 @@ public: * 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; } @@ -174,20 +204,21 @@ public: /** 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 ) ); } /** @@ -195,12 +226,12 @@ public: * 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); } /** @@ -208,7 +239,7 @@ public: * another. */ bool operator>=(const Cardinality& c) const throw() { - return !(*this < c); + return !isUnknown() && !c.isUnknown() && !(*this < c); } /** diff --git a/src/util/tls.h.in b/src/util/tls.h.in index fc0b6932b..bb69e7c82 100644 --- a/src/util/tls.h.in +++ b/src/util/tls.h.in @@ -143,6 +143,56 @@ public: } };/* class ThreadLocal */ +template +class ThreadLocal : public ThreadLocalImpl { + typedef ThreadLocalImpl super; + +public: + ThreadLocal() : super() {} + ThreadLocal(T* t) : super(t) {} + ThreadLocal(const ThreadLocal& tl) : super(tl) {} + + ThreadLocal& operator=(T* t) { + return static_cast< ThreadLocal& >(super::operator=(t)); + } + ThreadLocal& operator=(const ThreadLocal& tl) { + return static_cast< ThreadLocal& >(super::operator=(tl)); + } + // special operators for pointers + T& operator*() { + return *static_cast(*this); + } + const T& operator*() const { + return *static_cast(*this); + } + T* operator->() { + return static_cast(*this); + } + const T* operator->() const { + return static_cast(*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 */ + }/* CVC4 namespace */ #endif /* @CVC4_TLS_SUPPORTED@ */ diff --git a/test/regress/regress0/datatypes/typed_v10l30054.cvc b/test/regress/regress0/datatypes/typed_v10l30054.cvc index 80c148863..3714ece35 100644 --- a/test/regress/regress0/datatypes/typed_v10l30054.cvc +++ b/test/regress/regress0/datatypes/typed_v10l30054.cvc @@ -1,44 +1,44 @@ -% 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 +% 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)))); diff --git a/test/regress/regress0/datatypes/typed_v1l80005.cvc b/test/regress/regress0/datatypes/typed_v1l80005.cvc index 9a85f1b88..c4d69dd05 100644 --- a/test/regress/regress0/datatypes/typed_v1l80005.cvc +++ b/test/regress/regress0/datatypes/typed_v1l80005.cvc @@ -1,22 +1,22 @@ -% 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: 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))))); diff --git a/test/regress/regress0/datatypes/typed_v2l30079.cvc b/test/regress/regress0/datatypes/typed_v2l30079.cvc index 990cfbb24..4a144c9a5 100644 --- a/test/regress/regress0/datatypes/typed_v2l30079.cvc +++ b/test/regress/regress0/datatypes/typed_v2l30079.cvc @@ -1,20 +1,20 @@ -% 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: 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))))); diff --git a/test/regress/regress0/datatypes/typed_v3l20092.cvc b/test/regress/regress0/datatypes/typed_v3l20092.cvc index 43dfa3373..204c2d968 100644 --- a/test/regress/regress0/datatypes/typed_v3l20092.cvc +++ b/test/regress/regress0/datatypes/typed_v3l20092.cvc @@ -1,22 +1,22 @@ -% 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 +% 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))))); diff --git a/test/regress/regress0/datatypes/typed_v5l30069.cvc b/test/regress/regress0/datatypes/typed_v5l30069.cvc index 662391b90..b03b1a88c 100644 --- a/test/regress/regress0/datatypes/typed_v5l30069.cvc +++ b/test/regress/regress0/datatypes/typed_v5l30069.cvc @@ -1,29 +1,29 @@ -% 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 +% 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)))); diff --git a/test/regress/regress0/datatypes/v10l40099.cvc b/test/regress/regress0/datatypes/v10l40099.cvc index f2cc332f3..3471e8428 100644 --- a/test/regress/regress0/datatypes/v10l40099.cvc +++ b/test/regress/regress0/datatypes/v10l40099.cvc @@ -1,45 +1,45 @@ -% 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 +% 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)))); diff --git a/test/regress/regress0/datatypes/v1l20009.cvc b/test/regress/regress0/datatypes/v1l20009.cvc index 9eea247a2..0adba1da7 100644 --- a/test/regress/regress0/datatypes/v1l20009.cvc +++ b/test/regress/regress0/datatypes/v1l20009.cvc @@ -1,16 +1,16 @@ -% 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 +% 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)))))))))); diff --git a/test/regress/regress0/datatypes/v2l40025.cvc b/test/regress/regress0/datatypes/v2l40025.cvc index f78d5b2cf..f3cd83323 100644 --- a/test/regress/regress0/datatypes/v2l40025.cvc +++ b/test/regress/regress0/datatypes/v2l40025.cvc @@ -1,21 +1,21 @@ -% 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: 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))))); diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc index a681599ee..107c3e1a2 100644 --- a/test/regress/regress0/datatypes/v3l60006.cvc +++ b/test/regress/regress0/datatypes/v3l60006.cvc @@ -1,26 +1,26 @@ -% 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 +% 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)))); diff --git a/test/regress/regress0/datatypes/v5l30058.cvc b/test/regress/regress0/datatypes/v5l30058.cvc index 4159f6c70..9691cf5c6 100644 --- a/test/regress/regress0/datatypes/v5l30058.cvc +++ b/test/regress/regress0/datatypes/v5l30058.cvc @@ -1,29 +1,29 @@ -% 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)))); +% 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)))); diff --git a/test/regress/run_regression b/test/regress/run_regression index 8f2e385d7..28bb5cb42 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -49,7 +49,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then 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" @@ -57,7 +57,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then 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 @@ -83,7 +83,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then 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" @@ -91,7 +91,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then 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 @@ -120,8 +120,8 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then 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 diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 381d5fdea..6d6b0740b 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -5,7 +5,7 @@ ** 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 @@ -70,6 +70,7 @@ public: 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 ); } -- 2.30.2