diff options
58 files changed, 4286 insertions, 192 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 7c08293be..bcc96637f 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -2,10 +2,10 @@ /*! \file command.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): dejan ** 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 @@ -498,6 +498,35 @@ void GetOptionCommand::toStream(std::ostream& out) const { out << "GetOption(" << d_flag << ")"; } +/* class DatatypeDeclarationCommand */ + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) : + d_datatypes() { + d_datatypes.push_back(datatype); + Debug("datatypes") << "Create datatype command." << endl; +} + +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) : + d_datatypes(datatypes) { + Debug("datatypes") << "Create datatype command." << endl; +} + +void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) { + Debug("datatypes") << "Invoke datatype command." << endl; + //smtEngine->addDatatypeDefinitions(d_datatype); +} + +void DatatypeDeclarationCommand::toStream(std::ostream& out) const { + out << "DatatypeDeclarationCommand(["; + for(vector<DatatypeType>::const_iterator i = d_datatypes.begin(), + i_end = d_datatypes.end(); + i != i_end; + ++i) { + out << *i << ";" << endl; + } + out << "])"; +} + /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) { diff --git a/src/expr/command.h b/src/expr/command.h index fbb48b6b0..585e60eb4 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -2,10 +2,10 @@ /*! \file command.h ** \verbatim ** Original author: mdeters - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): none + ** Major contributors: dejan + ** Minor contributors (to current version): cconway ** 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 @@ -28,11 +28,13 @@ #include <sstream> #include <string> #include <vector> +#include <map> #include "expr/expr.h" #include "expr/type.h" #include "util/result.h" #include "util/sexpr.h" +#include "util/datatype.h" namespace CVC4 { @@ -264,6 +266,16 @@ public: void printResult(std::ostream& out) const; };/* class GetOptionCommand */ +class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { +private: + std::vector<DatatypeType> d_datatypes; +public: + DatatypeDeclarationCommand(const DatatypeType& datatype); + DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); + void invoke(SmtEngine* smtEngine); + void toStream(std::ostream& out) const; +};/* class DatatypeDeclarationCommand */ + class CVC4_PUBLIC CommandSequence : public Command { private: /** All the commands to be executed (in sequence) */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 6e8b6c63c..21fc0a4a1 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -2,10 +2,10 @@ /*! \file expr_manager_template.cpp ** \verbatim ** Original author: dejan - ** Major contributors: mdeters, cconway + ** Major contributors: cconway, mdeters ** 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 @@ -22,13 +22,15 @@ #include "util/options.h" #include "util/stats.h" +#include <map> + ${includes} // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 32 "${template}" +#line 34 "${template}" #ifdef CVC4_STATISTICS_ON #define INC_STAT(kind) \ @@ -340,6 +342,63 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)))); } +DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) { + NodeManagerScope nms(d_nodeManager); + TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(datatype)); + Type type(d_nodeManager, typeNode); + DatatypeType dtt(type); + const Datatype& dt = typeNode->getConst<Datatype>(); + if(!dt.isResolved()) { + std::map<std::string, DatatypeType> resolutions; + resolutions.insert(std::make_pair(datatype.getName(), dtt)); + const_cast<Datatype&>(dt).resolve(this, resolutions); + } + return dtt; +} + +std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + NodeManagerScope nms(d_nodeManager); + std::map<std::string, DatatypeType> resolutions; + std::vector<DatatypeType> dtts; + for(std::vector<Datatype>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); + i != i_end; + ++i) { + TypeNode* typeNode = new TypeNode(d_nodeManager->mkTypeConst(*i)); + Type type(d_nodeManager, typeNode); + DatatypeType dtt(type); + CheckArgument(resolutions.find((*i).getName()) == resolutions.end(), + datatypes, + "cannot construct two datatypes at the same time with the same name `%s'", + (*i).getName().c_str()); + resolutions.insert(std::make_pair((*i).getName(), dtt)); + dtts.push_back(dtt); + } + for(std::vector<DatatypeType>::iterator i = dtts.begin(), i_end = dtts.end(); + i != i_end; + ++i) { + const Datatype& dt = (*i).getDatatype(); + if(!dt.isResolved()) { + const_cast<Datatype&>(dt).resolve(this, resolutions); + } + } + return dtts; +} + +ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode))); +} + +SelectorType ExprManager::mkSelectorType(Type domain, Type range) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSelectorType(*domain.d_typeNode, *range.d_typeNode))); +} + +TesterType ExprManager::mkTesterType(Type domain) const { + NodeManagerScope nms(d_nodeManager); + return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTesterType(*domain.d_typeNode))); +} + SortType ExprManager::mkSort(const std::string& name) const { NodeManagerScope nms(d_nodeManager); return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index f51d6fa28..415d05878 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking, cconway ** 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 @@ -241,20 +241,40 @@ public: */ TupleType mkTupleType(const std::vector<Type>& types); - /** Make a type representing a bit-vector of the given size */ + /** Make a type representing a bit-vector of the given size. */ BitVectorType mkBitVectorType(unsigned size) const; - /** Make the type of arrays with the given parameterization */ + /** Make the type of arrays with the given parameterization. */ ArrayType mkArrayType(Type indexType, Type constituentType) const; + /** Make a type representing the given datatype. */ + DatatypeType mkDatatypeType(const Datatype& datatype); + + /** + * Make a set of types representing the given datatypes, which may be + * mutually recursive. + */ + std::vector<DatatypeType> mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); + + /** + * Make a type representing a constructor with the given parameterization. + */ + ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const; + + /** Make a type representing a selector with the given parameterization. */ + SelectorType mkSelectorType(Type domain, Type range) const; + + /** Make a type representing a tester with the given parameterization. */ + TesterType mkTesterType(Type domain) const; + /** Make a new sort with the given name. */ SortType mkSort(const std::string& name) const; - /** Make a new sort from a constructor */ + /** Make a new sort from a constructor. */ SortType mkSort(SortConstructorType constructor, const std::vector<TypeNode>& children) const; - /** Make a sort constructor from a name and arity */ + /** Make a sort constructor from a name and arity. */ SortConstructorType mkSortConstructor(const std::string& name, size_t arity) const; diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 1a9722939..489564d5f 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -18,6 +18,13 @@ #include "cvc4_public.h" +// putting the constant-payload #includes up here allows circularity +// (some of them may require a completely-defined Expr type). This +// way, those #includes can forward-declare some stuff to get Expr's +// getConst<> template instantiations correct, and then #include +// "expr.h" safely, then go on to completely declare their own stuff. +${includes} + #ifndef __CVC4__EXPR_H #define __CVC4__EXPR_H @@ -28,13 +35,11 @@ #include "util/exception.h" #include "util/language.h" -${includes} - // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 38 "${template}" +#line 43 "${template}" namespace CVC4 { @@ -576,6 +581,31 @@ public: static inline void setDepth(std::ostream& out, long depth) { out.iword(s_iosIndex) = depth; } + + /** + * Set the expression depth on the output stream for the current + * stack scope. This makes sure the old depth is reset on the stream + * after normal OR exceptional exit from the scope, using the RAII + * C++ idiom. + */ + class Scope { + std::ostream& d_out; + long d_oldDepth; + + public: + + inline Scope(std::ostream& out, long depth) : + d_out(out), + d_oldDepth(ExprSetDepth::getDepth(out)) { + ExprSetDepth::setDepth(out, depth); + } + + inline ~Scope() { + ExprSetDepth::setDepth(d_out, d_oldDepth); + } + + };/* class ExprSetDepth::Scope */ + };/* class ExprSetDepth */ /** @@ -621,6 +651,31 @@ public: static inline void setPrintTypes(std::ostream& out, bool printTypes) { out.iword(s_iosIndex) = printTypes; } + + /** + * Set the print-types state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrintTypes; + + public: + + inline Scope(std::ostream& out, bool printTypes) : + d_out(out), + d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) { + ExprPrintTypes::setPrintTypes(out, printTypes); + } + + inline ~Scope() { + ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes); + } + + };/* class ExprPrintTypes::Scope */ + };/* class ExprPrintTypes */ /** @@ -668,13 +723,38 @@ public: // (offset by one to detect whether default has been set yet) out.iword(s_iosIndex) = int(l) + 1; } + + /** + * Set a language on the output stream for the current stack scope. + * This makes sure the old language is reset on the stream after + * normal OR exceptional exit from the scope, using the RAII C++ + * idiom. + */ + class Scope { + std::ostream& d_out; + OutputLanguage d_oldLanguage; + + public: + + inline Scope(std::ostream& out, OutputLanguage language) : + d_out(out), + d_oldLanguage(ExprSetLanguage::getLanguage(out)) { + ExprSetLanguage::setLanguage(out, language); + } + + inline ~Scope() { + ExprSetLanguage::setLanguage(d_out, d_oldLanguage); + } + + };/* class ExprSetLanguage::Scope */ + };/* class ExprSetLanguage */ }/* CVC4::expr namespace */ ${getConst_instantiations} -#line 676 "${template}" +#line 682 "${template}" namespace expr { diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 40bf9992c..da2847d84 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -138,25 +138,26 @@ function constant { includes="${includes} #include \"$4\"" mkConst_instantiations="${mkConst_instantiations} -template <> -Expr ExprManager::mkConst($2 const& val); +#line $lineno \"$kf\" +template <> Expr ExprManager::mkConst($2 const& val); " mkConst_implementations="${mkConst_implementations} -template <> -Expr ExprManager::mkConst($2 const& val) { +#line $lineno \"$kf\" +template <> Expr ExprManager::mkConst($2 const& val) { +#line $lineno \"$kf\" return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val))); } " getConst_instantiations="${getConst_instantiations} -template <> -$2 const & Expr::getConst< $2 >() const; +#line $lineno \"$kf\" +template <> $2 const & Expr::getConst< $2 >() const; " getConst_implementations="${getConst_implementations} -template <> -$2 const & Expr::getConst() const { - // check even for production builds - CheckArgument(getKind() == ::CVC4::kind::$1, *this, - \"Improper kind for getConst<$2>()\"); +#line $lineno \"$kf\" +template <> $2 const & Expr::getConst() const { +#line $lineno \"$kf\" + CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\"); +#line $lineno \"$kf\" return d_node->getConst< $2 >(); } " diff --git a/src/expr/mkkind b/src/expr/mkkind index 631f73a89..f7f6ba836 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -74,7 +74,7 @@ function theory { theory_id="$1" theory_enum="$1, - ${theory_enum}" + ${theory_enum}" theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; " } diff --git a/src/expr/node.h b/src/expr/node.h index 2509640e0..d3775cb3f 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -813,7 +813,7 @@ namespace CVC4 { // for hash_maps, hash_sets.. struct NodeHashFunction { - size_t operator()(const CVC4::Node& node) const { + size_t operator()(CVC4::Node node) const { return (size_t) node.getId(); } };/* struct NodeHashFunction */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 793b701f8..9449594e3 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -2,10 +2,10 @@ /*! \file node_manager.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: cconway, dejan - ** Minor contributors (to current version): acsys, taking + ** Major contributors: cconway + ** Minor contributors (to current version): acsys, taking, dejan ** 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 @@ -26,6 +26,7 @@ #include "theory/arith/theory_arith_type_rules.h" #include "theory/arrays/theory_arrays_type_rules.h" #include "theory/bv/theory_bv_type_rules.h" +#include "theory/datatypes/theory_datatypes_type_rules.h" #include "util/Assert.h" #include "util/options.h" @@ -434,6 +435,15 @@ TypeNode NodeManager::computeType(TNode n, bool check) case kind::BITVECTOR_SIGN_EXTEND: typeNode = CVC4::theory::bv::BitVectorExtendTypeRule::computeType(this, n, check); break; + case kind::APPLY_CONSTRUCTOR: + typeNode = CVC4::theory::datatypes::DatatypeConstructorTypeRule::computeType(this, n, check); + break; + case kind::APPLY_SELECTOR: + typeNode = CVC4::theory::datatypes::DatatypeSelectorTypeRule::computeType(this, n, check); + break; + case kind::APPLY_TESTER: + typeNode = CVC4::theory::datatypes::DatatypeTesterTypeRule::computeType(this, n, check); + break; default: Debug("getType") << "FAILURE" << std::endl; Unhandled(n.getKind()); @@ -509,4 +519,20 @@ TypeNode NodeManager::getType(TNode n, bool check) return typeNode; } +TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) { + std::vector<TypeNode> sorts; + Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl; + for(Datatype::Constructor::const_iterator i = constructor.begin(); + i != constructor.end(); + ++i) { + Debug("datatypes") << *(*i).getSelector().getType().d_typeNode << std::endl; + TypeNode sort = (*(*i).getSelector().getType().d_typeNode)[1]; + Debug("datatypes") << "ctor sort: " << sort << std::endl; + sorts.push_back(sort); + } + Debug("datatypes") << "ctor range: " << range << std::endl; + sorts.push_back(range); + return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); +} + }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 1760f48c7..7f7d37a52 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, dejan ** Minor contributors (to current version): acsys, taking ** 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 @@ -55,8 +55,8 @@ namespace attr { struct SortArityTag {}; }/* CVC4::expr::attr namespace */ -typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr; -typedef expr::Attribute<attr::SortArityTag, uint64_t> SortArityAttr; +typedef Attribute<attr::VarNameTag, std::string> VarNameAttr; +typedef Attribute<attr::SortArityTag, uint64_t> SortArityAttr; }/* CVC4::expr namespace */ @@ -542,6 +542,15 @@ public: /** Make the type of arrays with the given parameterization */ inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + /** Make a type representing a constructor with the given parameterization */ + TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range); + + /** Make a type representing a selector with the given parameterization */ + inline TypeNode mkSelectorType(TypeNode domain, TypeNode range); + + /** Make a type representing a tester with given parameterization */ + inline TypeNode mkTesterType(TypeNode domain); + /** Make a new (anonymous) sort of arity 0. */ inline TypeNode mkSort(); @@ -796,6 +805,14 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } +inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) { + return mkTypeNode(kind::SELECTOR_TYPE, domain, range); +} + +inline TypeNode NodeManager::mkTesterType(TypeNode domain) { + return mkTypeNode(kind::TESTER_TYPE, domain ); +} + inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); if(find == d_nodeValuePool.end()) { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 78554f61f..6dd9c5cec 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -2,10 +2,10 @@ /*! \file type.cpp ** \verbatim ** Original author: cconway - ** Major contributors: mdeters, dejan + ** Major contributors: dejan, mdeters ** 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 @@ -186,6 +186,58 @@ Type::operator BitVectorType() const throw(AssertionException) { return BitVectorType(*this); } +/** Cast to a Constructor type */ +Type::operator DatatypeType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isDatatype()); + return DatatypeType(*this); +} + +/** Is this the Datatype type? */ +bool Type::isDatatype() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isDatatype(); +} + +/** Cast to a Constructor type */ +Type::operator ConstructorType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isConstructor()); + return ConstructorType(*this); +} + +/** Is this the Constructor type? */ +bool Type::isConstructor() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isConstructor(); +} + +/** Cast to a Selector type */ +Type::operator SelectorType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isSelector()); + return SelectorType(*this); +} + +/** Is this the Selector type? */ +bool Type::isSelector() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isSelector(); +} + +/** Cast to a Tester type */ +Type::operator TesterType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isTester()); + return TesterType(*this); +} + +/** Is this the Tester type? */ +bool Type::isTester() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isTester(); +} + /** Is this a function type? */ bool Type::isFunction() const { NodeManagerScope nms(d_nodeManager); @@ -349,6 +401,26 @@ BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : Assert(isBitVector()); } +DatatypeType::DatatypeType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isDatatype()); +} + +ConstructorType::ConstructorType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isConstructor()); +} + +SelectorType::SelectorType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isSelector()); +} + +TesterType::TesterType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isTester()); +} + FunctionType::FunctionType(const Type& t) throw(AssertionException) : Type(t) { Assert(isFunction()); @@ -392,8 +464,32 @@ Type ArrayType::getConstituentType() const { return makeType(d_typeNode->getArrayConstituentType()); } -size_t TypeHashStrategy::hash(const Type& t) { - return TypeNodeHashStrategy::hash(*t.d_typeNode); +Type ConstructorType::getReturnType() const { + return makeType(d_typeNode->getConstructorReturnType()); +} + +const Datatype& DatatypeType::getDatatype() const { + return d_typeNode->getConst<Datatype>(); +} + +DatatypeType SelectorType::getDomain() const { + return DatatypeType(makeType((*d_typeNode)[0])); +} + +Type SelectorType::getRangeType() const { + return makeType((*d_typeNode)[1]); +} + +DatatypeType TesterType::getDomain() const { + return DatatypeType(makeType((*d_typeNode)[0])); +} + +BooleanType TesterType::getRangeType() const { + return BooleanType(makeType(d_nodeManager->booleanType())); +} + +size_t TypeHashFunction::operator()(const Type& t) { + return TypeNodeHashFunction()(NodeManager::fromType(t)); } }/* CVC4 namespace */ diff --git a/src/expr/type.h b/src/expr/type.h index 130aa3122..3b476ddf5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters, dejan ** 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 @@ -36,6 +36,8 @@ class TypeNode; class SmtEngine; +class Datatype; + template <bool ref_count> class NodeTemplate; @@ -44,6 +46,10 @@ class IntegerType; class RealType; class BitVectorType; class ArrayType; +class DatatypeType; +class ConstructorType; +class SelectorType; +class TesterType; class FunctionType; class TupleType; class KindType; @@ -52,10 +58,10 @@ class SortConstructorType; class Type; /** Strategy for hashing Types */ -struct CVC4_PUBLIC TypeHashStrategy { +struct CVC4_PUBLIC TypeHashFunction { /** Return a hash code for type t */ - static size_t hash(const CVC4::Type& t); -};/* struct TypeHashStrategy */ + size_t operator()(const CVC4::Type& t); +};/* struct TypeHashFunction */ /** * Output operator for types @@ -259,6 +265,54 @@ public: operator ArrayType() const throw(AssertionException); /** + * Is this a datatype type? + * @return true if the type is a datatype type + */ + bool isDatatype() const; + + /** + * Cast this type to a datatype type + * @return the DatatypeType + */ + operator DatatypeType() const throw(AssertionException); + + /** + * Is this a constructor type? + * @return true if the type is a constructor type + */ + bool isConstructor() const; + + /** + * Cast this type to a constructor type + * @return the ConstructorType + */ + operator ConstructorType() const throw(AssertionException); + + /** + * Is this a selector type? + * @return true if the type is a selector type + */ + bool isSelector() const; + + /** + * Cast this type to a selector type + * @return the SelectorType + */ + operator SelectorType() const throw(AssertionException); + + /** + * Is this a tester type? + * @return true if the type is a tester type + */ + bool isTester() const; + + /** + * Cast this type to a tester type + * @return the TesterType + */ + operator TesterType() const throw(AssertionException); + + /** * Is this a sort kind? * @return true if this is a sort kind */ @@ -449,6 +503,78 @@ public: unsigned getSize() const; };/* class BitVectorType */ + +/** + * Class encapsulating the datatype type + */ +class CVC4_PUBLIC DatatypeType : public Type { + +public: + + /** Construct from the base type */ + DatatypeType(const Type& type) throw(AssertionException); + + /** Get the underlying datatype */ + const Datatype& getDatatype() const; + +};/* class DatatypeType */ + + +/** + * Class encapsulating the constructor type + */ +class CVC4_PUBLIC ConstructorType : public Type { + +public: + + /** Construct from the base type */ + ConstructorType(const Type& type) throw(AssertionException); + + /** Get the return type */ + Type getReturnType() const; + +};/* class ConstructorType */ + + +/** + * Class encapsulating the Selector type + */ +class CVC4_PUBLIC SelectorType : public Type { + +public: + + /** Construct from the base type */ + SelectorType(const Type& type) throw(AssertionException); + + /** Get the domain type for this selector (the datatype type) */ + DatatypeType getDomain() const; + + /** Get the range type for this selector (the field type) */ + Type getRangeType() const; + +};/* class SelectorType */ + +/** + * Class encapsulating the Tester type + */ +class CVC4_PUBLIC TesterType : public Type { + +public: + + /** Construct from the base type */ + TesterType(const Type& type) throw(AssertionException); + + /** Get the type that this tester tests (the datatype type) */ + DatatypeType getDomain() const; + + /** + * Get the range type for this tester (included for sake of + * interface completeness), but doesn't give useful information). + */ + BooleanType getRangeType() const; + +};/* class TesterType */ + }/* CVC4 namespace */ #endif /* __CVC4__TYPE_H */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index badc3b72f..7549af895 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking ** 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 @@ -76,28 +76,38 @@ TypeNode TypeNode::getArrayConstituentType() const { return (*this)[1]; } -/** Is this a function type? */ +TypeNode TypeNode::getConstructorReturnType() const { + Assert(isConstructor()); + return (*this)[getNumChildren()-1]; +} + bool TypeNode::isFunction() const { return getKind() == kind::FUNCTION_TYPE; } -/** Is this a predicate type? NOTE: all predicate types are also - function types. */ bool TypeNode::isPredicate() const { return isFunction() && getRangeType().isBoolean(); } -vector<TypeNode> TypeNode::getArgTypes() const { - Assert(isFunction()); +std::vector<TypeNode> TypeNode::getArgTypes() const { vector<TypeNode> args; - for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { - args.push_back((*this)[i]); + if(isTester()) { + Assert(getNumChildren() == 1); + args.push_back((*this)[0]); + } else { + Assert(isFunction() || isConstructor() || isSelector()); + for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { + args.push_back((*this)[i]); + } } return args; } TypeNode TypeNode::getRangeType() const { - Assert(isFunction()); + if(isTester()) { + return NodeManager::currentNM()->booleanType(); + } + Assert(isFunction() || isConstructor() || isSelector()); return (*this)[getNumChildren()-1]; } @@ -137,6 +147,26 @@ bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE; } +/** Is this a datatype type */ +bool TypeNode::isDatatype() const { + return getKind() == kind::DATATYPE_TYPE; +} + +/** Is this a constructor type */ +bool TypeNode::isConstructor() const { + return getKind() == kind::CONSTRUCTOR_TYPE; +} + +/** Is this a selector type */ +bool TypeNode::isSelector() const { + return getKind() == kind::SELECTOR_TYPE; +} + +/** Is this a tester type */ +bool TypeNode::isTester() const { + return getKind() == kind::TESTER_TYPE; +} + /** Is this a bit-vector type of size <code>size</code> */ bool TypeNode::isBitVector(unsigned size) const { return getKind() == kind::BITVECTOR_TYPE && diff --git a/src/expr/type_node.h b/src/expr/type_node.h index ead85cd19..049173867 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking ** 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 @@ -360,18 +360,32 @@ public: /** Get the element type (for array types) */ TypeNode getArrayConstituentType() const; - /** Is this a function type? */ + /** Get the return type (for constructor types) */ + TypeNode getConstructorReturnType() const; + + /** + * Is this a function type? Function-like things (e.g. datatype + * selectors) that aren't actually functions are NOT considered + * functions, here. + */ bool isFunction() const; - /** Get the argument types */ + /** + * Get the argument types of a function, datatype constructor, + * datatype selector, or datatype tester. + */ std::vector<TypeNode> getArgTypes() const; - /** Get the range type (i.e., the type of the result). */ + /** + * Get the range type (i.e., the type of the result) of a function, + * datatype constructor, datatype selector, or datatype tester. + */ TypeNode getRangeType() const; /** * Is this a predicate type? - * NOTE: all predicate types are also function types. + * NOTE: all predicate types are also function types (so datatype + * testers are not considered "predicates" for the purpose of this function). */ bool isPredicate() const; @@ -387,6 +401,18 @@ public: /** Is this a bit-vector type of size <code>size</code> */ bool isBitVector(unsigned size) const; + /** Is this a datatype type */ + bool isDatatype() const; + + /** Is this a constructor type */ + bool isConstructor() const; + + /** Is this a selector type */ + bool isSelector() const; + + /** Is this a tester type */ + bool isTester() const; + /** Get the size of this bit-vector type */ unsigned getBitVectorSize() const; @@ -430,11 +456,11 @@ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { } // for hash_maps, hash_sets.. -struct TypeNodeHashStrategy { - static inline size_t hash(const TypeNode& node) { +struct TypeNodeHashFunction { + size_t operator()(TypeNode node) const { return (size_t) node.getId(); } -};/* struct TypeNodeHashStrategy */ +};/* struct TypeNodeHashFunction */ }/* CVC4 namespace */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 0a05271e2..33e576a32 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2,10 +2,10 @@ /*! \file Cvc.g ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** 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 @@ -37,7 +37,7 @@ options { @lexer::includes { /** This suppresses warnings about the redefinition of token symbols between different - * parsers. The redefinitions should be harmless as long as no client: (a) #include's + * parsers. The redefinitions should be harmless as long as no client: (a) #include's * the lexer headers for two grammars AND (b) uses the token symbol definitions. */ #pragma GCC system_header @@ -56,6 +56,26 @@ options { namespace CVC4 { class Expr; }/* CVC4 namespace */ + +namespace CVC4 { + namespace parser { + namespace cvc { + /** + * This class is just here to get around an unfortunate bit of Antlr. + * We use strings below as return values from rules, which require + * them to be constructible by a uintptr_t. So we derive the string + * class to provide just such a conversion. + */ + class mystring : public std::string { + public: + mystring(const std::string& s) : std::string(s) {} + mystring(uintptr_t) : std::string() {} + mystring() : std::string() {} + };/* class mystring */ + }/* CVC4::parser::cvc namespace */ + }/* CVC4::parser namespace */ +}/* CVC4 namespace */ + } @parser::postinclude { @@ -72,7 +92,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ -#undef PARSER_STATE +#undef PARSER_STATE #define PARSER_STATE ((Parser*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() @@ -109,6 +129,8 @@ command returns [CVC4::Command* cmd = 0] Expr f; SExpr sexpr; std::string s; + Type t; + std::vector<CVC4::Datatype> dts; Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; } : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); } @@ -119,6 +141,13 @@ command returns [CVC4::Command* cmd = 0] { cmd = new SetOptionCommand(AntlrInput::tokenText($STRING_LITERAL), sexpr); } | PUSH_TOK SEMICOLON { cmd = new PushCommand(); } | POP_TOK SEMICOLON { cmd = new PopCommand(); } + // Datatypes can be mututally-recursive if they're in the same + // definition block, separated by a comma. So we parse everything + // and then ask the ExprManager to resolve everything in one go. + | DATATYPE_TOK datatypeDef[dts] + ( COMMA datatypeDef[dts] )* + END_TOK SEMICOLON + { cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } | declaration[cmd] | EOF ; @@ -159,8 +188,8 @@ declType[CVC4::Type& t, std::vector<std::string>& idList] Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* A sort declaration (e.g., "T : TYPE") */ - TYPE_TOK - { PARSER_STATE->mkSorts(idList); + TYPE_TOK + { PARSER_STATE->mkSorts(idList); t = EXPR_MANAGER->kindType(); } | /* A variable declaration */ type[t] { PARSER_STATE->mkVars(idList,t); } @@ -179,7 +208,7 @@ type[CVC4::Type& t] : /* Simple type */ baseType[t] | /* Single-parameter function type */ - baseType[t] ARROW_TOK baseType[t2] + baseType[t] ARROW_TOK baseType[t2] { t = EXPR_MANAGER->mkFunctionType(t,t2); } | /* Multi-parameter function type */ LPAREN baseType[t] @@ -218,34 +247,62 @@ identifier[std::string& id, ; /** - * Matches a type. - * TODO: parse more types + * Matches a type (which MUST be already declared). + * + * @return the type identifier */ baseType[CVC4::Type& t] + : maybeUndefinedBaseType[t,CHECK_DECLARED] + ; + +/** + * Matches a type (which may not be declared yet). Returns the + * identifier. If the type is declared, returns the Type in the 't' + * parameter; otherwise a null Type is returned in 't'. If 'check' is + * CHECK_DECLARED and the type is not declared, an exception is + * thrown. + * + * @return the type identifier + * + * @TODO parse more types + */ +maybeUndefinedBaseType[CVC4::Type& t, + CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id] @init { - std::string id; Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; + AssertArgument(check == CHECK_DECLARED || check == CHECK_NONE, + check, "CVC parser: can't use CHECK_UNDECLARED with maybeUndefinedBaseType[]"); } - : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); } - | INT_TOK { t = EXPR_MANAGER->integerType(); } - | REAL_TOK { t = EXPR_MANAGER->realType(); } - | typeSymbol[t] + : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); id = AntlrInput::tokenText($BOOLEAN_TOK); } + | INT_TOK { t = EXPR_MANAGER->integerType(); id = AntlrInput::tokenText($INT_TOK); } + | REAL_TOK { t = EXPR_MANAGER->realType(); id = AntlrInput::tokenText($REAL_TOK); } + | typeSymbol[t,check] + { id = $typeSymbol.id; } ; /** - * Matches a type identifier + * Matches a type identifier. Returns the identifier. If the type is + * declared, returns the Type in the 't' parameter; otherwise a null + * Type is returned in 't'. If 'check' is CHECK_DECLARED and the type + * is not declared, an exception is thrown. + * + * @return the type identifier */ -typeSymbol[CVC4::Type& t] +typeSymbol[CVC4::Type& t, + CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id] @init { - std::string id; Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : identifier[id,CHECK_DECLARED,SYM_SORT] - { t = PARSER_STATE->getSort(id); } + : identifier[id,check,SYM_SORT] + { bool isNew = (check == CHECK_UNDECLARED || check == CHECK_NONE) && + !PARSER_STATE->isDeclared(id, SYM_SORT); + t = isNew ? Type() : PARSER_STATE->getSort(id); + } ; /** * Matches a CVC4 formula. + * * @return the expression representing the formula */ formula[CVC4::Expr& formula] @@ -311,7 +368,7 @@ iffFormula[CVC4::Expr& f] Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl; } : impliesFormula[f] - ( IFF_TOK + ( IFF_TOK iffFormula[e] { f = MK_EXPR(CVC4::kind::IFF, f, e); } )? @@ -371,7 +428,7 @@ andFormula[CVC4::Expr& f] std::vector<Expr> exprs; Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : notFormula[f] + : notFormula[f] ( AND_TOK { exprs.push_back(f); } notFormula[f] { exprs.push_back(f); } )* { @@ -412,9 +469,9 @@ comparisonFormula[CVC4::Expr& f] ( ( EQUAL_TOK { op = CVC4::kind::EQUAL; negate = false; } | DISEQUAL_TOK { op = CVC4::kind::EQUAL; negate = true; } | GT_TOK { op = CVC4::kind::GT; negate = false; } - | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; } + | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; } | LT_TOK { op = CVC4::kind::LT; negate = false; } - | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; }) + | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; }) plusTerm[e] { f = MK_EXPR(op, f, e); if(negate) { @@ -424,7 +481,7 @@ comparisonFormula[CVC4::Expr& f] )? ; -/** Parses a plus/minus term (left-associative). +/** Parses a plus/minus term (left-associative). TODO: This won't take advantage of n-ary PLUS's. */ plusTerm[CVC4::Expr& f] @init { @@ -435,13 +492,13 @@ plusTerm[CVC4::Expr& f] } : multTerm[f] ( ( PLUS_TOK { op = CVC4::kind::PLUS; } - | MINUS_TOK { op = CVC4::kind::MINUS; } ) + | MINUS_TOK { op = CVC4::kind::MINUS; } ) multTerm[e] { f = MK_EXPR(op, f, e); } )* ; -/** Parses a multiply/divide term (left-associative). +/** Parses a multiply/divide term (left-associative). TODO: This won't take advantage of n-ary MULT's. */ multTerm[CVC4::Expr& f] @init { @@ -451,7 +508,7 @@ multTerm[CVC4::Expr& f] } : expTerm[f] ( ( STAR_TOK { op = CVC4::kind::MULT; } - | DIV_TOK { op = CVC4::kind::DIVISION; } ) + | DIV_TOK { op = CVC4::kind::DIVISION; } ) expTerm[e] { f = MK_EXPR(op, f, e); } )* @@ -494,18 +551,29 @@ unaryTerm[CVC4::Expr& f] std::vector<Expr> args; Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : /* function application */ - // { isFunction(AntlrInput::tokenText(LT(1))) }? + : /* function/constructor application */ functionSymbol[f] { args.push_back( f ); } LPAREN formulaList[args] RPAREN // TODO: check arity - { f = MK_EXPR(CVC4::kind::APPLY_UF, args); } + { Type t = f.getType(); + if( t.isFunction() ) { + f = MK_EXPR(CVC4::kind::APPLY_UF, args); + } else if( t.isConstructor() ) { + Debug("parser-idt") << "apply constructor: " << name.c_str() << " " << args.size() << std::endl; + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); + } else if( t.isSelector() ) { + Debug("parser-idt") << "apply selector: " << name.c_str() << " " << args.size() << std::endl; + f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args); + } else if( t.isTester() ) { + Debug("parser-idt") << "apply tester: " << name.c_str() << " " << args.size() << std::endl; + f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); + } + } | /* if-then-else */ iteTerm[f] - | /* Unary minus */ MINUS_TOK unaryTerm[f] { f = MK_EXPR(CVC4::kind::UMINUS, f); } @@ -517,10 +585,17 @@ unaryTerm[CVC4::Expr& f] | FALSE_TOK { f = MK_CONST(false); } | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } + | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } | /* variable */ identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { f = PARSER_STATE->getVariable(name); } + { f = PARSER_STATE->getVariable(name); + // datatypes: 0-ary constructors + if( PARSER_STATE->getType(name).isConstructor() ){ + args.push_back( f ); + f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args); + } + } ; /** @@ -546,7 +621,7 @@ iteElseTerm[CVC4::Expr& f] std::vector<Expr> args; Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : ELSE_TOK formula[f] + : ELSE_TOK formula[f] | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); } THEN_TOK iteThen = formula[f] { args.push_back(f); } iteElse = iteElseTerm[f] { args.push_back(f); } @@ -564,10 +639,65 @@ functionSymbol[CVC4::Expr& f] std::string name; } : identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { PARSER_STATE->checkFunction(name); + { PARSER_STATE->checkFunctionLike(name); f = PARSER_STATE->getVariable(name); } ; +/** + * Parses a datatype definition + */ +datatypeDef[std::vector<CVC4::Datatype>& datatypes] +@init { + std::string id; +} + : identifier[id,CHECK_UNDECLARED,SYM_SORT] + { datatypes.push_back(Datatype(id)); } + EQUAL_TOK constructorDef[datatypes.back()] + ( BAR_TOK constructorDef[datatypes.back()] )* + ; + +/** + * Parses a constructor defintion for type + */ +constructorDef[CVC4::Datatype& type] +@init { + std::string id; + CVC4::Datatype::Constructor* ctor; +} + : identifier[id,CHECK_UNDECLARED,SYM_SORT] + { + // make the tester + std::string testerId("is_"); + testerId.append(id); + PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); + ctor = new CVC4::Datatype::Constructor(id, testerId); + } + ( LPAREN + selector[*ctor] + ( COMMA selector[*ctor] )* + RPAREN + )? + { // make the constructor + type.addConstructor(*ctor); + Debug("parser-idt") << "constructor: " << id.c_str() << std::endl; + delete ctor; + } + ; + +selector[CVC4::Datatype::Constructor& ctor] +@init { + std::string id; + Type type; +} + : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON maybeUndefinedBaseType[type,CHECK_NONE] + { if(type.isNull()) { + ctor.addArg(id, Datatype::UnresolvedType($maybeUndefinedBaseType.id)); + } else { + ctor.addArg(id, type); + } + Debug("parser-idt") << "selector: " << id.c_str() << std::endl; + } + ; // Keywords @@ -598,6 +728,16 @@ TRUE_TOK : 'TRUE'; TYPE_TOK : 'TYPE'; XOR_TOK : 'XOR'; +DATATYPE_TOK : 'DATATYPE'; +END_TOK : 'END'; +BAR_TOK : '|'; + +ARRAY_TOK : 'ARRAY'; +OF_TOK : 'OF'; +WITH_TOK : 'WITH'; + +BITVECTOR_TOK : 'BITVECTOR'; + // Symbols COLON : ':'; diff --git a/src/parser/input.h b/src/parser/input.h index b9123fc45..71b2faeae 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -2,10 +2,10 @@ /*! \file input.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** 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 @@ -179,7 +179,7 @@ protected: /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; -}; +};/* class Input */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 0ebccf720..c8a9876d5 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -72,8 +72,7 @@ Expr Parser::getFunction(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } -Type -Parser::getType(const std::string& var_name, +Type Parser::getType(const std::string& var_name, SymbolType type) { Assert( isDeclared(var_name, type) ); Type t = getSymbol(var_name, type).getType(); @@ -98,9 +97,15 @@ bool Parser::isBoolean(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); } -/* Returns true if name is bound to a function. */ -bool Parser::isFunction(const std::string& name) { - return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); +/* Returns true if name is bound to a function-like thing (function, + * constructor, tester, or selector). */ +bool Parser::isFunctionLike(const std::string& name) { + if(!isDeclared(name, SYM_VARIABLE)) { + return false; + } + Type type = getType(name); + return type.isFunction() || type.isConstructor() || + type.isTester() || type.isSelector(); } /* Returns true if name is bound to a defined function. */ @@ -200,7 +205,7 @@ Parser::mkSortConstructor(const std::string& name, size_t arity) { return type; } -const std::vector<Type> +std::vector<Type> Parser::mkSorts(const std::vector<std::string>& names) { std::vector<Type> types; for(unsigned i = 0; i < names.size(); ++i) { @@ -209,6 +214,53 @@ Parser::mkSorts(const std::vector<std::string>& names) { return types; } +std::vector<DatatypeType> +Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { + std::vector<DatatypeType> types = + d_exprManager->mkMutualDatatypeTypes(datatypes); + Assert(datatypes.size() == types.size()); + for(unsigned i = 0; i < datatypes.size(); ++i) { + DatatypeType t = types[i]; + const Datatype& dt = t.getDatatype(); + Debug("parser-idt") << "define " << dt.getName() << " as " << t << std::endl; + defineType(dt.getName(), t); + for(Datatype::const_iterator j = dt.begin(), + j_end = dt.end(); + j != j_end; + ++j) { + const Datatype::Constructor& ctor = *j; + Expr::printtypes::Scope pts(Debug("parser-idt"), true); + Expr constructor = ctor.getConstructor(); + Debug("parser-idt") << "+ define " << constructor << std::endl; + string constructorName = constructor.toString(); + if(isDeclared(constructorName, SYM_VARIABLE)) { + throw ParserException(constructorName + " already declared"); + } + defineVar(constructorName, constructor); + Expr tester = ctor.getTester(); + Debug("parser-idt") << "+ define " << tester << std::endl; + string testerName = tester.toString(); + if(isDeclared(testerName, SYM_VARIABLE)) { + throw ParserException(testerName + " already declared"); + } + defineVar(testerName, tester); + for(Datatype::Constructor::const_iterator k = ctor.begin(), + k_end = ctor.end(); + k != k_end; + ++k) { + Expr selector = (*k).getSelector(); + Debug("parser-idt") << "+++ define " << selector << std::endl; + string selectorName = selector.toString(); + if(isDeclared(selectorName, SYM_VARIABLE)) { + throw ParserException(selectorName + " already declared"); + } + defineVar(selectorName, selector); + } + } + } + return types; +} + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: @@ -249,10 +301,10 @@ void Parser::checkDeclaration(const std::string& varName, } } -void Parser::checkFunction(const std::string& name) +void Parser::checkFunctionLike(const std::string& name) throw (ParserException) { - if( d_checksEnabled && !isFunction(name) ) { - parseError("Expecting function symbol, found '" + name + "'"); + if( d_checksEnabled && !isFunctionLike(name) ) { + parseError("Expecting function-like symbol, found '" + name + "'"); } } diff --git a/src/parser/parser.h b/src/parser/parser.h index 15fe5126c..718b862ab 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -263,7 +263,7 @@ public: * @throws ParserException if checks are enabled and name is not * bound to a function */ - void checkFunction(const std::string& name) throw (ParserException); + void checkFunctionLike(const std::string& name) throw (ParserException); /** * Check that <code>kind</code> can accept <code>numArgs</code> arguments. @@ -337,8 +337,13 @@ public: /** * Creates new sorts with the given names (all of arity 0). */ - const std::vector<Type> - mkSorts(const std::vector<std::string>& names); + std::vector<Type> mkSorts(const std::vector<std::string>& names); + + /** + * Create sorts of mutually-recursive datatypes. + */ + std::vector<DatatypeType> + mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes); /** * Add an operator to the current legal set. @@ -357,8 +362,8 @@ public: /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); - /** Is the symbol bound to a function? */ - bool isFunction(const std::string& name); + /** Is the symbol bound to a function (or function-like thing)? */ + bool isFunctionLike(const std::string& name); /** Is the symbol bound to a defined function? */ bool isDefinedFunction(const std::string& name); diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 39d834891..96ac46bf1 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -2,10 +2,10 @@ /*! \file Smt.g ** \verbatim ** Original author: cconway - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters, taking + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): taking ** 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 @@ -365,7 +365,7 @@ functionSymbol[CVC4::Expr& fun] std::string name; } : functionName[name,CHECK_DECLARED] - { PARSER_STATE->checkFunction(name); + { PARSER_STATE->checkFunctionLike(name); fun = PARSER_STATE->getVariable(name); } ; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f34279149..a5a633e48 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2,8 +2,8 @@ /*! \file Smt2.g ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters, taking + ** Major contributors: mdeters + ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -357,7 +357,7 @@ term[CVC4::Expr& expr] | /* A non-built-in function application */ LPAREN_TOK functionName[name,CHECK_DECLARED] - { PARSER_STATE->checkFunction(name); + { PARSER_STATE->checkFunctionLike(name); const bool isDefinedFunction = PARSER_STATE->isDefinedFunction(name); if(isDefinedFunction) { @@ -578,7 +578,7 @@ functionSymbol[CVC4::Expr& fun] std::string name; } : functionName[name,CHECK_DECLARED] - { PARSER_STATE->checkFunction(name); + { PARSER_STATE->checkFunctionLike(name); fun = PARSER_STATE->getVariable(name); } ; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index d2cf3f8b1..a048bc3b2 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -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 @@ -20,6 +20,8 @@ #include "util/language.h" #include <iostream> +#include <algorithm> +#include <iterator> using namespace std; @@ -29,7 +31,157 @@ namespace cvc { void CvcPrinter::toStream(std::ostream& out, TNode n, int toDepth, bool types) const { - n.toStream(out, toDepth, types, language::output::LANG_AST); + // null + if(n.getKind() == kind::NULL_EXPR) { + out << "NULL"; + return; + } + + // variable + if(n.getMetaKind() == kind::metakind::VARIABLE) { + string s; + if(n.getAttribute(expr::VarNameAttr(), s)) { + out << s; + } else { + if(n.getKind() == kind::VARIABLE) { + out << "var_"; + } else { + out << n.getKind() << '_'; + } + out << n.getId(); + } + if(types) { + // print the whole type, but not *its* type + out << ":"; + n.getType().toStream(out, -1, false, language::output::LANG_CVC4); + } + + return; + } + + // constant + if(n.getMetaKind() == kind::metakind::CONSTANT) { + switch(n.getKind()) { + case kind::BITVECTOR_TYPE: + out << "BITVECTOR(" << n.getConst<BitVectorSize>().size << ")"; + break; + case kind::CONST_BITVECTOR: { + const BitVector& bv = n.getConst<BitVector>(); + const Integer& x = bv.getValue(); + out << "0bin"; + unsigned n = bv.getSize(); + while(n-- > 0) { + out << (x.testBit(n) ? '1' : '0'); + } + break; + } + case kind::CONST_BOOLEAN: + // the default would print "1" or "0" for bool, that's not correct + // for our purposes + out << (n.getConst<bool>() ? "TRUE" : "FALSE"); + break; + case kind::CONST_RATIONAL: { + const Rational& rat = n.getConst<Rational>(); + out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; + break; + } + case kind::BUILTIN: + switch(Kind k = n.getConst<Kind>()) { + case kind::EQUAL: out << '='; break; + case kind::PLUS: out << '+'; break; + case kind::MULT: out << '*'; break; + case kind::MINUS: + case kind::UMINUS: out << '-'; break; + case kind::DIVISION: out << '/'; break; + case kind::LT: out << '<'; break; + case kind::LEQ: out << "<="; break; + case kind::GT: out << '>'; break; + case kind::GEQ: out << ">="; break; + case kind::IMPLIES: out << "=>"; break; + case kind::IFF: out << "<=>"; break; + default: + out << k; + } + break; + default: + // fall back on whatever operator<< does on underlying type; we + // might luck out and be SMT-LIB v2 compliant + kind::metakind::NodeValueConstPrinter::toStream(out, n); + } + + return; + } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { + out << n.getOperator(); + if(n.getNumChildren() > 0) { + out << '('; + if(n.getNumChildren() > 1) { + copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", ")); + } + out << n[n.getNumChildren() - 1] << ')'; + } + return; + } else if(n.getMetaKind() == kind::metakind::OPERATOR) { + switch(Kind k = n.getKind()) { + case kind::FUNCTION_TYPE: + case kind::CONSTRUCTOR_TYPE: + case kind::SELECTOR_TYPE: + case kind::TESTER_TYPE: + if(n.getNumChildren() > 0) { + copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " -> ")); + out << n[n.getNumChildren() - 1]; + } + break; + + case kind::ARRAY_TYPE: + out << "ARRAY " << n[0] << " OF " << n[1]; + break; + case kind::SELECT: + out << n[0] << '[' << n[1] << ']'; + break; + case kind::STORE: + out << n[0] << " WITH [" << n[1] << "] = " << n[2]; + break; + + case kind::TUPLE_TYPE: + out << '['; + copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ",")); + out << n[n.getNumChildren() - 1]; + out << ']'; + break; + case kind::TUPLE: + out << "( "; + copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, ", ")); + out << n[n.getNumChildren() - 1]; + out << " )"; + break; + + case kind::ITE: + out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2]; + break; + + default: + if(k == kind::NOT && n[0].getKind() == kind::EQUAL) { + // collapse NOT-over-EQUAL + out << n[0][0] << " /= " << n[0][1]; + } else if(n.getNumChildren() == 2) { + // infix operator + out << n[0] << ' ' << n.getOperator() << ' ' << n[1]; + } else { + // prefix operator + out << n.getOperator() << ' '; + if(n.getNumChildren() > 0) { + if(n.getNumChildren() > 1) { + copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " ")); + } + out << n[n.getNumChildren() - 1]; + } + } + } + return; + } + + Unhandled(); + }/* CvcPrinter::toStream() */ }/* CVC4::printer::cvc namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d821b7f4a..2467db3bb 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking, cconway ** 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 @@ -46,6 +46,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arrays/theory_arrays.h" #include "theory/bv/theory_bv.h" +#include "theory/datatypes/theory_datatypes.h" using namespace std; @@ -98,7 +99,7 @@ class SmtEnginePrivate { public: /** - * Pre-process an Node. This is expected to be highly-variable, + * Pre-process a Node. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple * passes over the Node. */ @@ -141,6 +142,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine->addTheory<theory::arith::TheoryArith>(); d_theoryEngine->addTheory<theory::arrays::TheoryArrays>(); d_theoryEngine->addTheory<theory::bv::TheoryBV>(); + d_theoryEngine->addTheory<theory::datatypes::TheoryDatatypes>(); switch(Options::current()->uf_implementation) { case Options::TIM: d_theoryEngine->addTheory<theory::uf::tim::TheoryUFTim>(); @@ -442,29 +444,40 @@ Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n, Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in) throw(NoSuchFunctionException, AssertionException) { - Node n; - if(!Options::current()->lazyDefinitionExpansion) { - Debug("expand") << "have: " << n << endl; - hash_map<TNode, Node, TNodeHashFunction> cache; - n = expandDefinitions(smt, in, cache); - Debug("expand") << "made: " << n << endl; - } else { - n = in; - } + try { + Node n; + if(!Options::current()->lazyDefinitionExpansion) { + Debug("expand") << "have: " << n << endl; + hash_map<TNode, Node, TNodeHashFunction> cache; + n = expandDefinitions(smt, in, cache); + Debug("expand") << "made: " << n << endl; + } else { + n = in; + } - // For now, don't re-statically-learn from learned facts; this could - // be useful though (e.g., theory T1 could learn something further - // from something learned previously by T2). - NodeBuilder<> learned(kind::AND); - learned << n; - smt.d_theoryEngine->staticLearning(n, learned); - if(learned.getNumChildren() == 1) { - learned.clear(); - } else { - n = learned; - } + // For now, don't re-statically-learn from learned facts; this could + // be useful though (e.g., theory T1 could learn something further + // from something learned previously by T2). + NodeBuilder<> learned(kind::AND); + learned << n; + smt.d_theoryEngine->staticLearning(n, learned); + if(learned.getNumChildren() == 1) { + learned.clear(); + } else { + n = learned; + } - return smt.d_theoryEngine->preprocess(n); + return smt.d_theoryEngine->preprocess(n); + } catch(TypeCheckingExceptionPrivate& tcep) { + // Calls to this function should have already weeded out any + // typechecking exceptions via (e.g.) ensureBoolean(). But a + // theory could still create a new expression that isn't + // well-typed, and we don't want the C++ runtime to abort our + // process without any error notice. + InternalError("A bad expression was produced. " + "Original exception follows:\n%s", + tcep.toString().c_str()); + } } Result SmtEngine::check() { @@ -479,10 +492,21 @@ Result SmtEngine::quickCheck() { void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) throw(NoSuchFunctionException, AssertionException) { - Debug("smt") << "push_back assertion " << n << endl; - smt.d_haveAdditions = true; - Node node = SmtEnginePrivate::preprocess(smt, n); - smt.d_propEngine->assertFormula(node); + try { + Debug("smt") << "push_back assertion " << n << endl; + smt.d_haveAdditions = true; + Node node = SmtEnginePrivate::preprocess(smt, n); + smt.d_propEngine->assertFormula(node); + } catch(TypeCheckingExceptionPrivate& tcep) { + // Calls to this function should have already weeded out any + // typechecking exceptions via (e.g.) ensureBoolean(). But a + // theory could still create a new expression that isn't + // well-typed, and we don't want the C++ runtime to abort our + // process without any error notice. + InternalError("A bad expression was produced. " + "Original exception follows:\n%s", + tcep.toString().c_str()); + } } void SmtEngine::ensureBoolean(const BoolExpr& e) { diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index b72502eca..0d680f4c9 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -3,7 +3,7 @@ AM_CPPFLAGS = \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -SUBDIRS = builtin booleans uf arith arrays bv +SUBDIRS = builtin booleans uf arith arrays bv datatypes noinst_LTLIBRARIES = libtheory.la @@ -36,7 +36,8 @@ libtheory_la_LIBADD = \ @builddir@/uf/libuf.la \ @builddir@/arith/libarith.la \ @builddir@/arrays/libarrays.la \ - @builddir@/bv/libbv.la + @builddir@/bv/libbv.la \ + @builddir@/datatypes/libdatatypes.la EXTRA_DIST = \ rewriter_tables_template.h \ diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index d50397598..716323b8a 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_builtin_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -36,7 +36,7 @@ class TheoryBuiltinRewriter { public: static inline RewriteResponse postRewrite(TNode node) { - if (node.getKind() == kind::EQUAL) { + if(node.getKind() == kind::EQUAL) { return Rewriter::callPostRewrite(Theory::theoryOf(node[0]), node); } return RewriteResponse(REWRITE_DONE, node); diff --git a/src/theory/datatypes/Makefile b/src/theory/datatypes/Makefile new file mode 100644 index 000000000..cb3da4be3 --- /dev/null +++ b/src/theory/datatypes/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/datatypes + +include $(topdir)/Makefile.subdir diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am new file mode 100644 index 000000000..69d83faf4 --- /dev/null +++ b/src/theory/datatypes/Makefile.am @@ -0,0 +1,16 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libdatatypes.la + +libdatatypes_la_SOURCES = \ + theory_datatypes_type_rules.h \ + theory_datatypes.h \ + datatypes_rewriter.h \ + theory_datatypes.cpp \ + union_find.h \ + union_find.cpp + +EXTRA_DIST = kinds diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h new file mode 100644 index 000000000..4fa684c6e --- /dev/null +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -0,0 +1,118 @@ +/********************* */ +/*! \file datatypes_rewriter.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief Rewriter for the theory of inductive datatypes + ** + ** Rewriter for the theory of inductive datatypes. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H +#define __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H + +#include "theory/rewriter.h" +#include "theory/datatypes/theory_datatypes.h" + +namespace CVC4 { +namespace theory { +namespace datatypes { + +class DatatypesRewriter { + +public: + + static RewriteResponse postRewrite(TNode in) { + Debug("datatypes-rewrite") << "post-rewriting " << in << std::endl; + + /* + checkFiniteWellFounded(); + */ + + if(in.getKind() == kind::APPLY_TESTER) { + if(in[0].getKind() == kind::APPLY_CONSTRUCTOR) { + bool result = TheoryDatatypes::checkTrivialTester(in); + Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial tester " << in + << " " << result << std::endl; + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(result)); + } else { + const Datatype& dt = in[0].getType().getConst<Datatype>(); + if(dt.getNumConstructors() == 1) { + // only one constructor, so it must be + Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "only one ctor for " << dt.getName() + << " and that is " << dt[0].getName() + << std::endl; + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(true)); + } + } + } + if(in.getKind() == kind::APPLY_SELECTOR && + in[0].getKind() == kind::APPLY_CONSTRUCTOR) { + // Have to be careful not to rewrite well-typed expressions + // where the selector doesn't match the constructor, + // e.g. "pred(zero)". + TNode selector = in.getOperator(); + TNode constructor = in[0].getOperator(); + Expr selectorExpr = selector.toExpr(); + Expr constructorExpr = constructor.toExpr(); + size_t selectorIndex = Datatype::indexOf(selectorExpr); + size_t constructorIndex = Datatype::indexOf(constructorExpr); + const Datatype& dt = Datatype::datatypeOf(constructorExpr); + const Datatype::Constructor& c = dt[constructorIndex]; + if(c.getNumArgs() > selectorIndex && + c[selectorIndex].getSelector() == selectorExpr) { + Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial selector " << in + << std::endl; + return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); + } else { + Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Would rewrite trivial selector " << in + << " but ctor doesn't match stor" + << std::endl; + } + } + + if(in.getKind() == kind::EQUAL && in[0] == in[1]) { + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(true)); + } + if(in.getKind() == kind::EQUAL && + TheoryDatatypes::checkClashSimple(in[0], in[1])) { + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(false)); + } + + return RewriteResponse(REWRITE_DONE, in); + } + + static RewriteResponse preRewrite(TNode in) { + Debug("datatypes-rewrite") << "pre-rewriting " << in << std::endl; + return RewriteResponse(REWRITE_DONE, in); + } + + static inline void init() {} + static inline void shutdown() {} + +};/* class DatatypesRewriter */ + +}/* CVC4::theory::datatypes namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */ + diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds new file mode 100644 index 000000000..8cac2da62 --- /dev/null +++ b/src/theory/datatypes/kinds @@ -0,0 +1,34 @@ +# kinds -*- sh -*- +# +# For documentation on this file format, please refer to +# src/theory/builtin/kinds. +# + +theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h" + +properties check presolve + +rewriter ::CVC4::theory::datatypes::DatatypesRewriter "theory/datatypes/datatypes_rewriter.h" + +# constructor type has a list of selector types followed by a return type +operator CONSTRUCTOR_TYPE 1: "constructor" + +# selector type has domain type and a range type +operator SELECTOR_TYPE 2 "selector" + +# tester type has a constructor type +operator TESTER_TYPE 1 "tester" + +parameterized APPLY_CONSTRUCTOR CONSTRUCTOR_TYPE 0: "constructor application" + +parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application" + +parameterized APPLY_TESTER TESTER_TYPE 1: "tester application" + +constant DATATYPE_TYPE \ + ::CVC4::Datatype \ + "::CVC4::DatatypeHashStrategy" \ + "util/datatype.h" \ + "datatype type" + +endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp new file mode 100644 index 000000000..f55003178 --- /dev/null +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -0,0 +1,1260 @@ +/********************* */ +/*! \file theory_datatypes.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief Implementation of the theory of datatypes + ** + ** Implementation of the theory of datatypes. + **/ + + +#include "theory/datatypes/theory_datatypes.h" +#include "theory/valuation.h" +#include "expr/kind.h" +#include "util/datatype.h" +#include "util/Assert.h" + +#include <map> + + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::datatypes; + +int TheoryDatatypes::getConstructorIndex( TypeNode t, Node c ) { + map<TypeNode, vector<Node> >::iterator it = d_cons.find( t ); + if( it != d_cons.end() ) { + for( int i = 0; i<(int)it->second.size(); i++ ) { + if( it->second[i] == c ) { + return i; + } + } + } + return -1; +} + +int TheoryDatatypes::getTesterIndex( TypeNode t, Node c ) { + map<TypeNode, vector<Node> >::iterator it = d_testers.find( t ); + if( it != d_testers.end() ) { + for( int i = 0; i<(int)it->second.size(); i++ ) { + if( it->second[i] == c ) { + return i; + } + } + } + return -1; +} + +void TheoryDatatypes::checkFiniteWellFounded() { + if( requiresCheckFiniteWellFounded ) { + Debug("datatypes-finite") << "Check finite, well-founded." << endl; + + //check well-founded and finite, create distinguished ground terms + map<TypeNode, vector<Node> >::iterator it; + vector<Node>::iterator itc; + for( it = d_cons.begin(); it != d_cons.end(); ++it ) { + d_distinguishTerms[it->first] = Node::null(); + d_finite[it->first] = false; + d_wellFounded[it->first] = false; + for( itc = it->second.begin(); itc != it->second.end(); ++itc ) { + d_cons_finite[*itc] = false; + d_cons_wellFounded[*itc] = false; + } + } + bool changed; + do{ + changed = false; + for( it = d_cons.begin(); it != d_cons.end(); ++it ) { + TypeNode t = it->first; + Debug("datatypes-finite") << "check " << t << endl; + bool typeFinite = true; + for( itc = it->second.begin(); itc != it->second.end(); ++itc ) { + Node cn = *itc; + TypeNode ct = cn.getType(); + Debug("datatypes-finite") << " check cons " << ct << endl; + if( !d_cons_finite[cn] ) { + int c; + for( c=0; c<(int)ct.getNumChildren()-1; c++ ) { + Debug("datatypes-finite") << " check sel " << c << " of " << ct << ": " << endl << ct[c] << endl; + TypeNode ts = ct[c]; + Debug("datatypes") << " check : " << ts << endl; + if( !isDatatype( ts ) || !d_finite[ ts ] ) { + break; + } + } + if( c == (int)ct.getNumChildren()-1 ) { + changed = true; + d_cons_finite[cn] = true; + Debug("datatypes-finite") << ct << " is finite" << endl; + } else { + typeFinite = false; + } + } + if( !d_cons_wellFounded[cn] ) { + int c; + for( c=0; c<(int)ct.getNumChildren()-1; c++ ) { + Debug("datatypes") << " check sel " << c << " of " << ct << endl; + Debug("datatypes") << ct[c] << endl; + TypeNode ts = ct[c]; + Debug("datatypes") << " check : " << ts << endl; + if( isDatatype( ts ) && !d_wellFounded[ ts ] ) { + break; + } + } + if( c == (int)ct.getNumChildren()-1 ) { + changed = true; + d_cons_wellFounded[cn] = true; + Debug("datatypes-finite") << ct << " is well founded" << endl; + } + } + if( d_cons_wellFounded[cn] ) { + if( !d_wellFounded[t] ) { + changed = true; + d_wellFounded[t] = true; + // also set distinguished ground term + Debug("datatypes") << "set distinguished ground term out of " << ct << endl; + Debug("datatypes-finite") << t << " is type wf" << endl; + NodeManager* nm = NodeManager::currentNM(); + vector< NodeTemplate<true> > children; + children.push_back( cn ); + for( int c=0; c<(int)ct.getNumChildren()-1; c++ ) { + TypeNode ts = ct[c]; + if( isDatatype( ts ) ) { + children.push_back( d_distinguishTerms[ts] ); + } else { + nm->mkVar( ts ); + } + } + Node dgt = nm->mkNode( APPLY_CONSTRUCTOR, children ); + Debug("datatypes-finite") << "set distinguished ground term " << t << " to " << dgt << endl; + d_distinguishTerms[t] = dgt; + } + } + } + if( typeFinite && !d_finite[t] ) { + changed = true; + d_finite[t] = true; + Debug("datatypes-finite") << t << " now type finite" << endl; + } + } + } while( changed ); + map<TypeNode, bool >::iterator itb; + for( itb=d_finite.begin(); itb != d_finite.end(); ++itb ) { + Debug("datatypes-finite") << itb->first << " is "; + Debug("datatypes-finite") << ( itb->second ? "" : "not ") << "finite." << endl; + } + for( itb=d_wellFounded.begin(); itb != d_wellFounded.end(); ++itb ) { + Debug("datatypes-finite") << itb->first << " is "; + Debug("datatypes-finite") << ( itb->second ? "" : "not ") << "well founded." << endl; + if( !itb->second && isDatatype( itb->first ) ) { + //throw exception? + } + } + requiresCheckFiniteWellFounded = false; + } +} + +TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valuation) : + Theory(THEORY_DATATYPES, c, out, valuation), + d_currAsserts(c), + d_currEqualities(c), + d_drv_map(c), + d_axioms(c), + d_selectors(c), + d_reps(c), + d_selector_eq(c), + d_equivalence_class(c), + d_inst_map(c), + d_labels(c), + d_ccChannel(this), + d_cc(c, &d_ccChannel), + d_unionFind(c), + d_disequalities(c), + d_equalities(c), + d_conflict(), + d_noMerge(false) { + requiresCheckFiniteWellFounded = true; +} + + +TheoryDatatypes::~TheoryDatatypes() { +} + + +void TheoryDatatypes::addDatatypeDefinitions(TypeNode dttn) { + AssertArgument(dttn.getKind() == DATATYPE_TYPE, dttn, "expected a datatype"); + + Debug("datatypes") << "TheoryDatatypes::addDataTypeDefinitions(): " + << dttn.getConst<Datatype>().getName() << endl; + if(d_addedDatatypes.find(dttn) != d_addedDatatypes.end()) { + // already have incorporated this datatype definition + Debug("datatypes") << "+ can skip" << endl; + return; + } + + const Datatype& dt = dttn.getConst<Datatype>(); + Debug("datatypes") << dt << endl; + for(Datatype::const_iterator it = dt.begin(); it != dt.end(); ++it) { + Node constructor = Node::fromExpr((*it).getConstructor()); + d_cons[dttn].push_back(constructor); + d_testers[dttn].push_back(Node::fromExpr((*it).getTester())); + for(Datatype::Constructor::const_iterator itc = (*it).begin(); itc != (*it).end(); ++itc) { + Node selector = Node::fromExpr((*itc).getSelector()); + d_sels[constructor].push_back(selector); + d_sel_cons[selector] = constructor; + } + } + requiresCheckFiniteWellFounded = true; + d_addedDatatypes.insert(dttn); +} + + +void TheoryDatatypes::addSharedTerm(TNode t) { + Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " + << t << endl; +} + + +void TheoryDatatypes::notifyEq(TNode lhs, TNode rhs) { + Debug("datatypes") << "TheoryDatatypes::notifyEq(): " + << lhs << " = " << rhs << endl; + //if(!d_conflict.isNull()) { + // return; + //} + //merge(lhs,rhs); + //FIXME + //Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs); + //addEquality(eq); + //d_drv_map[eq] = d_cc.explain( lhs, rhs ); +} + +void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) { + Debug("datatypes") << "TheoryDatatypes::notifyCongruent(): " + << lhs << " = " << rhs << endl; + if(d_conflict.isNull()) { + merge(lhs,rhs); + } + Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl; +} + + +void TheoryDatatypes::presolve() { + Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; + checkFiniteWellFounded(); +} + +void TheoryDatatypes::check(Effort e) { + for( int i=0; i<(int)d_currAsserts.size(); i++ ) { + Debug("datatypes") << "currAsserts[" << i << "] = " << d_currAsserts[i] << endl; + } + for( int i=0; i<(int)d_currEqualities.size(); i++ ) { + Debug("datatypes") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; + } + for( BoolMap::iterator i = d_inst_map.begin(); i != d_inst_map.end(); i++ ) { + Debug("datatypes") << "inst_map = " << (*i).first << endl; + } + for( EqListsN::iterator i = d_selector_eq.begin(); i != d_selector_eq.end(); i++ ) { + EqListN* m = (*i).second; + Debug("datatypes") << "selector_eq " << (*i).first << ":" << endl; + for( EqListN::const_iterator j = m->begin(); j != m->end(); j++ ) { + Debug("datatypes") << " : " << (*j) << endl; + } + } + while(!done()) { + Node assertion = get(); + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { + cout << "*** TheoryDatatypes::check(): " << assertion << endl; + } + d_currAsserts.push_back( assertion ); + + //clear from the derived map + if( !d_drv_map[assertion].get().isNull() ) { + Debug("datatypes") << "Assertion has already been derived" << endl; + d_drv_map[assertion] = Node::null(); + } else { + collectTerms( assertion ); + switch(assertion.getKind()) { + case kind::EQUAL: + case kind::IFF: + addEquality(assertion); + break; + case kind::APPLY_TESTER: + checkTester( assertion ); + break; + case kind::NOT: + { + switch( assertion[0].getKind()) { + case kind::EQUAL: + case kind::IFF: + { + Node a = assertion[0][0]; + Node b = assertion[0][1]; + addDisequality(assertion[0]); + Debug("datatypes") << "hello." << endl; + d_cc.addTerm(a); + d_cc.addTerm(b); + if(Debug.isOn("datatypes")) { + Debug("datatypes") << " a == > " << a << endl + << " b == > " << b << endl + << " find(a) == > " << debugFind(a) << endl + << " find(b) == > " << debugFind(b) << endl; + } + // There are two ways to get a conflict here. + if(d_conflict.isNull()) { + if(find(a) == find(b)) { + // We get a conflict this way if we WERE previously watching + // a, b and were notified previously (via notifyCongruent()) + // that they were congruent. + NodeBuilder<> nb(kind::AND); + nb << d_cc.explain( assertion[0][0], assertion[0][1] ); + nb << assertion; + d_conflict = nb; + Debug("datatypes") << "Disequality conflict " << d_conflict << endl; + } else { + + // If we get this far, there should be nothing conflicting due + // to this disequality. + Assert(!d_cc.areCongruent(a, b)); + } + } + } + break; + case kind::APPLY_TESTER: + checkTester( assertion ); + break; + default: + Unhandled(assertion[0].getKind()); + break; + } + } + break; + default: + Unhandled(assertion.getKind()); + break; + } + if(!d_conflict.isNull()) { + throwConflict(); + return; + } + } + } + + if( e == FULL_EFFORT ) { + Debug("datatypes-split") << "Check for splits " << e << endl; + //do splitting + for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) { + Node sf = find( (*i).first ); + if( sf == (*i).first || sf.getKind() != APPLY_CONSTRUCTOR ) { + Debug("datatypes-split") << "Check for splitting " << (*i).first << ", "; + EqList* lbl = (sf == (*i).first) ? (*i).second : (*d_labels.find( sf )).second; + if( lbl->empty() ) { + Debug("datatypes-split") << "empty label" << endl; + } else { + Debug("datatypes-split") << "label size = " << lbl->size() << endl; + } + Node cons = getPossibleCons( (*i).first, false ); + if( !cons.isNull() ) { + Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl; + TypeNode typ = (*i).first.getType(); + int cIndex = getConstructorIndex( typ, cons ); + Assert( cIndex != -1 ); + Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, d_testers[typ][cIndex], (*i).first ); + NodeBuilder<> nb(kind::OR); + nb << test << test.notNode(); + Node lemma = nb; + Debug("datatypes-split") << "Lemma is " << lemma << endl; + d_out->lemma( lemma ); + return; + } + } else { + Debug("datatypes-split") << (*i).first << " is " << sf << endl; + } + } + } + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { + cout << "TheoryDatatypes::check(): done" << endl; + } +} + +void TheoryDatatypes::checkTester( Node assertion, bool doAdd ) { + Debug("datatypes") << "Check tester " << assertion << endl; + + Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion; + + //add the term into congruence closure consideration + d_cc.addTerm( tassertion[0] ); + + Node assertionRep = assertion; + Node tassertionRep = tassertion; + Node tRep = tassertion[0]; + //tRep = collapseSelector( tRep, Node::null(), true ); + tRep = find( tRep ); + Debug("datatypes") << "tRep is " << tRep << " " << tassertion[0] << endl; + //add label instead for the representative (if it is different) + if( tRep != tassertion[0] ) { + tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep ); + assertionRep = ( assertion.getKind() == NOT ) ? tassertionRep.notNode() : tassertionRep; + //add explanation + if( doAdd ) { + Node explanation = d_cc.explain( tRep, tassertion[0] ); + NodeBuilder<> nb(kind::AND); + nb << explanation << assertion; + explanation = nb; + Debug("datatypes-drv") << "Check derived tester " << assertionRep << endl; + Debug("datatypes-drv") << " Justification is " << explanation << endl; + d_drv_map[assertionRep] = explanation; + } + } + + //if tRep is a constructor, it is trivial + if( tRep.getKind() == APPLY_CONSTRUCTOR ) { + if( checkTrivialTester( tassertionRep ) == (assertionRep.getKind() == NOT) ) { + d_conflict = doAdd ? assertionRep : NodeManager::currentNM()->mkConst(true); + Debug("datatypes") << "Trivial conflict " << assertionRep << endl; + } + return; + } + + addTermToLabels( tRep ); + EqLists::iterator lbl_i = d_labels.find(tRep); + //Debug("datatypes") << "Found " << (lbl_i == d_labels.end()) << endl; + Assert( lbl_i != d_labels.end() ); + + EqList* lbl = (*lbl_i).second; + //Debug("datatypes") << "Check lbl = " << lbl << ", size = " << lbl->size() << endl; + + //check if empty label (no possible constructors for term) + bool add = true; + int notCount = 0; + if( !lbl->empty() ) { + for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + Node leqn = (*i); + if( leqn.getKind() == kind::NOT ) { + if( leqn[0].getOperator() == tassertionRep.getOperator() ) { + if( assertionRep.getKind() == NOT ) { + add = false; + } else { + NodeBuilder<> nb(kind::AND); + nb << leqn; + if( doAdd ) nb << assertionRep; + d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; + Debug("datatypes") << "Contradictory labels " << d_conflict << endl; + return; + } + break; + } + notCount++; + } else { + if( (leqn.getOperator() == tassertionRep.getOperator()) == (assertionRep.getKind() == NOT) ) { + NodeBuilder<> nb(kind::AND); + nb << leqn; + if( doAdd ) nb << assertionRep; + d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; + Debug("datatypes") << "Contradictory labels(2) " << d_conflict << endl; + return; + } + add = false; + break; + } + } + } + if( add ) { + if( assertionRep.getKind() == NOT && notCount == (int)d_cons[ tRep.getType() ].size()-1 ) { + NodeBuilder<> nb(kind::AND); + if( !lbl->empty() ) { + for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + nb << (*i); + } + } + if( doAdd ) nb << assertionRep; + d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; + Debug("datatypes") << "Exhausted possibilities for labels " << d_conflict << endl; + return; + } + if( doAdd ) { + lbl->push_back( assertionRep ); + Debug("datatypes") << "Add to labels " << lbl->size() << endl; + } + } + if( doAdd ) { + checkInstantiate( tRep ); + if( !d_conflict.isNull() ) { + return; + } + //inspect selectors + updateSelectors( tRep ); + } + return; +} + +bool TheoryDatatypes::checkTrivialTester(Node assertion) { + AssertArgument(assertion.getKind() == APPLY_TESTER && + assertion[0].getKind() == APPLY_CONSTRUCTOR, + assertion, "argument must be a tester-over-constructor"); + TNode tester = assertion.getOperator(); + TNode ctor = assertion[0].getOperator(); + // if they have the same index (and the node has passed + // typechecking) then this is a trivial tester + return Datatype::indexOf(tester.toExpr()) == Datatype::indexOf(ctor.toExpr()); +} + +void TheoryDatatypes::checkInstantiate( Node t ) { + Debug("datatypes") << "TheoryDatatypes::checkInstantiate() " << t << endl; + Assert( t == find( t ) ); + + //if labels were created for t, and t has not been instantiated + if( t.getKind() != APPLY_CONSTRUCTOR ) { + //for each term in equivalance class + initializeEqClass( t ); + EqListN* eqc = (*d_equivalence_class.find( t )).second; + for( EqListN::const_iterator iter = eqc->begin(); iter != eqc->end(); iter++ ) { + Node te = *iter; + Assert( find( te ) == t ); + if( d_inst_map.find( te ) == d_inst_map.end() ) { + Node cons = getPossibleCons( te, true ); + EqLists::iterator lbl_i = d_labels.find( t ); + //there is one remaining constructor + if( !cons.isNull() && lbl_i != d_labels.end() ) { + EqList* lbl = (*lbl_i).second; + //only one constructor possible for term (label is singleton), apply instantiation rule + bool consFinite = d_cons_finite[cons]; + //find if selectors have been applied to t + vector< Node > selectorVals; + selectorVals.push_back( cons ); + NodeBuilder<> justifyEq(kind::AND); + bool foundSel = false; + for( int i=0; i<(int)d_sels[cons].size(); i++ ) { + Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, d_sels[cons][i], te ); + Debug("datatypes") << "Selector[" << i << "] = " << s << endl; + if( d_selectors.find( s ) != d_selectors.end() ) { + Node sf = find( s ); + if( sf != s && sf.getKind() != SKOLEM ) { + justifyEq << d_cc.explain( sf, s ); + } + foundSel = true; + s = sf; + } + selectorVals.push_back( s ); + } + if( consFinite || foundSel ) { + d_inst_map[ te ] = true; + //instantiate, add equality + Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals ); + if( find( val ) != find( te ) ) { + Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te ); + Debug("datatypes") << "Instantiate Equal: " << newEq << "." << endl; + if( lbl->size() == 1 || (*lbl)[ lbl->size()-1 ].getKind() != NOT ) { + justifyEq << (*lbl)[ lbl->size()-1 ]; + } else { + if( !lbl->empty() ) { + for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + justifyEq << (*i); + } + } + } + Node jeq; + if( justifyEq.getNumChildren() == 1 ) { + jeq = justifyEq.getChild( 0 ); + } else { + jeq = justifyEq; + } + Debug("datatypes-split") << "Instantiate " << newEq << endl; + addDerivedEquality( newEq, jeq ); + return; + } + } else { + Debug("datatypes") << "infinite constructor, no selectors " << cons << endl; + } + } + } + } + } +} + +//checkInst = true is for checkInstantiate, checkInst = false is for splitting +Node TheoryDatatypes::getPossibleCons( Node t, bool checkInst ) { + Node tf = find( t ); + EqLists::iterator lbl_i = d_labels.find( tf ); + if( lbl_i != d_labels.end() ) { + EqList* lbl = (*lbl_i).second; + TypeNode typ = t.getType(); + + //if ended by one positive tester + if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) { + if( checkInst ) { + Assert( getTesterIndex( typ, (*lbl)[ lbl->size()-1 ].getOperator() ) != -1 ); + return d_cons[typ][ getTesterIndex( typ, (*lbl)[ lbl->size()-1 ].getOperator() ) ]; + } + //if (n-1) negative testers + } else if( !checkInst || (int)lbl->size() == (int)d_cons[ t.getType() ].size()-1 ) { + vector< bool > possibleCons; + possibleCons.resize( (int)d_cons[ t.getType() ].size(), true ); + if( !lbl->empty() ) { + for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + TNode leqn = (*i); + Assert( getTesterIndex( typ, leqn[0].getOperator() ) != -1 ); + possibleCons[ getTesterIndex( typ, leqn[0].getOperator() ) ] = false; + } + } + Node cons = Node::null(); + for( int i=0; i<(int)possibleCons.size(); i++ ) { + if( possibleCons[i] ) { + cons = d_cons[typ][ i ]; + if( !checkInst ) { + //if there is a selector, split + for( int i=0; i<(int)d_sels[cons].size(); i++ ) { + Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, d_sels[cons][i], tf ); + if( d_selectors.find( s ) != d_selectors.end() ) { + Debug("datatypes") << " getPosCons: found selector " << s << endl; + return cons; + } + } + } + } + } + if( !checkInst ) { + for( int i=0; i<(int)possibleCons.size(); i++ ) { + if( possibleCons[i] && !d_cons_finite[ d_cons[typ][ i ] ] ) { + Debug("datatypes") << "Did not find selector for " << tf; + Debug("datatypes") << " and " << d_cons[typ][ i ] << " is not finite." << endl; + return Node::null(); + } + } + } else { + Assert( !cons.isNull() ); + } + return cons; + } + } + return Node::null(); +} + +Node TheoryDatatypes::getValue(TNode n) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + + case kind::VARIABLE: + Unhandled(kind::VARIABLE); + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); + + default: + Unhandled(n.getKind()); + } +} + +void TheoryDatatypes::merge(TNode a, TNode b) { + if( d_noMerge ) { + Debug("datatypes") << "Append to merge pending list " << d_merge_pending.size() << endl; + d_merge_pending[d_merge_pending.size()-1].push_back( pair< Node, Node >( a, b ) ); + return; + } + Assert(d_conflict.isNull()); + Debug("datatypes") << "Merge "<< a << " " << b << endl; + + // make "a" the one with shorter diseqList + EqLists::iterator deq_ia = d_disequalities.find(a); + EqLists::iterator deq_ib = d_disequalities.find(b); + + if(deq_ia != d_disequalities.end()) { + if(deq_ib == d_disequalities.end() || + (*deq_ia).second->size() > (*deq_ib).second->size()) { + TNode tmp = a; + a = b; + b = tmp; + } + } + + a = find(a); + b = find(b); + + //Debug("datatypes") << "After find: "<< a << " " << b << endl; + + if( a == b) { + return; + } + //if b is a selector, swap a and b + if( b.getKind() == APPLY_SELECTOR && a.getKind() != APPLY_SELECTOR ) { + TNode tmp = a; + a = b; + b = tmp; + } + //make constructors the representatives + if( a.getKind() == APPLY_CONSTRUCTOR ) { + TNode tmp = a; + a = b; + b = tmp; + } + //make sure skolem variable is not representative + if( b.getKind() == SKOLEM ) { + TNode tmp = a; + a = b; + b = tmp; + } + + + NodeBuilder<> explanation(kind::AND); + if( checkClash( a, b, explanation ) ) { + explanation << d_cc.explain( a, b ); + d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; + Debug("datatypes") << "Clash " << a << " " << b << endl; + Debug("datatypes") << "Conflict is " << d_conflict << endl; + return; + } + Debug("datatypes-debug") << "Done clash" << endl; + + Debug("datatypes") << "Set canon: "<< a << " " << b << endl; + + // b becomes the canon of a + d_unionFind.setCanon(a, b); + d_reps[a] = false; + d_reps[b] = true; + //merge equivalence classes + initializeEqClass( a ); + initializeEqClass( b ); + EqListN* eqc_a = (*d_equivalence_class.find( a )).second; + EqListN* eqc_b = (*d_equivalence_class.find( b )).second; + for( EqListN::const_iterator i = eqc_a->begin(); i != eqc_a->end(); i++ ) { + eqc_b->push_back( *i ); + } + + //Debug("datatypes") << "After check 1" << endl; + + deq_ia = d_disequalities.find(a); + map<TNode, TNode> alreadyDiseqs; + if(deq_ia != d_disequalities.end()) { + /* + * Collecting the disequalities of b, no need to check for conflicts + * since the representative of b does not change and we check all the things + * in a's class when we look at the diseq list of find(a) + */ + + EqLists::iterator deq_ib = d_disequalities.find(b); + if(deq_ib != d_disequalities.end()) { + EqList* deq = (*deq_ib).second; + for(EqList::const_iterator j = deq->begin(); j != deq->end(); j++) { + TNode deqn = *j; + TNode s = deqn[0]; + TNode t = deqn[1]; + TNode sp = find(s); + TNode tp = find(t); + Assert(sp == b || tp == b, "test1"); + if(sp == b) { + alreadyDiseqs[tp] = deqn; + } else { + alreadyDiseqs[sp] = deqn; + } + } + } + + /* + * Looking for conflicts in the a disequality list. Note + * that at this point a and b are already merged. Also has + * the side effect that it adds them to the list of b (which + * became the canonical representative) + */ + + EqList* deqa = (*deq_ia).second; + for(EqList::const_iterator i = deqa->begin(); i != deqa->end(); i++) { + TNode deqn = (*i); + Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF); + TNode s = deqn[0]; + TNode t = deqn[1]; + + TNode sp = find(s); + TNode tp = find(t); + if(sp == tp) { + Debug("datatypes") << "Construct standard conflict " << deqn << " " << sp << endl; + Node explanation = d_cc.explain(deqn[0], deqn[1]); + d_conflict = NodeManager::currentNM()->mkNode( kind::AND, explanation, deqn.notNode() ); + Debug("datatypes") << "Conflict is " << d_conflict << endl; + return; + } + Assert( sp == b || tp == b, "test2"); + + // make sure not to add duplicates + + if(sp == b) { + if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { + appendToDiseqList(b, deqn); + alreadyDiseqs[tp] = deqn; + } + } else { + if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { + appendToDiseqList(b, deqn); + alreadyDiseqs[sp] = deqn; + } + } + + } + } + + //Debug("datatypes-debug") << "Done clash" << endl; + checkCycles(); + if( !d_conflict.isNull() ) { + return; + } + Debug("datatypes-debug") << "Done cycles" << endl; + + //merge selector lists + updateSelectors( a ); + Debug("datatypes-debug") << "Done collapse" << endl; + + //merge labels + EqLists::iterator lbl_i = d_labels.find( a ); + if(lbl_i != d_labels.end()) { + EqList* lbl = (*lbl_i).second; + if( !lbl->empty() ) { + for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + checkTester( *i ); + if( !d_conflict.isNull() ) { + return; + } + } + } + } + Debug("datatypes-debug") << "Done merge labels" << endl; + + //do unification + if( d_conflict.isNull() ) { + if( a.getKind() == APPLY_CONSTRUCTOR && b.getKind() == APPLY_CONSTRUCTOR && + a.getOperator() == b.getOperator() ) { + Debug("datatypes") << "Unification: " << a << " and " << b << "." << endl; + for( int i=0; i<(int)a.getNumChildren(); i++ ) { + if( find( a[i] ) != find( b[i] ) ) { + Node newEq = NodeManager::currentNM()->mkNode( EQUAL, a[i], b[i] ); + Node jEq = d_cc.explain(a, b); + Debug("datatypes-drv") << "UEqual: " << newEq << ", justification: " << jEq << " from " << a << " " << b << endl; + Debug("datatypes-drv") << "UEqual find: " << find( a[i] ) << " " << find( b[i] ) << endl; + addDerivedEquality( newEq, jEq ); + } + } + } + } + + Debug("datatypes-debug") << "merge(): Done" << endl; +} + +Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) { + if( t.getKind() == APPLY_SELECTOR ) { + //collapse constructor + TypeNode typ = t[0].getType(); + Node sel = t.getOperator(); + TypeNode selType = sel.getType(); + Node cons = d_sel_cons[sel]; + Node tmp = find( t[0] ); + Node retNode = t; + if( tmp.getKind() == APPLY_CONSTRUCTOR ) { + if( tmp.getOperator() == cons ) { + int selIndex = -1; + for(int i=0; i<(int)d_sels[cons].size(); i++ ) { + if( d_sels[cons][i] == sel ) { + selIndex = i; + break; + } + } + Assert( selIndex != -1 ); + Debug("datatypes") << "Applied selector " << t << " to correct constructor, index = " << selIndex << endl; + Debug("datatypes") << "Return " << tmp[selIndex] << endl; + retNode = tmp[selIndex]; + } else { + Debug("datatypes") << "Applied selector " << t << " to wrong constructor " << endl; + Debug("datatypes") << "Return distinguished term "; + Debug("datatypes") << d_distinguishTerms[ selType[1] ] << " of type " << selType[1] << endl; + retNode = d_distinguishTerms[ selType[1] ]; + } + if( useContext ) { + Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); + d_axioms[neq] = true; + Debug("datatypes-split") << "Collapse selector " << neq << endl; + addEquality( neq ); + } + } else { + if( useContext ) { + int cIndex = getConstructorIndex( typ, cons ); + Assert( cIndex != -1 ); + //check labels + Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, d_testers[typ][cIndex], tmp ); + checkTester( tester, false ); + if( !d_conflict.isNull() ) { + Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl; + retNode = d_distinguishTerms[ selType[1] ]; + + Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t ); + NodeBuilder<> nb(kind::AND); + Node trueNode = NodeManager::currentNM()->mkConst(true); + if( d_conflict != trueNode ) { + nb << d_conflict; + } + d_conflict = Node::null(); + tmp = find( tmp ); + if( tmp != t[0] ) { + nb << d_cc.explain( tmp, t[0] ); + } + Assert( nb.getNumChildren()>0 ); + Node jEq = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb; + Debug("datatypes-drv") << "Collapse selector " << neq << endl; + addDerivedEquality( neq, jEq ); + } + } + } + return retNode; + } + return t; +} + +void TheoryDatatypes::updateSelectors( Node a ) { + EqListsN::iterator sel_a_i = d_selector_eq.find( a ); + if( sel_a_i != d_selector_eq.end() ) { + EqListN* sel_a = (*sel_a_i).second; + Debug("datatypes") << a << " has " << sel_a->size() << " selectors" << endl; + if( !sel_a->empty() ) { + EqListN* sel_b = NULL; + for( EqListN::const_iterator i = sel_a->begin(); i != sel_a->end(); i++ ) { + Node s = (*i); + Node b = find( a ); + if( b != a ) { + EqListsN::iterator sel_b_i = d_selector_eq.find( b ); + if( sel_b_i == d_selector_eq.end() ) { + sel_b = new(getContext()->getCMM()) EqListN(true, getContext(), false, + ContextMemoryAllocator<Node>(getContext()->getCMM())); + d_selector_eq.insertDataFromContextMemory(b, sel_b); + } else { + sel_b = (*sel_b_i).second; + } + a = b; + } + Debug("datatypes") << "Merge selector " << s << " into " << b << endl; + Debug("datatypes") << "Find is " << find( s[0] ) << endl; + Assert( s.getKind() == APPLY_SELECTOR && + find( s[0] ) == b ); + if( b != s[0] ) { + Node t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, s.getOperator(), b ); + //add to labels + addTermToLabels( t ); + merge( s, t ); + s = t; + d_selectors[s] = true; + d_cc.addTerm( s ); + } + s = collapseSelector( s, true ); + if( !d_conflict.isNull() ) { + return; + } + if( sel_b && s.getKind() == APPLY_SELECTOR ) { + sel_b->push_back( s ); + } + } + } + } else { + Debug("datatypes") << a << " has no selectors" << endl; + } +} + +void TheoryDatatypes::collectTerms( TNode t ) { + for( int i=0; i<(int)t.getNumChildren(); i++ ) { + collectTerms( t[i] ); + } + if( t.getKind() == APPLY_SELECTOR ) { + if( d_selectors.find( t ) == d_selectors.end() ) { + Debug("datatypes-split") << " Found selector " << t << endl; + d_selectors[ t ] = true; + d_cc.addTerm( t ); + Node tmp = find( t[0] ); + checkInstantiate( tmp ); + + Node s = t; + if( tmp != t[0] ) { + s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp ); + } + Debug("datatypes-split") << " Before collapse: " << s << endl; + s = collapseSelector( s, true ); + Debug("datatypes-split") << " After collapse: " << s << endl; + if( s.getKind() == APPLY_SELECTOR ) { + //add selector to selector eq list + Debug("datatypes") << " Add selector to list " << tmp << " " << t << endl; + EqListsN::iterator sel_i = d_selector_eq.find( tmp ); + EqListN* sel; + if( sel_i == d_selector_eq.end() ) { + sel = new(getContext()->getCMM()) EqListN(true, getContext(), false, + ContextMemoryAllocator<Node>(getContext()->getCMM())); + d_selector_eq.insertDataFromContextMemory(tmp, sel); + } else { + sel = (*sel_i).second; + } + sel->push_back( s ); + } else { + Debug("datatypes") << " collapsed selector to " << s << endl; + } + } + } + addTermToLabels( t ); +} + +void TheoryDatatypes::addTermToLabels( Node t ) { + if( t.getKind() == APPLY_SELECTOR ) { + + } + if( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) { + Node tmp = find( t ); + if( tmp == t ) { + //add to labels + EqLists::iterator lbl_i = d_labels.find(t); + if(lbl_i == d_labels.end()) { + EqList* lbl = new(getContext()->getCMM()) EqList(true, getContext(), false, + ContextMemoryAllocator<TNode>(getContext()->getCMM())); + d_labels.insertDataFromContextMemory(tmp, lbl); + } + } + } +} + +void TheoryDatatypes::initializeEqClass( Node t ) { + EqListsN::iterator eqc_i = d_equivalence_class.find( t ); + if( eqc_i == d_equivalence_class.end() ) { + EqListN* eqc = new(getContext()->getCMM()) EqListN(true, getContext(), false, + ContextMemoryAllocator<Node>(getContext()->getCMM())); + eqc->push_back( t ); + d_equivalence_class.insertDataFromContextMemory(t, eqc); + } +} + +void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { + Debug("datatypes") << "appending " << eq << endl + << " to diseq list of " << of << endl; + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + Assert(of == debugFind(of)); + EqLists::iterator deq_i = d_disequalities.find(of); + EqList* deq; + if(deq_i == d_disequalities.end()) { + deq = new(getContext()->getCMM()) EqList(true, getContext(), false, + ContextMemoryAllocator<TNode>(getContext()->getCMM())); + d_disequalities.insertDataFromContextMemory(of, deq); + } else { + deq = (*deq_i).second; + } + deq->push_back(eq); + //if(Debug.isOn("uf")) { + // Debug("uf") << " size is now " << deq->size() << endl; + //} +} + +void TheoryDatatypes::appendToEqList(TNode of, TNode eq) { + Debug("datatypes") << "appending " << eq << endl + << " to eq list of " << of << endl; + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + Assert(of == debugFind(of)); + EqLists::iterator eq_i = d_equalities.find(of); + EqList* eql; + if(eq_i == d_equalities.end()) { + eql = new(getContext()->getCMM()) EqList(true, getContext(), false, + ContextMemoryAllocator<TNode>(getContext()->getCMM())); + d_equalities.insertDataFromContextMemory(of, eql); + } else { + eql = (*eq_i).second; + } + eql->push_back(eq); + //if(Debug.isOn("uf")) { + // Debug("uf") << " size is now " << eql->size() << endl; + //} +} + +void TheoryDatatypes::addDerivedEquality(TNode eq, TNode jeq) { + Debug("datatypes-drv") << "Justification for " << eq << "is: " << jeq << "." << endl; + d_drv_map[eq] = jeq; + addEquality( eq ); +} + +void TheoryDatatypes::addEquality(TNode eq) { + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + if( eq[0] != eq[1] ) { + Debug("datatypes") << "Add equality " << eq << "." << endl; + d_merge_pending.push_back( vector< pair< Node, Node > >() ); + bool prevNoMerge = d_noMerge; + d_noMerge = true; + d_cc.addTerm(eq[0]); + d_cc.addTerm(eq[1]); + d_cc.addEquality(eq); + d_currEqualities.push_back(eq); + d_noMerge = prevNoMerge; + unsigned int mpi = d_merge_pending.size()-1; + vector< pair< Node, Node > > mp; + mp.insert( mp.begin(), d_merge_pending[mpi].begin(), d_merge_pending[mpi].end() ); + d_merge_pending.pop_back(); + if( d_conflict.isNull() ) { + merge(eq[0], eq[1]); + } + for( int i=0; i<(int)mp.size(); i++ ) { + if( d_conflict.isNull() ) { + merge( mp[i].first, mp[i].second ); + } + } + } +} + +void TheoryDatatypes::addDisequality(TNode eq) { + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + + TNode a = eq[0]; + TNode b = eq[1]; + + appendToDiseqList(find(a), eq); + appendToDiseqList(find(b), eq); +} + +void TheoryDatatypes::registerEqualityForPropagation(TNode eq) { + // should NOT be in search at this point, this must be called during + // preregistration + + // FIXME with lemmas on demand, this could miss future propagations, + // since we are not necessarily at context level 0, but are updating + // context-sensitive structures. + + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); + + TNode a = eq[0]; + TNode b = eq[1]; + + appendToEqList(find(a), eq); + appendToEqList(find(b), eq); +} + +void TheoryDatatypes::throwConflict() { + Debug("datatypes") << "Convert conflict : " << d_conflict << endl; + NodeBuilder<> nb(kind::AND); + convertDerived( d_conflict, nb ); + if( nb.getNumChildren() == 1 ) { + d_conflict = nb.getChild( 0 ); + } else { + d_conflict = nb; + } + if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) { + cout << "Conflict constructed : " << d_conflict << endl; + } + if( d_conflict.getKind() != kind::AND ) { + NodeBuilder<> nb(kind::AND); + nb << d_conflict << d_conflict; + d_conflict = nb; + } + d_out->conflict( d_conflict, false ); + d_conflict = Node::null(); +} + +void TheoryDatatypes::convertDerived(Node n, NodeBuilder<>& nb) { + if( n.getKind() == kind::AND ) { + for( int i=0; i<(int)n.getNumChildren(); i++ ) { + convertDerived( n[i], nb ); + } + } else if( !d_drv_map[ n ].get().isNull() ) { + //Debug("datatypes") << "Justification for " << n << " is " << d_drv_map[ n ].get() << endl; + convertDerived( d_drv_map[ n ].get(), nb ); + } else if( d_axioms.find( n ) == d_axioms.end() ) { + nb << n; + } +} + +void TheoryDatatypes::checkCycles() { + for( BoolMap::iterator i = d_reps.begin(); i != d_reps.end(); i++ ) { + if( (*i).second ) { + map< Node, bool > visited; + NodeBuilder<> explanation(kind::AND); + if( searchForCycle( (*i).first, (*i).first, visited, explanation ) ) { + Assert( explanation.getNumChildren()>0 ); + d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation; + Debug("datatypes") << "Detected cycle for " << (*i).first << endl; + Debug("datatypes") << "Conflict is " << d_conflict << endl; + return; + } + } + } +} + +//postcondition: if cycle detected, explanation is why n is a subterm of on +bool TheoryDatatypes::searchForCycle( Node n, Node on, + map< Node, bool >& visited, + NodeBuilder<>& explanation ) { + //Debug("datatypes") << "Search for cycle " << n << " " << on << endl; + if( n.getKind() == APPLY_CONSTRUCTOR ) { + for( int i=0; i<(int)n.getNumChildren(); i++ ) { + Node nn = find( n[i] ); + if( visited.find( nn ) == visited.end() ) { + visited[nn] = true; + if( nn == on || searchForCycle( nn, on, visited, explanation ) ) { + if( nn != n[i] ) { + explanation << d_cc.explain( nn, n[i] ); + } + return true; + } + } + } + } + return false; +} + +//should be called initially with explanation of why n1 and n2 are equal +bool TheoryDatatypes::checkClash( Node n1, Node n2, NodeBuilder<>& explanation ) { + //Debug("datatypes") << "Check clash " << n1 << " " << n2 << endl; + Node n1f = find( n1 ); + Node n2f = find( n2 ); + bool retVal = false; + if( n1f != n2f ) { + if( n1f.getKind() == kind::APPLY_CONSTRUCTOR && n2f.getKind() == kind::APPLY_CONSTRUCTOR ) { + if( n1f.getOperator() != n2f.getOperator() ) { + retVal =true; + } else { + Assert( n1f.getNumChildren() == n2f.getNumChildren() ); + for( int i=0; i<(int)n1f.getNumChildren(); i++ ) { + if( checkClash( n1f[i], n2f[i], explanation ) ) { + retVal = true; + break; + } + } + } + } + if( retVal ) { + if( n1f != n1 ) { + explanation << d_cc.explain( n1f, n1 ); + } + if( n2f != n2 ) { + explanation << d_cc.explain( n2f, n2 ); + } + } + } + return retVal; +} + +bool TheoryDatatypes::checkClashSimple( Node n1, Node n2 ) { + if( n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR ) { + if( n1.getOperator() != n2.getOperator() ) { + return true; + } else { + Assert( n1.getNumChildren() == n2.getNumChildren() ); + for( int i=0; i<(int)n1.getNumChildren(); i++ ) { + if( checkClashSimple( n1[i], n2[i] ) ) { + return true; + } + } + } + } + return false; +} diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h new file mode 100644 index 000000000..e3f045e06 --- /dev/null +++ b/src/theory/datatypes/theory_datatypes.h @@ -0,0 +1,218 @@ +/********************* */ +/*! \file theory_datatypes.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief Theory of datatypes. + ** + ** Theory of datatypes. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H +#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H + +#include "theory/theory.h" +#include "util/congruence_closure.h" +#include "util/datatype.h" +#include "theory/datatypes/union_find.h" +#include "util/hash.h" + +#include <ext/hash_set> +#include <iostream> +#include <map> + +namespace CVC4 { +namespace theory { +namespace datatypes { + +class TheoryDatatypes : public Theory { +private: + typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList; + typedef context::CDMap<Node, EqList*, NodeHashFunction> EqLists; + typedef context::CDList<Node, context::ContextMemoryAllocator<Node> > EqListN; + typedef context::CDMap<Node, EqListN*, NodeHashFunction> EqListsN; + typedef context::CDMap< Node, bool, NodeHashFunction > BoolMap; + + std::hash_set<TypeNode, TypeNodeHashFunction> d_addedDatatypes; + + context::CDList<Node> d_currAsserts; + context::CDList<Node> d_currEqualities; + /** a list of types with the list of constructors for that type */ + std::map<TypeNode, std::vector<Node> > d_cons; + /** a list of types with the list of constructors for that type */ + std::map<TypeNode, std::vector<Node> > d_testers; + /** a list of constructors with the list of selectors */ + std::map<Node, std::vector<Node> > d_sels; + /** map from selectors to the constructors they are for */ + std::map<Node, Node > d_sel_cons; + /** the distinguished ground term for each type */ + std::map<TypeNode, Node > d_distinguishTerms; + /** finite datatypes/constructor */ + std::map< TypeNode, bool > d_finite; + std::map< Node, bool > d_cons_finite; + /** well founded datatypes/constructor */ + std::map< TypeNode, bool > d_wellFounded; + std::map< Node, bool > d_cons_wellFounded; + /** whether we need to check finite and well foundedness */ + bool requiresCheckFiniteWellFounded; + /** map from equalties and the equalities they are derived from */ + context::CDMap< Node, Node, NodeHashFunction > d_drv_map; + /** equalities that are axioms */ + BoolMap d_axioms; + /** list of all selectors */ + BoolMap d_selectors; + /** list of all representatives */ + BoolMap d_reps; + /** map from nodes to a list of selectors whose arguments are in the equivalence class of that node */ + EqListsN d_selector_eq; + /** map from node representatives to list of nodes in their eq class */ + EqListsN d_equivalence_class; + /** map from terms to whether they have been instantiated */ + BoolMap d_inst_map; + //Type getType( TypeNode t ); + int getConstructorIndex( TypeNode t, Node c ); + int getTesterIndex( TypeNode t, Node c ); + bool isDatatype( TypeNode t ) { return d_cons.find( t )!=d_cons.end(); } + void checkFiniteWellFounded(); + + /** + * map from terms to testers asserted for that term + * for each t, this is either a list of equations of the form + * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers, + * or a list of equations of the form + * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ) followed by + * is_[constructor_(n+1)]( t ), each of which is a unique tester. + */ + EqLists d_labels; + + class CongruenceChannel { + TheoryDatatypes* d_datatypes; + + public: + CongruenceChannel(TheoryDatatypes* datatypes) : d_datatypes(datatypes) {} + void notifyCongruent(TNode a, TNode b) { + d_datatypes->notifyCongruent(a, b); + } + };/* class CongruenceChannel */ + friend class CongruenceChannel; + + /** + * Output channel connected to the congruence closure module. + */ + CongruenceChannel d_ccChannel; + + /** + * Instance of the congruence closure module. + */ + CongruenceClosure<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cc; + + /** + * Union find for storing the equalities. + */ + UnionFind<Node, NodeHashFunction> d_unionFind; + + /** + * Received a notification from the congruence closure algorithm that the two nodes + * a and b have been merged. + */ + void notifyCongruent(TNode a, TNode b); + + /** + * List of all disequalities this theory has seen. + * Maintaints the invariant that if a is in the + * disequality list of b, then b is in that of a. + * */ + EqLists d_disequalities; + + /** List of all (potential) equalities to be propagated. */ + EqLists d_equalities; + + /** + * stores the conflicting disequality (still need to call construct + * conflict to get the actual explanation) + */ + Node d_conflict; + bool d_noMerge; + std::vector< std::vector< std::pair< Node, Node > > > d_merge_pending; +public: + TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation); + ~TheoryDatatypes(); + void preRegisterTerm(TNode n) { + TypeNode type = n.getType(); + if(type.getKind() == kind::DATATYPE_TYPE) { + addDatatypeDefinitions(type); + } + } + void registerTerm(TNode n) { } + + void presolve(); + + void addSharedTerm(TNode t); + void notifyEq(TNode lhs, TNode rhs); + void check(Effort e); + void propagate(Effort e) { } + void explain(TNode n, Effort e) { } + Node getValue(TNode n); + void shutdown() { } + std::string identify() const { return std::string("TheoryDatatypes"); } + + void addDatatypeDefinitions(TypeNode dttn); + +private: + /* Helper methods */ + void checkTester( Node assertion, bool doAdd = true ); + static bool checkTrivialTester(Node assertion); + void checkInstantiate( Node t ); + Node getPossibleCons( Node t, bool checkInst = false ); + Node collapseSelector( TNode t, bool useContext = false ); + void updateSelectors( Node a ); + void collectTerms( TNode t ); + void addTermToLabels( Node t ); + void initializeEqClass( Node t ); + + /* from uf_morgan */ + void merge(TNode a, TNode b); + inline TNode find(TNode a); + inline TNode debugFind(TNode a) const; + void appendToDiseqList(TNode of, TNode eq); + void appendToEqList(TNode of, TNode eq); + void addDisequality(TNode eq); + void addDerivedEquality(TNode eq, TNode jeq); + void addEquality(TNode eq); + void registerEqualityForPropagation(TNode eq); + void convertDerived(Node n, NodeBuilder<>& nb); + void throwConflict(); + + void checkCycles(); + bool searchForCycle( Node n, Node on, + std::map< Node, bool >& visited, + NodeBuilder<>& explanation ); + bool checkClash( Node n1, Node n2, NodeBuilder<>& explanation ); + static bool checkClashSimple( Node n1, Node n2 ); + friend class DatatypesRewriter;// for access to checkClashSimple(); +};/* class TheoryDatatypes */ + +inline TNode TheoryDatatypes::find(TNode a) { + return d_unionFind.find(a); +} + +inline TNode TheoryDatatypes::debugFind(TNode a) const { + return d_unionFind.debugFind(a); +} + + +}/* CVC4::theory::datatypes namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */ diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h new file mode 100644 index 000000000..1fd24cf53 --- /dev/null +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -0,0 +1,99 @@ +/********************* */ +/*! \file theory_datatypes_type_rules.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief Theory of datatypes + ** + ** Theory of datatypes. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H +#define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H + +namespace CVC4 { +namespace theory { +namespace datatypes { + +struct DatatypeConstructorTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); + TypeNode consType = n.getOperator().getType(check); + if(check) { + Debug("typecheck-idt") << "typecheck cons: " << n << " " << n.getNumChildren() << std::endl; + Debug("typecheck-idt") << "cons type: " << consType << " " << consType.getNumChildren() << std::endl; + if(n.getNumChildren() != consType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the constructor type"); + } + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + TypeNode::iterator tchild_it = consType.begin(); + for(; child_it != child_it_end; ++child_it, ++tchild_it) { + TypeNode childType = (*child_it).getType(check); + Debug("typecheck-idt") << "typecheck cons arg: " << childType << " " << (*tchild_it) << std::endl; + if(childType != *tchild_it) { + throw TypeCheckingExceptionPrivate(n, "bad type for constructor argument"); + } + } + } + return consType.getConstructorReturnType(); + } +};/* struct DatatypeConstructorTypeRule */ + +struct DatatypeSelectorTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::APPLY_SELECTOR); + TypeNode selType = n.getOperator().getType(check); + Debug("typecheck-idt") << "typecheck sel: " << n << std::endl; + Debug("typecheck-idt") << "sel type: " << selType << std::endl; + if(check) { + if(n.getNumChildren() != 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the selector type"); + } + TypeNode childType = n[0].getType(check); + if(selType[0] != childType) { + throw TypeCheckingExceptionPrivate(n, "bad type for selector argument"); + } + } + return selType[1]; + } +};/* struct DatatypeSelectorTypeRule */ + +struct DatatypeTesterTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw(TypeCheckingExceptionPrivate) { + Assert(n.getKind() == kind::APPLY_TESTER); + if(check) { + if(n.getNumChildren() != 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the tester type"); + } + TypeNode testType = n.getOperator().getType(check); + TypeNode childType = n[0].getType(check); + Debug("typecheck-idt") << "typecheck test: " << n << std::endl; + Debug("typecheck-idt") << "test type: " << testType << std::endl; + if(testType[0] != childType) { + throw TypeCheckingExceptionPrivate(n, "bad type for tester argument"); + } + } + return nodeManager->booleanType(); + } +};/* struct DatatypeSelectorTypeRule */ + + +}/* CVC4::theory::datatypes namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H */ diff --git a/src/theory/datatypes/union_find.cpp b/src/theory/datatypes/union_find.cpp new file mode 100644 index 000000000..e56c9f282 --- /dev/null +++ b/src/theory/datatypes/union_find.cpp @@ -0,0 +1,59 @@ +/********************* */ +/*! \file union_find.cpp + ** \verbatim + ** Original author: ajreynol + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Path-compressing, backtrackable union-find using an undo + ** stack. Refactored from the UF union-find. + ** + ** Path-compressing, backtrackable union-find using an undo stack + ** rather than storing items in a CDMap<>. + **/ + +#include <iostream> + +#include "theory/datatypes/union_find.h" +#include "util/Assert.h" +#include "expr/node.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace datatypes { + +template <class NodeType, class NodeHash> +void UnionFind<NodeType, NodeHash>::notify() { + Trace("datatypesuf") << "datatypesUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; + while(d_offset < d_trace.size()) { + pair<TNode, TNode> p = d_trace.back(); + if(p.second.isNull()) { + d_map.erase(p.first); + Trace("datatypesuf") << "datatypesUF " << d_trace.size() << " erasing " << p.first << endl; + } else { + d_map[p.first] = p.second; + Trace("datatypesuf") << "datatypesUF " << d_trace.size() << " replacing " << p << endl; + } + d_trace.pop_back(); + } + Trace("datatypesuf") << "datatypesUF cancelling finished." << endl; +} + +// The following declarations allow us to put functions in the .cpp file +// instead of the header, since we know which instantiations are needed. + +template void UnionFind<Node, NodeHashFunction>::notify(); + +template void UnionFind<TNode, TNodeHashFunction>::notify(); + +}/* CVC4::theory::datatypes namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/datatypes/union_find.h b/src/theory/datatypes/union_find.h new file mode 100644 index 000000000..31b18e7e9 --- /dev/null +++ b/src/theory/datatypes/union_find.h @@ -0,0 +1,148 @@ +/********************* */ +/*! \file union_find.h + ** \verbatim + ** Original author: ajreynol + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Path-compressing, backtrackable union-find using an undo + ** stack. Refactored from the UF union-find. + ** + ** Path-compressing, backtrackable union-find using an undo stack + ** rather than storing items in a CDMap<>. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__DATATYPES__UNION_FIND_H +#define __CVC4__THEORY__DATATYPES__UNION_FIND_H + +#include <utility> +#include <vector> +#include <ext/hash_map> + +#include "expr/node.h" +#include "context/cdo.h" + +namespace CVC4 { + +namespace context { + class Context; +}/* CVC4::context namespace */ + +namespace theory { +namespace datatypes { + +// NodeType \in { Node, TNode } +template <class NodeType, class NodeHash> +class UnionFind : context::ContextNotifyObj { + /** Our underlying map type. */ + typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; + + /** + * Our map of Nodes to their canonical representatives. + * If a Node is not present in the map, it is its own + * representative. + */ + MapType d_map; + + /** Our undo stack for changes made to d_map. */ + std::vector<std::pair<TNode, TNode> > d_trace; + + /** Our current offset in the d_trace stack (context-dependent). */ + context::CDO<size_t> d_offset; + +public: + UnionFind(context::Context* ctxt) : + context::ContextNotifyObj(ctxt), + d_offset(ctxt, 0) { + } + + ~UnionFind() throw() { } + + /** + * Return a Node's union-find representative, doing path compression. + */ + inline TNode find(TNode n); + + /** + * Return a Node's union-find representative, NOT doing path compression. + * This is useful for Assert() statements, debug checking, and similar + * things that you do NOT want to mutate the structure. + */ + inline TNode debugFind(TNode n) const; + + /** + * Set the canonical representative of n to newParent. They should BOTH + * be their own canonical representatives on entry to this funciton. + */ + inline void setCanon(TNode n, TNode newParent); + + +public: + /** + * Called by the Context when a pop occurs. Cancels everything to the + * current context level. Overrides ContextNotifyObj::notify(). + */ + void notify(); + +};/* class UnionFind<> */ + +template <class NodeType, class NodeHash> +inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const { + typename MapType::const_iterator i = d_map.find(n); + if(i == d_map.end()) { + return n; + } else { + return debugFind((*i).second); + } +} + +template <class NodeType, class NodeHash> +inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) { + Trace("datatypesuf") << "datatypesUF find of " << n << std::endl; + typename MapType::iterator i = d_map.find(n); + if(i == d_map.end()) { + Trace("datatypesuf") << "datatypesUF it is rep" << std::endl; + return n; + } else { + Trace("datatypesuf") << "datatypesUF not rep: par is " << (*i).second << std::endl; + std::pair<TNode, TNode> pr = *i; + // our iterator is invalidated by the recursive call to find(), + // since it mutates the map + TNode p = find(pr.second); + if(p == pr.second) { + return p; + } + d_trace.push_back(std::make_pair(n, pr.second)); + d_offset = d_trace.size(); + Trace("datatypesuf") << "datatypesUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl; + pr.second = p; + d_map.insert(pr); + return p; + } +} + +template <class NodeType, class NodeHash> +inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) { + Assert(d_map.find(n) == d_map.end()); + Assert(d_map.find(newParent) == d_map.end()); + if(n != newParent) { + Trace("datatypesuf") << "datatypesUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl; + d_map[n] = newParent; + d_trace.push_back(std::make_pair(n, TNode::null())); + d_offset = d_trace.size(); + } +} + +}/* CVC4::theory::datatypes namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /*__CVC4__THEORY__DATATYPES__UNION_FIND_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cb29bb98e..d37916515 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2,10 +2,10 @@ /*! \file theory_engine.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: barrett - ** Minor contributors (to current version): cconway, taking + ** Major contributors: taking, barrett, dejan + ** Minor contributors (to current version): cconway ** 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 @@ -166,6 +166,11 @@ struct preprocess_stack_element { }; Node TheoryEngine::preprocess(TNode node) { + // Make sure the node is type-checked first (some rewrites depend on + // typechecking having succeeded to be safe). + if(Options::current()->typeChecking) { + node.getType(true); + } // Remove ITEs and rewrite the node Node preprocessed = Rewriter::rewrite(removeITEs(node)); return preprocessed; @@ -300,7 +305,7 @@ Node TheoryEngine::removeITEs(TNode node) { Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])" << "->" - << "["<<newAssertion.getId() << "," << newAssertion << "]" + << "[" << newAssertion.getId() << "," << newAssertion << "]" << endl; Node preprocessed = preprocess(newAssertion); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 1cdae3810..6226406d7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -265,7 +265,7 @@ public: // Get the atom TNode atom = node.getKind() == kind::NOT ? node[0] : node; - // Again, eqaulity is a special case + // Again, equality is a special case if (atom.getKind() == kind::EQUAL) { theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]); Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl; diff --git a/src/util/Assert.h b/src/util/Assert.h index 5bb2e830f..ec942e00b 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): acsys ** 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 @@ -200,6 +200,29 @@ public: } };/* class IllegalArgumentException */ +class CVC4_PUBLIC InternalErrorException : public AssertionException { +protected: + InternalErrorException() : AssertionException() {} + +public: + InternalErrorException(const char* function, const char* file, unsigned line) : + AssertionException() { + construct("Internal error detected", "", + function, file, line); + } + + InternalErrorException(const char* function, const char* file, unsigned line, + const char* fmt, ...) : + AssertionException() { + va_list args; + va_start(args, fmt); + construct("Internal error detected", "", + function, file, line, fmt, args); + va_end(args); + } + +};/* class InternalErrorException */ + #ifdef CVC4_DEBUG #ifdef CVC4_DEBUG @@ -249,6 +272,8 @@ void debugAssertionFailed(const AssertionException& thisException, throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unimplemented(msg...) \ throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) +#define InternalError(msg...) \ + throw InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define CheckArgument(cond, arg, msg...) \ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 24d82f01c..eb63885a2 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -37,6 +37,8 @@ libutil_la_SOURCES = \ configuration_private.h \ configuration.cpp \ bitvector.h \ + datatype.h \ + datatype.cpp \ gmp_util.h \ sexpr.h \ stats.h \ diff --git a/src/util/bitvector.h b/src/util/bitvector.h index ca69fb506..ade08164b 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -2,10 +2,10 @@ /*! \file bitvector.h ** \verbatim ** Original author: dejan - ** Major contributors: cconway - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters, cconway + ** 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 @@ -28,7 +28,7 @@ namespace CVC4 { -class BitVector { +class CVC4_PUBLIC BitVector { private: @@ -157,24 +157,24 @@ inline BitVector::BitVector(const std::string& num, unsigned base) { } d_value = Integer(num,base); -} +}/* BitVector::BitVector() */ /** * Hash function for the BitVector constants. */ -struct BitVectorHashStrategy { +struct CVC4_PUBLIC BitVectorHashStrategy { static inline size_t hash(const BitVector& bv) { return bv.hash(); } -}; +};/* struct BitVectorHashStrategy */ /** * The structure representing the extraction operation for bit-vectors. The * operation map bit-vectors to bit-vector of size <code>high - low + 1</code> * by taking the bits at indices <code>high ... low</code> */ -struct BitVectorExtract { +struct CVC4_PUBLIC BitVectorExtract { /** The high bit of the range for this extract */ unsigned high; /** The low bit of the range for this extract */ @@ -186,73 +186,75 @@ struct BitVectorExtract { bool operator == (const BitVectorExtract& extract) const { return high == extract.high && low == extract.low; } -}; +};/* struct BitVectorExtract */ /** * Hash function for the BitVectorExtract objects. */ -class BitVectorExtractHashStrategy { +class CVC4_PUBLIC BitVectorExtractHashStrategy { public: static size_t hash(const BitVectorExtract& extract) { size_t hash = extract.low; hash ^= extract.high + 0x9e3779b9 + (hash << 6) + (hash >> 2); return hash; } -}; +};/* class BitVectorExtractHashStrategy */ -struct BitVectorSize { +struct CVC4_PUBLIC BitVectorSize { unsigned size; BitVectorSize(unsigned size) : size(size) {} operator unsigned () const { return size; } -}; +};/* struct BitVectorSize */ -struct BitVectorRepeat { +struct CVC4_PUBLIC BitVectorRepeat { unsigned repeatAmount; BitVectorRepeat(unsigned repeatAmount) : repeatAmount(repeatAmount) {} operator unsigned () const { return repeatAmount; } -}; +};/* struct BitVectorRepeat */ -struct BitVectorZeroExtend { +struct CVC4_PUBLIC BitVectorZeroExtend { unsigned zeroExtendAmount; BitVectorZeroExtend(unsigned zeroExtendAmount) : zeroExtendAmount(zeroExtendAmount) {} operator unsigned () const { return zeroExtendAmount; } -}; +};/* struct BitVectorZeroExtend */ -struct BitVectorSignExtend { +struct CVC4_PUBLIC BitVectorSignExtend { unsigned signExtendAmount; BitVectorSignExtend(unsigned signExtendAmount) : signExtendAmount(signExtendAmount) {} operator unsigned () const { return signExtendAmount; } -}; +};/* struct BitVectorSignExtend */ -struct BitVectorRotateLeft { +struct CVC4_PUBLIC BitVectorRotateLeft { unsigned rotateLeftAmount; BitVectorRotateLeft(unsigned rotateLeftAmount) : rotateLeftAmount(rotateLeftAmount) {} operator unsigned () const { return rotateLeftAmount; } -}; +};/* struct BitVectorRotateLeft */ -struct BitVectorRotateRight { +struct CVC4_PUBLIC BitVectorRotateRight { unsigned rotateRightAmount; BitVectorRotateRight(unsigned rotateRightAmount) : rotateRightAmount(rotateRightAmount) {} operator unsigned () const { return rotateRightAmount; } -}; +};/* struct BitVectorRotateRight */ template <typename T> -struct UnsignedHashStrategy { +struct CVC4_PUBLIC UnsignedHashStrategy { static inline size_t hash(const T& x) { return (size_t)x; } -}; +};/* struct UnsignedHashStrategy */ +inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) CVC4_PUBLIC; inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) { return os << bv.toString(); } +inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) CVC4_PUBLIC; inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) { return os << "[" << bv.high << ":" << bv.low << "]"; } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp new file mode 100644 index 000000000..c795eaba6 --- /dev/null +++ b/src/util/datatype.cpp @@ -0,0 +1,371 @@ +/********************* */ +/*! \file datatype.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief A class representing a Datatype definition + ** + ** A class representing a Datatype definition for the theory of + ** inductive datatypes. + **/ + +#include <string> +#include <sstream> + +#include "util/datatype.h" +#include "expr/type.h" +#include "expr/expr_manager.h" +#include "expr/node.h" + +using namespace std; + +namespace CVC4 { + +namespace expr { + namespace attr { + struct DatatypeIndexTag {}; + } +} + +typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr; + +const Datatype& Datatype::datatypeOf(Expr item) { + TypeNode t = Node::fromExpr(item).getType(); + switch(t.getKind()) { + case kind::CONSTRUCTOR_TYPE: + return t[t.getNumChildren() - 1].getConst<Datatype>(); + case kind::SELECTOR_TYPE: + case kind::TESTER_TYPE: + return t[0].getConst<Datatype>(); + default: + Unhandled("arg must be a datatype constructor, selector, or tester"); + } +} + +size_t Datatype::indexOf(Expr item) { + AssertArgument(item.getType().isConstructor() || + item.getType().isTester() || + item.getType().isSelector(), + item, + "arg must be a datatype constructor, selector, or tester"); + TNode n = Node::fromExpr(item); + Assert(n.hasAttribute(DatatypeIndexAttr())); + return n.getAttribute(DatatypeIndexAttr()); +} + +void Datatype::resolve(ExprManager* em, + const std::map<std::string, DatatypeType>& resolutions) + throw(AssertionException, DatatypeResolutionException) { + + CheckArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(!d_resolved, "cannot resolve a Datatype twice"); + CheckArgument(resolutions.find(d_name) != resolutions.end(), "Datatype::resolve(): resolutions doesn't contain me!"); + DatatypeType self = (*resolutions.find(d_name)).second; + CheckArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!"); + d_resolved = true; + size_t index = 0; + for(iterator i = begin(), i_end = end(); i != i_end; ++i) { + (*i).resolve(em, self, resolutions); + Assert((*i).isResolved()); + Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); + Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); + } + Assert(index == getNumConstructors()); +} + +void Datatype::addConstructor(const Constructor& c) { + CheckArgument(!d_resolved, this, + "cannot add a constructor to a finalized Datatype"); + d_constructors.push_back(c); +} + +bool Datatype::operator==(const Datatype& other) const throw() { + // two datatypes are == iff the name is the same and they have + // exactly matching constructors (in the same order) + + if(this == &other) { + return true; + } + + if(isResolved() != other.isResolved()) { + return false; + } + + if(d_name != other.d_name || + getNumConstructors() != other.getNumConstructors()) { + return false; + } + for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) { + Assert(j != other.end()); + // two constructors are == iff they have the same name, their + // constructors and testers are equal and they have exactly + // matching args (in the same order) + if((*i).getName() != (*j).getName() || + (*i).getNumArgs() != (*j).getNumArgs()) { + return false; + } + // testing equivalence of constructors and testers is harder b/c + // this constructor might not be resolved yet; only compare them + // if they are both resolved + Assert(isResolved() == !(*i).d_constructor.isNull() && + isResolved() == !(*i).d_tester.isNull() && + (*i).d_constructor.isNull() == (*j).d_constructor.isNull() && + (*i).d_tester.isNull() == (*j).d_tester.isNull()); + if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) { + return false; + } + if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) { + return false; + } + for(Constructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) { + Assert(l != (*j).end()); + if((*k).getName() != (*l).getName()) { + return false; + } + // testing equivalence of selectors is harder b/c args might not + // be resolved yet + Assert(isResolved() == (*k).isResolved() && + (*k).isResolved() == (*l).isResolved()); + if((*k).isResolved()) { + // both are resolved, so simply compare the selectors directly + if((*k).d_selector != (*l).d_selector) { + return false; + } + } else { + // neither is resolved, so compare their (possibly unresolved) + // types; we don't know if they'll be resolved the same way, + // so we can't ever say unresolved types are equal + if(!(*k).d_selector.isNull() && !(*l).d_selector.isNull()) { + if((*k).d_selector.getType() != (*l).d_selector.getType()) { + return false; + } + } else { + if((*k).isUnresolvedSelf() && (*l).isUnresolvedSelf()) { + // Fine, the selectors are equal if the rest of the + // enclosing datatypes are equal... + } else { + return false; + } + } + } + } + } + return true; +} + +const Datatype::Constructor& Datatype::operator[](size_t index) const { + CheckArgument(index < getNumConstructors(), index, "index out of bounds"); + return d_constructors[index]; +} + +void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self, + const std::map<std::string, DatatypeType>& resolutions) + throw(AssertionException, DatatypeResolutionException) { + CheckArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager"); + CheckArgument(!isResolved(), + "cannot resolve a Datatype constructor twice; " + "perhaps the same constructor was added twice, " + "or to two datatypes?"); + size_t index = 0; + for(iterator i = begin(), i_end = end(); i != i_end; ++i) { + if((*i).d_selector.isNull()) { + string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1); + (*i).d_name.resize((*i).d_name.find('\0')); + if(typeName == "") { + (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, self)); + } else { + map<string, DatatypeType>::const_iterator j = resolutions.find(typeName); + if(j == resolutions.end()) { + stringstream msg; + msg << "cannot resolve type \"" << typeName << "\" " + << "in selector \"" << (*i).d_name << "\" " + << "of constructor \"" << d_name << "\""; + throw DatatypeResolutionException(msg.str()); + } else { + (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, (*j).second)); + } + } + } else { + (*i).d_selector = em->mkVar((*i).d_name, em->mkSelectorType(self, (*i).d_selector.getType())); + } + Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); + (*i).d_resolved = true; + } + + Assert(index == getNumArgs()); + + // Set constructor/tester last, since Constructor::isResolved() + // returns true when d_tester is not the null Expr. If something + // fails above, we want Constuctor::isResolved() to remain "false" + d_tester = em->mkVar(d_name.substr(d_name.find('\0') + 1), em->mkTesterType(self)); + d_name.resize(d_name.find('\0')); + d_constructor = em->mkVar(d_name, em->mkConstructorType(*this, self)); +} + +Datatype::Constructor::Constructor(std::string name, std::string tester) : + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we stow + // the tester name away inside the constructor name until + // resolution. + d_name(name + '\0' + tester), + d_tester(), + d_args() { + CheckArgument(name != "", name, "cannot construct a datatype constructor without a name"); + CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester"); +} + +void Datatype::Constructor::addArg(std::string selectorName, Type selectorType) { + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we stow + // the selector type away inside a var until resolution (when we can + // create the proper selector type) + CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type"); + Expr type = selectorType.getExprManager()->mkVar(selectorType); + Debug("datatypes") << type << endl; + d_args.push_back(Arg(selectorName, type)); +} + +void Datatype::Constructor::addArg(std::string selectorName, Datatype::UnresolvedType selectorType) { + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we stow + // the selector type away after a NUL in the name string until + // resolution (when we can create the proper selector type) + CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type"); + d_args.push_back(Arg(selectorName + '\0' + selectorType.getName(), Expr())); +} + +void Datatype::Constructor::addArg(std::string selectorName, Datatype::SelfType) { + // We don't want to introduce a new data member, because eventually + // we're going to be a constant stuffed inside a node. So we mark + // the name string with a NUL to indicate that we have a + // self-selecting selector until resolution (when we can create the + // proper selector type) + CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor"); + d_args.push_back(Arg(selectorName + '\0', Expr())); +} + +std::string Datatype::Constructor::getName() const throw() { + string name = d_name; + if(!isResolved()) { + name.resize(name.find('\0')); + } + return name; +} + +Expr Datatype::Constructor::getConstructor() const { + CheckArgument(isResolved(), this, "this datatype constructor not yet resolved"); + return d_constructor; +} + +Expr Datatype::Constructor::getTester() const { + CheckArgument(isResolved(), this, "this datatype constructor not yet resolved"); + return d_tester; +} + +const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const { + CheckArgument(index < getNumArgs(), index, "index out of bounds"); + return d_args[index]; +} + +Datatype::Constructor::Arg::Arg(std::string name, Expr selector) : + d_name(name), + d_selector(selector), + d_resolved(false) { + CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name"); +} + +std::string Datatype::Constructor::Arg::getName() const throw() { + string name = d_name; + const size_t nul = name.find('\0'); + if(nul != string::npos) { + name.resize(nul); + } + return name; +} + +Expr Datatype::Constructor::Arg::getSelector() const { + CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor"); + return d_selector; +} + +bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() { + return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1; +} + +std::string Datatype::Constructor::Arg::getSelectorTypeName() const { + Type t; + if(isResolved()) { + t = SelectorType(d_selector.getType()).getRangeType(); + } else { + if(d_selector.isNull()) { + string typeName = d_name.substr(d_name.find('\0') + 1); + return (typeName == "") ? "[self]" : typeName; + } else { + t = d_selector.getType(); + } + } + + return t.isDatatype() ? DatatypeType(t).getDatatype().getName() : t.toString(); +} + +std::ostream& operator<<(std::ostream& os, const Datatype& dt) { + // can only output datatypes in the CVC4 native language + Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + + os << "DATATYPE " << dt.getName() << " =" << endl; + Datatype::const_iterator i = dt.begin(), i_end = dt.end(); + if(i != i_end) { + os << " "; + do { + os << *i << endl; + if(++i != i_end) { + os << "| "; + } + } while(i != i_end); + } + os << "END;" << endl; + + return os; +} + +std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) { + // can only output datatypes in the CVC4 native language + Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + + os << ctor.getName(); + + Datatype::Constructor::const_iterator i = ctor.begin(), i_end = ctor.end(); + if(i != i_end) { + os << "("; + do { + os << *i; + if(++i != i_end) { + os << ", "; + } + } while(i != i_end); + os << ")"; + } + + return os; +} + +std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) { + // can only output datatypes in the CVC4 native language + Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + + os << arg.getName() << ": " << arg.getSelectorTypeName(); + + return os; +} + +}/* CVC4 namespace */ diff --git a/src/util/datatype.h b/src/util/datatype.h new file mode 100644 index 000000000..e3e7d669c --- /dev/null +++ b/src/util/datatype.h @@ -0,0 +1,445 @@ +/********************* */ +/*! \file datatype.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief A class representing a Datatype definition + ** + ** A class representing a Datatype definition for the theory of + ** inductive datatypes. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__DATATYPE_H +#define __CVC4__DATATYPE_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> + +namespace CVC4 { + // messy; Expr needs Datatype (because it's the payload of a + // CONSTANT-kinded expression), and Datatype needs Expr. + class CVC4_PUBLIC Datatype; +}/* CVC4 namespace */ + +#include "expr/expr.h" +#include "expr/type.h" +#include "util/Assert.h" +#include "util/output.h" +#include "util/hash.h" +#include "util/exception.h" + +namespace CVC4 { + +class CVC4_PUBLIC ExprManager; + +/** + * An exception that is thrown when a datatype resolution fails. + */ +class CVC4_PUBLIC DatatypeResolutionException : public Exception { +public: + inline DatatypeResolutionException(std::string msg); +};/* class DatatypeResolutionException */ + +/** + * The representation of an inductive datatype. + * + * This is far more complicated than it first seems. Consider this + * datatype definition: + * + * DATATYPE nat = + * succ(pred: nat) + * | zero + * END; + * + * You cannot define "nat" until you have a Type for it, but you + * cannot have a Type for it until you fill in the type of the "pred" + * selector, which needs the Type. So we have a chicken-and-egg + * problem. It's even more complicated when we have mutual recusion + * between datatypes, since the CVC presentation language does not + * require forward-declarations. Here, we define trees of lists that + * contain trees of lists (etc): + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(list), + * list = cons(car: tree, cdr: list) | nil + * END; + * + * Note that while parsing the "tree" definition, we have to take it + * on faith that "list" is a valid type. We build Datatype objects to + * describe "tree" and "list", and their constructors and constructor + * arguments, but leave any unknown types (including self-references) + * in an "unresolved" state. After parsing the whole DATATYPE block, + * we create a DatatypeType through + * ExprManager::mkMutualDatatypeTypes(). The ExprManager creates a + * DatatypeType for each, but before "releasing" this type into the + * wild, it does a round of in-place "resolution" on each Datatype by + * calling Datatype::resolve() with a map of string -> DatatypeType to + * allow the datatype to construct the necessary testers and + * selectors. + * + * An additional point to make is that we want to ease the burden on + * both the parser AND the users of the CVC4 API, so this class takes + * on the task of generating its own selectors and testers, for + * instance. That means that, after reifying the Datatype with the + * ExprManager, the parser needs to go through the (now-resolved) + * Datatype and request ; see src/parser/parser.cpp for how this is + * done. For API usage ideas, see test/unit/util/datatype_black.h. + */ +class CVC4_PUBLIC Datatype { +public: + static const Datatype& datatypeOf(Expr item); + static size_t indexOf(Expr item); + + /** + * A holder type (used in calls to Datatype::Constructor::addArg()) + * to allow a Datatype to refer to itself. Self-typed fields of + * Datatypes will be properly typed when a Type is created for the + * Datatype by the ExprManager (which calls Datatype::resolve()). + */ + class CVC4_PUBLIC SelfType { + };/* class Datatype::SelfType */ + + /** + * An unresolved type (used in calls to + * Datatype::Constructor::addArg()) to allow a Datatype to refer to + * itself or to other mutually-recursive Datatypes. Unresolved-type + * fields of Datatypes will be properly typed when a Type is created + * for the Datatype by the ExprManager (which calls + * Datatype::resolve()). + */ + class CVC4_PUBLIC UnresolvedType { + std::string d_name; + public: + inline UnresolvedType(std::string name); + inline std::string getName() const throw(); + };/* class Datatype::UnresolvedType */ + + /** + * A constructor for a Datatype. + */ + class CVC4_PUBLIC Constructor { + public: + /** + * A Datatype constructor argument (i.e., a Datatype field). + */ + class CVC4_PUBLIC Arg { + + std::string d_name; + Expr d_selector; + bool d_resolved; + + explicit Arg(std::string name, Expr selector); + friend class Constructor; + friend class Datatype; + + bool isUnresolvedSelf() const throw(); + + public: + + /** Get the name of this constructor argument. */ + std::string getName() const throw(); + /** + * Get the selector for this constructor argument; this call is + * only permitted after resolution. + */ + Expr getSelector() const; + /** + * Get the name of the type of this constructor argument + * (Datatype field). Can be used for not-yet-resolved Datatypes + * (in which case the name of the unresolved type, or "[self]" + * for a self-referential type is returned). + */ + std::string getSelectorTypeName() const; + + /** + * Returns true iff this constructor argument has been resolved. + */ + bool isResolved() const throw(); + + };/* class Datatype::Constructor::Arg */ + + /** The type for iterators over constructor arguments. */ + typedef std::vector<Arg>::iterator iterator; + /** The (const) type for iterators over constructor arguments. */ + typedef std::vector<Arg>::const_iterator const_iterator; + + private: + + std::string d_name; + Expr d_constructor; + Expr d_tester; + std::vector<Arg> d_args; + + void resolve(ExprManager* em, DatatypeType self, + const std::map<std::string, DatatypeType>& resolutions) + throw(AssertionException, DatatypeResolutionException); + friend class Datatype; + + public: + /** + * Create a new Datatype constructor with the given name for the + * constructor and the given name for the tester. The actual + * constructor and tester aren't created until resolution time. + */ + explicit Constructor(std::string name, std::string tester); + + /** + * Add an argument (i.e., a data field) of the given name and type + * to this Datatype constructor. + */ + void addArg(std::string selectorName, Type selectorType); + /** + * Add an argument (i.e., a data field) of the given name to this + * Datatype constructor that refers to an as-yet-unresolved + * Datatype (which may be mutually-recursive). + */ + void addArg(std::string selectorName, Datatype::UnresolvedType selectorType); + /** + * Add a self-referential (i.e., a data field) of the given name + * to this Datatype constructor that refers to the enclosing + * Datatype. For example, using the familiar "nat" Datatype, to + * create the "pred" field for "succ" constructor, one uses + * succ::addArg("pred", Datatype::SelfType())---the actual Type + * cannot be passed because the Datatype is still under + * construction. + * + * This is a special case of + * Constructor::addArg(std::string, Datatype::UnresolvedType). + */ + void addArg(std::string selectorName, Datatype::SelfType); + + /** Get the name of this Datatype constructor. */ + std::string getName() const throw(); + /** + * Get the constructor operator of this Datatype constructor. The + * Datatype must be resolved. + */ + Expr getConstructor() const; + /** + * Get the tester operator of this Datatype constructor. The + * Datatype must be resolved. + */ + Expr getTester() const; + /** + * Get the number of arguments (so far) of this Datatype constructor. + */ + inline size_t getNumArgs() const throw(); + + /** + * Returns true iff this Datatype constructor has already been + * resolved. + */ + inline bool isResolved() const throw(); + + /** Get the beginning iterator over Constructor args. */ + inline iterator begin() throw(); + /** Get the ending iterator over Constructor args. */ + inline iterator end() throw(); + /** Get the beginning const_iterator over Constructor args. */ + inline const_iterator begin() const throw(); + /** Get the ending const_iterator over Constructor args. */ + inline const_iterator end() const throw(); + + /** Get the ith Constructor arg. */ + const Arg& operator[](size_t index) const; + + };/* class Datatype::Constructor */ + + /** The type for iterators over constructors. */ + typedef std::vector<Constructor>::iterator iterator; + /** The (const) type for iterators over constructors. */ + typedef std::vector<Constructor>::const_iterator const_iterator; + +private: + std::string d_name; + std::vector<Constructor> d_constructors; + bool d_resolved; + + /** + * Datatypes refer to themselves, recursively, and we have a + * chicken-and-egg problem. The DatatypeType around the Datatype + * cannot exist until the Datatype is finalized, and the Datatype + * cannot refer to the DatatypeType representing itself until it + * exists. resolve() is called by the ExprManager when a Type. Has + * the effect of freezing the object, too; that is, addConstructor() + * will fail after a call to resolve(). + */ + void resolve(ExprManager* em, + const std::map<std::string, DatatypeType>& resolutions) + throw(AssertionException, DatatypeResolutionException); + friend class ExprManager;// for access to resolve() + +public: + + /** Create a new Datatype of the given name. */ + inline explicit Datatype(std::string name); + + /** Add a constructor to this Datatype. */ + void addConstructor(const Constructor& c); + + /** Get the name of this Datatype. */ + inline std::string getName() const throw(); + /** Get the number of constructors (so far) for this Datatype. */ + inline size_t getNumConstructors() const throw(); + + /** + * Return true iff the two Datatypes are the same. + * + * We need == for mkConst(Datatype) to properly work---since if the + * Datatype Expr requested is the same as an already-existing one, + * we need to return that one. For that, we have a hash and + * operator==. We provide != for symmetry. We don't provide + * operator<() etc. because given two Datatype Exprs, you could + * simply compare those rather than the (bare) Datatypes. This + * means, though, that Datatype cannot be stored in a sorted list or + * RB tree directly, so maybe we can consider adding these + * comparison operators later on. + */ + bool operator==(const Datatype& other) const throw(); + /** Return true iff the two Datatypes are not the same. */ + inline bool operator!=(const Datatype& other) const throw(); + + /** Return true iff this Datatype has already been resolved. */ + inline bool isResolved() const throw(); + + /** Get the beginning iterator over Constructors. */ + inline iterator begin() throw(); + /** Get the ending iterator over Constructors. */ + inline iterator end() throw(); + /** Get the beginning const_iterator over Constructors. */ + inline const_iterator begin() const throw(); + /** Get the ending const_iterator over Constructors. */ + inline const_iterator end() const throw(); + + /** Get the ith Constructor. */ + const Constructor& operator[](size_t index) const; + +};/* class Datatype */ + + +/** + * A hash strategy for Datatypes. Needed because Datatypes are used + * as the constant payload in CONSTANT-kinded TypeNodes (for + * DATATYPE_TYPE expressions). + */ +struct CVC4_PUBLIC DatatypeHashStrategy { + static inline size_t hash(const Datatype& dt) { + return StringHashFunction()(dt.getName()); + } +};/* struct DatatypeHashStrategy */ + + +// FUNCTION DECLARATIONS FOR OUTPUT STREAMS + +std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) CVC4_PUBLIC; + +// INLINE FUNCTIONS + +inline DatatypeResolutionException::DatatypeResolutionException(std::string msg) : + Exception(msg) { +} + +inline Datatype::UnresolvedType::UnresolvedType(std::string name) : + d_name(name) { +} + +inline std::string Datatype::UnresolvedType::getName() const throw() { + return d_name; +} + +inline Datatype::Datatype(std::string name) : + d_name(name), + d_constructors(), + d_resolved(false) { +} + +inline std::string Datatype::getName() const throw() { + return d_name; +} + +inline size_t Datatype::getNumConstructors() const throw() { + return d_constructors.size(); +} + +inline bool Datatype::operator!=(const Datatype& other) const throw() { + return !(*this == other); +} + +inline bool Datatype::isResolved() const throw() { + return d_resolved; +} + +inline Datatype::iterator Datatype::begin() throw() { + return d_constructors.begin(); +} + +inline Datatype::iterator Datatype::end() throw() { + return d_constructors.end(); +} + +inline Datatype::const_iterator Datatype::begin() const throw() { + return d_constructors.begin(); +} + +inline Datatype::const_iterator Datatype::end() const throw() { + return d_constructors.end(); +} + +inline bool Datatype::Constructor::isResolved() const throw() { + return !d_tester.isNull(); +} + +inline size_t Datatype::Constructor::getNumArgs() const throw() { + return d_args.size(); +} + +inline bool Datatype::Constructor::Arg::isResolved() const throw() { + // We could just write: + // + // return !d_selector.isNull() && d_selector.getType().isSelector(); + // + // HOWEVER, this causes problems in ExprManager tear-down, because + // the attributes are removed before the pool is purged. When the + // pool is purged, this triggers an equality test between Datatypes, + // and this triggers a call to isResolved(), which breaks because + // d_selector has no type after attributes are stripped. + // + // This problem, coupled with the fact that this function is called + // _often_, means we should just use a boolean flag. + // + return d_resolved; +} + +inline Datatype::Constructor::iterator Datatype::Constructor::begin() throw() { + return d_args.begin(); +} + +inline Datatype::Constructor::iterator Datatype::Constructor::end() throw() { + return d_args.end(); +} + +inline Datatype::Constructor::const_iterator Datatype::Constructor::begin() const throw() { + return d_args.begin(); +} + +inline Datatype::Constructor::const_iterator Datatype::Constructor::end() const throw() { + return d_args.end(); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__DATATYPE_H */ diff --git a/test/Makefile.am b/test/Makefile.am index 10b724a7d..aceef1b68 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \ blu='[1;34m'; \ std='[m'; \ } -subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3 +subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3 check-recursive: check-pre .PHONY: check-pre check-pre: diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index c732ffbb2..12e2bb347 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra bv lemmas push-pop +SUBDIRS = . arith precedence uf uflra bv datatypes lemmas push-pop TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 MAKEFLAGS = -k diff --git a/test/regress/regress0/datatypes/Makefile b/test/regress/regress0/datatypes/Makefile new file mode 100644 index 000000000..dc577ad8b --- /dev/null +++ b/test/regress/regress0/datatypes/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/datatypes + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am new file mode 100644 index 000000000..8d6dbbf73 --- /dev/null +++ b/test/regress/regress0/datatypes/Makefile.am @@ -0,0 +1,39 @@ +SUBDIRS = . + +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + datatype.cvc \ + datatype0.cvc \ + datatype1.cvc \ + datatype2.cvc \ + datatype3.cvc \ + datatype4.cvc \ + datatype13.cvc \ + mutually-recursive.cvc \ + rewriter.cvc \ + typed_v1l50016-simp.cvc + +EXTRA_DIST = $(TESTS) + +if CVC4_BUILD_PROFILE_COMPETITION +else +TESTS += \ + error.cvc +endif + +# and make sure to distribute it +EXTRA_DIST += \ + error.cvc + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/datatypes/datatype.cvc b/test/regress/regress0/datatypes/datatype.cvc new file mode 100644 index 000000000..38a7a017d --- /dev/null +++ b/test/regress/regress0/datatypes/datatype.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 + +DATATYPE nat = succ(pred : nat) | zero END; + +x : nat; + +QUERY (NOT is_succ(x) AND NOT is_zero(x)); diff --git a/test/regress/regress0/datatypes/datatype0.cvc b/test/regress/regress0/datatypes/datatype0.cvc new file mode 100644 index 000000000..02ba3c8ea --- /dev/null +++ b/test/regress/regress0/datatypes/datatype0.cvc @@ -0,0 +1,8 @@ +% EXPECT: valid +% EXIT: 20 + +DATATYPE nat = succ(pred : nat) | zero END; + +x : nat; + +QUERY (is_succ(x) OR is_zero(x)); diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc new file mode 100644 index 000000000..4c5984cb9 --- /dev/null +++ b/test/regress/regress0/datatypes/datatype1.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 + +DATATYPE + tree = node(left : tree, right : tree) | leaf +END; + +x : tree; +z : tree; + +QUERY NOT (left(left(z)) = x AND is_node(z) AND z = x); diff --git a/test/regress/regress0/datatypes/datatype13.cvc b/test/regress/regress0/datatypes/datatype13.cvc new file mode 100644 index 000000000..3cf4def42 --- /dev/null +++ b/test/regress/regress0/datatypes/datatype13.cvc @@ -0,0 +1,44 @@ +% EXPECT: valid +% EXIT: 20 + +DATATYPE enum = enum1 +| enum2 +| enum3 +| enum4 +| enum5 +| enum6 +| enum7 +| enum8 +| enum9 +| enum10 +| enum11 +| enum12 +| enum13 +| enum14 +| enum15 +| enum16 +| enum17 +| enum18 +| enum19 +| enum20 +| enum21 +| enum22 +| enum23 +| enum24 +| enum25 +| enum26 +| enum27 +| enum28 +| enum29 +| enum30 +| enum31 +| enum32 +| enum33 +END; + +x,y:enum; + +ASSERT x = enum1; +ASSERT y = enum33; +QUERY x /= y; + diff --git a/test/regress/regress0/datatypes/datatype2.cvc b/test/regress/regress0/datatypes/datatype2.cvc new file mode 100644 index 000000000..2e43b37e2 --- /dev/null +++ b/test/regress/regress0/datatypes/datatype2.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 + +DATATYPE + nat = succ(pred : nat) | zero, + list = cons(car : tree, cdr : list) | null, + tree = node(data : nat, children : list) | leaf +END; + +x : nat; +y : list; +z : tree; + +ASSERT x = succ(zero); +ASSERT z = IF is_cons(y) THEN car(y) ELSE node(x, null) ENDIF; + +QUERY (NOT is_cons(y)) => pred(data(z)) = zero; diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc new file mode 100644 index 000000000..53c9e2ffc --- /dev/null +++ b/test/regress/regress0/datatypes/datatype3.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 + +DATATYPE + tree = node(left : tree, right : tree) | leaf +END; + +x : tree; +z : tree; + +QUERY NOT (left(left(left(left(left(left(left(left(left(left(z)))))))))) = x AND is_node(z) AND z = x); diff --git a/test/regress/regress0/datatypes/datatype4.cvc b/test/regress/regress0/datatypes/datatype4.cvc new file mode 100644 index 000000000..87800919d --- /dev/null +++ b/test/regress/regress0/datatypes/datatype4.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +% EXIT: 10 +DATATYPE + TypeGeneric = generic +END; + +f: TypeGeneric -> INT; +a: TypeGeneric; + +QUERY(f(a) = 0); diff --git a/test/regress/regress0/datatypes/error.cvc b/test/regress/regress0/datatypes/error.cvc new file mode 100644 index 000000000..66fa17e02 --- /dev/null +++ b/test/regress/regress0/datatypes/error.cvc @@ -0,0 +1,7 @@ +% EXPECT-ERROR: CVC4 Error: +% EXPECT-ERROR: Parse Error: foo already declared +% EXIT: 1 + +DATATYPE single_ctor = foo(bar:REAL) END; +DATATYPE double_ctor = foo(bar:REAL) END; + diff --git a/test/regress/regress0/datatypes/mutually-recursive.cvc b/test/regress/regress0/datatypes/mutually-recursive.cvc new file mode 100644 index 000000000..68d5cd868 --- /dev/null +++ b/test/regress/regress0/datatypes/mutually-recursive.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 + +DATATYPE nat = succ(pred : nat2) | zero, + nat2 = succ2(pred2 : nat) | zero2 END; + +x : nat; + +DATATYPE list = cons(car : tree, cdr: list) | nil, + tree = node(left : tree, right : tree) | leaf(data : list) END; + +y : tree; + +QUERY (is_succ(x) => is_zero2(pred(x)) OR is_succ2(pred(x))) + AND (is_leaf(y) => is_cons(data(y)) OR is_nil(data(y))); diff --git a/test/regress/regress0/datatypes/rewriter.cvc b/test/regress/regress0/datatypes/rewriter.cvc new file mode 100644 index 000000000..f031e0462 --- /dev/null +++ b/test/regress/regress0/datatypes/rewriter.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 + +% simple test for rewriter cases + +DATATYPE single_ctor = foo(bar:REAL) END; +DATATYPE double_ctor = foo2(bar2:REAL) | baz END; + +x: single_ctor; +y: double_ctor; + +QUERY is_foo(x) AND bar2(foo2(0.0)) = 0.0; + diff --git a/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc b/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc new file mode 100644 index 000000000..b273d99e9 --- /dev/null +++ b/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc @@ -0,0 +1,44 @@ +% 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 : list ; +x3 : tree ; + +QUERY + +(NOT is_zero((LET x154 = (LET x155 = node((LET x156 = (LET x157 = (LET x158 = (LET x159 = (LET x160 = (LET x161 = (LET x162 = cons((LET x163 = (LET x164 = (LET x165 = (LET x166 = (LET x167 = (LET x168 = (LET x169 = (LET x170 = (LET x171 = (LET x172 = (LET x173 = x3 IN + (IF is_node(x173) THEN children(x173) ELSE null ENDIF)) IN + (IF is_cons(x172) THEN car(x172) ELSE leaf(zero) ENDIF)) IN + (IF is_node(x171) THEN children(x171) ELSE null ENDIF)) IN + (IF is_cons(x170) THEN cdr(x170) ELSE null ENDIF)) IN + (IF is_cons(x169) THEN car(x169) ELSE leaf(zero) ENDIF)) IN + (IF is_node(x168) THEN children(x168) ELSE null ENDIF)) IN + (IF is_cons(x167) THEN cdr(x167) ELSE null ENDIF)) IN + (IF is_cons(x166) THEN cdr(x166) ELSE null ENDIF)) IN + (IF is_cons(x165) THEN cdr(x165) ELSE null ENDIF)) IN + (IF is_cons(x164) THEN cdr(x164) ELSE null ENDIF)) IN + (IF is_cons(x163) THEN car(x163) ELSE leaf(zero) ENDIF)),cons((LET x174 = cons(x3,(LET x175 = node(cons(node((LET x176 = x3 IN + (IF is_node(x176) THEN children(x176) ELSE null ENDIF))),x2)) IN + (IF is_node(x175) THEN children(x175) ELSE null ENDIF))) IN + (IF is_cons(x174) THEN car(x174) ELSE leaf(zero) ENDIF)),cons(leaf(succ((LET x177 = node(null) IN + (IF is_leaf(x177) THEN data(x177) ELSE zero ENDIF)))),(LET x178 = (LET x179 = (LET x180 = (LET x181 = node(x2) IN + (IF is_node(x181) THEN children(x181) ELSE null ENDIF)) IN + (IF is_cons(x180) THEN car(x180) ELSE leaf(zero) ENDIF)) IN + (IF is_node(x179) THEN children(x179) ELSE null ENDIF)) IN + (IF is_cons(x178) THEN cdr(x178) ELSE null ENDIF))))) IN + (IF is_cons(x162) THEN cdr(x162) ELSE null ENDIF)) IN + (IF is_cons(x161) THEN cdr(x161) ELSE null ENDIF)) IN + (IF is_cons(x160) THEN car(x160) ELSE leaf(zero) ENDIF)) IN + (IF is_node(x159) THEN children(x159) ELSE null ENDIF)) IN + (IF is_cons(x158) THEN cdr(x158) ELSE null ENDIF)) IN + (IF is_cons(x157) THEN cdr(x157) ELSE null ENDIF)) IN + (IF is_cons(x156) THEN cdr(x156) ELSE null ENDIF))) IN + (IF is_leaf(x155) THEN data(x155) ELSE zero ENDIF)) IN + (IF is_succ(x154) THEN pred(x154) ELSE zero ENDIF)))); diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index bc49a7fac..646ebf9bb 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -33,6 +33,7 @@ UNIT_TESTS = \ context/cdvector_black \ util/assert_white \ util/bitvector_black \ + util/datatype_black \ util/configuration_black \ util/congruence_closure_white \ util/output_black \ diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index 14fb3406a..a56f05c0f 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -5,13 +5,13 @@ ** Major contributors: mdeters ** 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 ** information.\endverbatim ** - ** \brief Black box testing of CVC4::BitVector. + ** \brief Black box testing of CVC4::BitVector ** ** Black box testing of CVC4::BitVector. **/ diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h new file mode 100644 index 000000000..d0de68e33 --- /dev/null +++ b/test/unit/util/datatype_black.h @@ -0,0 +1,156 @@ +/********************* */ +/*! \file datatype_black.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::Datatype + ** + ** Black box testing of CVC4::Datatype. + **/ + +#include <cxxtest/TestSuite.h> +#include <sstream> + +#include "util/datatype.h" + +#include "expr/expr.h" +#include "expr/expr_manager.h" + +using namespace CVC4; +using namespace std; + +class DatatypeBlack : public CxxTest::TestSuite { + + ExprManager* d_em; + +public: + + void setUp() { + d_em = new ExprManager(); + } + + void tearDown() { + delete d_em; + } + + void testNat() { + Datatype nat("nat"); + + Datatype::Constructor succ("succ", "is_succ"); + succ.addArg("pred", Datatype::SelfType()); + nat.addConstructor(succ); + + Datatype::Constructor zero("zero", "is_zero"); + nat.addConstructor(zero); + + cout << nat << std::endl; + DatatypeType natType = d_em->mkDatatypeType(nat); + cout << natType << std::endl; + } + + void testTree() { + Datatype tree("tree"); + Type integerType = d_em->integerType(); + + Datatype::Constructor node("node", "is_node"); + node.addArg("left", Datatype::SelfType()); + node.addArg("right", Datatype::SelfType()); + tree.addConstructor(node); + + Datatype::Constructor leaf("leaf", "is_leaf"); + leaf.addArg("leaf", integerType); + tree.addConstructor(leaf); + + cout << tree << std::endl; + DatatypeType treeType = d_em->mkDatatypeType(tree); + cout << treeType << std::endl; + } + + void testList() { + Datatype list("list"); + Type integerType = d_em->integerType(); + + Datatype::Constructor cons("cons", "is_cons"); + cons.addArg("car", integerType); + cons.addArg("cdr", Datatype::SelfType()); + list.addConstructor(cons); + + Datatype::Constructor nil("nil", "is_nil"); + list.addConstructor(nil); + + cout << list << std::endl; + DatatypeType listType = d_em->mkDatatypeType(list); + cout << listType << std::endl; + } + + void testMutualListTrees() { + /* Create two mutual datatypes corresponding to this definition + * block: + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(list), + * list = cons(car: tree, cdr: list) | nil + * END; + */ + Datatype tree("tree"); + Datatype::Constructor node("node", "is_node"); + node.addArg("left", Datatype::SelfType()); + node.addArg("right", Datatype::SelfType()); + tree.addConstructor(node); + + Datatype::Constructor leaf("leaf", "is_leaf"); + leaf.addArg("leaf", Datatype::UnresolvedType("list")); + tree.addConstructor(leaf); + + cout << tree << std::endl; + + Datatype list("list"); + Datatype::Constructor cons("cons", "is_cons"); + cons.addArg("car", Datatype::UnresolvedType("tree")); + cons.addArg("cdr", Datatype::SelfType()); + list.addConstructor(cons); + + Datatype::Constructor nil("nil", "is_nil"); + list.addConstructor(nil); + + cout << list << std::endl; + + TS_ASSERT(! tree.isResolved()); + TS_ASSERT(! node.isResolved()); + TS_ASSERT(! leaf.isResolved()); + TS_ASSERT(! list.isResolved()); + TS_ASSERT(! cons.isResolved()); + TS_ASSERT(! nil.isResolved()); + + vector<Datatype> dts; + dts.push_back(tree); + dts.push_back(list); + vector<DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dts); + + TS_ASSERT(dtts[0].getDatatype().isResolved()); + TS_ASSERT(dtts[1].getDatatype().isResolved()); + + // add another constructor to list datatype resulting in an + // "otherNil-list" + Datatype::Constructor otherNil("otherNil", "is_otherNil"); + dts[1].addConstructor(otherNil); + + // remake the types + vector<DatatypeType> dtts2 = d_em->mkMutualDatatypeTypes(dts); + + TS_ASSERT_DIFFERS(dtts, dtts2); + TS_ASSERT_DIFFERS(dtts[1], dtts2[1]); + + // tree is also different because it's a tree of otherNil-lists + TS_ASSERT_DIFFERS(dtts[0], dtts2[0]); + } + +};/* class DatatypeBlack */ |