From 86df00c36c6cbabac53001082219c3fc8c0fa297 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 24 Sep 2012 20:55:58 +0000 Subject: [PATCH] some api changes --- src/expr/expr_manager_template.cpp | 5 ----- src/expr/expr_manager_template.h | 3 --- src/expr/expr_template.cpp | 4 ---- src/expr/expr_template.h | 16 +++++-------- src/expr/node_manager.h | 8 ------- src/expr/type.cpp | 18 --------------- src/expr/type.h | 24 -------------------- src/expr/type_checker_template.cpp | 7 ++---- src/expr/type_node.h | 10 --------- src/printer/cvc/cvc_printer.cpp | 3 --- src/smt/smt_engine.cpp | 2 +- src/smt/smt_engine.h | 5 ++++- src/theory/builtin/kinds | 7 ------ test/regress/regress0/datatypes/Makefile.am | 4 ++-- test/unit/expr/node_manager_black.h | 25 --------------------- 15 files changed, 14 insertions(+), 127 deletions(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 18b7bff0f..5e1ec0221 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -140,11 +140,6 @@ StringType ExprManager::stringType() const { return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->stringType()))); } -KindType ExprManager::kindType() const { - NodeManagerScope nms(d_nodeManager); - return KindType(Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()))); -} - RealType ExprManager::realType() const { NodeManagerScope nms(d_nodeManager); return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType()))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 8c964a5eb..e20edfb42 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -133,9 +133,6 @@ public: /** Get the type for strings. */ StringType stringType() const; - /** Get the type for sorts. */ - KindType kindType() const; - /** Get the type for reals. */ RealType realType() const; diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index c607ca0a7..5070c852f 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -436,10 +436,6 @@ bool Expr::isNull() const { return d_node->isNull(); } -Expr::operator bool() const { - return !isNull(); -} - bool Expr::isVariable() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index e26e99ded..96c7cfadf 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -148,12 +148,15 @@ struct ExprHashFunction { size_t operator()(CVC4::Expr e) const; };/* struct ExprHashFunction */ +class BoolExpr; + /** * Class encapsulating CVC4 expressions and methods for constructing new * expressions. */ class CVC4_PUBLIC Expr { -protected: + + friend class BoolExpr; /** The internal expression representation */ NodeTemplate* d_node; @@ -416,13 +419,6 @@ public: */ bool isNull() const; - /** - * Check if this is a null expression. - * - * @return true if NOT a null expression - */ - operator bool() const; - /** * Check if this is an expression representing a variable. * @@ -526,8 +522,6 @@ private: */ void debugPrint(); -protected: - /** * Returns the actual internal node. * @return the internal node @@ -961,7 +955,7 @@ public: ${getConst_instantiations} -#line 965 "${template}" +#line 959 "${template}" namespace expr { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 893fde64b..4a05b174d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -658,9 +658,6 @@ public: /** Get the (singleton) type for strings. */ inline TypeNode stringType(); - /** Get the (singleton) type for sorts. */ - inline TypeNode kindType(); - /** Get the bound var list type. */ inline TypeNode boundVarListType(); @@ -983,11 +980,6 @@ inline TypeNode NodeManager::stringType() { return TypeNode(mkTypeConst(STRING_TYPE)); } -/** Get the (singleton) type for sorts. */ -inline TypeNode NodeManager::kindType() { - return TypeNode(mkTypeConst(KIND_TYPE)); -} - /** Get the bound var list type. */ inline TypeNode NodeManager::boundVarListType() { return TypeNode(mkTypeConst(BOUND_VAR_LIST_TYPE)); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index d67aa1fe3..b55d33dcf 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -411,19 +411,6 @@ Type::operator SubrangeType() const throw(AssertionException) { return SubrangeType(*this); } -/** Is this a kind type (i.e., the type of a type)? */ -bool Type::isKind() const { - NodeManagerScope nms(d_nodeManager); - return d_typeNode->isKind(); -} - -/** Cast to a kind type */ -Type::operator KindType() const throw(AssertionException) { - NodeManagerScope nms(d_nodeManager); - Assert(isNull() || isKind()); - return KindType(*this); -} - vector FunctionType::getArgTypes() const { NodeManagerScope nms(d_nodeManager); vector args; @@ -551,11 +538,6 @@ ArrayType::ArrayType(const Type& t) throw(AssertionException) : Assert(isNull() || isArray()); } -KindType::KindType(const Type& t) throw(AssertionException) : - Type(t) { - Assert(isNull() || isKind()); -} - SortType::SortType(const Type& t) throw(AssertionException) : Type(t) { Assert(isNull() || isSort()); diff --git a/src/expr/type.h b/src/expr/type.h index 29b0ac128..513a4d60a 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -57,7 +57,6 @@ class SelectorType; class TesterType; class FunctionType; class TupleType; -class KindType; class SortType; class SortConstructorType; class PredicateSubtype; @@ -427,18 +426,6 @@ public: */ operator SubrangeType() const throw(AssertionException); - /** - * Is this a kind type (i.e., the type of a type)? - * @return true if this is a kind type - */ - bool isKind() const; - - /** - * Cast to a kind type - * @return the kind type - */ - operator KindType() const throw(AssertionException); - /** * Outputs a string representation of this type to the stream. * @param out the stream to output to @@ -618,17 +605,6 @@ public: };/* class SubrangeType */ -/** - * Class encapsulating the kind type (the type of types). - */ -class CVC4_PUBLIC KindType : public Type { - -public: - - /** Construct from the base type */ - KindType(const Type& type = Type()) throw(AssertionException); -};/* class KindType */ - /** * Class encapsulating the bit-vector type. */ diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index d559477f1..450baf505 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -41,13 +41,10 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) case kind::BUILTIN: typeNode = nodeManager->builtinOperatorType(); break; - case kind::SORT_TYPE: - typeNode = nodeManager->kindType(); - break; ${typerules} -#line 51 "${template}" +#line 48 "${template}" default: Debug("getType") << "FAILURE" << std::endl; @@ -70,7 +67,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) switch(n.getKind()) { ${construles} -#line 74 "${template}" +#line 71 "${template}" default:; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index e848cf9a9..af0734575 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -592,10 +592,6 @@ public: /** Get the bounds defining this subrange */ const SubrangeBounds& getSubrangeBounds() const; - /** Is this a kind type (i.e., the type of a type)? */ - bool isKind() const; - - /** * Returns the leastUpperBound in the extended type lattice of the two types. * If this is \top, i.e. there is no inhabited type that contains both, @@ -899,12 +895,6 @@ inline bool TypeNode::isSubrange() const { ( isPredicateSubtype() && getSubtypeBaseType().isSubrange() ); } -/** Is this a kind type (i.e., the type of a type)? */ -inline bool TypeNode::isKind() const { - return getKind() == kind::TYPE_CONSTANT && - getConst() == KIND_TYPE; -} - /** Is this a bit-vector type */ inline bool TypeNode::isBitVector() const { return getKind() == kind::BITVECTOR_TYPE || diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 35a85e681..a6693dd22 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -150,9 +150,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo case BOOLEAN_TYPE: out << "BOOLEAN"; break; - case KIND_TYPE: - out << "TYPE"; - break; default: out << tc; break; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6e8cc9b5d..cedd866f9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1888,7 +1888,7 @@ Expr SmtEngine::getValue(const Expr& e) "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response."; throw ModalException(msg); } - if(type.isKind() || type.isSortConstructor()) { + if(type.isSort() || type.isSortConstructor()) { const char* msg = "Cannot get value of a sort."; throw ModalException(msg); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index cbb97f9f7..0214cddd3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -559,7 +559,10 @@ public: */ SExpr getStatistic(std::string name) const throw(); - Result getStatusOfLastCommand() const { + /** + * Returns the most recent result of checkSat/query or (set-info :status). + */ + Result getStatusOfLastCommand() const throw() { return d_status; } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index da31d157f..8eff22ed4 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -251,13 +251,6 @@ sort BUILTIN_OPERATOR_TYPE \ not-well-founded \ "Built in type for built in operators" -# Justified because we can have an unbounded-but-finite number of -# sorts. Assuming we have |Z| is probably ok for now.. -sort KIND_TYPE \ - Cardinality::INTEGERS \ - not-well-founded \ - "Uninterpreted Sort" - variable SORT_TAG "sort tag" parameterized SORT_TYPE SORT_TAG 0: "sort type" # This is really "unknown" cardinality, but maybe this will be good diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 2ec558f20..aca663e18 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -40,10 +40,10 @@ TESTS = \ v3l60006.cvc \ v5l30058.cvc \ bug286.cvc \ - wrong-sel-simp.cvc + wrong-sel-simp.cvc \ + rec2.cvc FAILING_TESTS = \ - rec2.cvc \ rec5.cvc \ datatype-dump.cvc diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 75c3618ff..18dc96c98 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -180,7 +180,6 @@ public: TypeNode t3 = d_nodeManager->mkSort("T"); TS_ASSERT( t.isBoolean() ); TS_ASSERT( !t.isFunction() ); - TS_ASSERT( !t.isKind() ); TS_ASSERT( !t.isNull() ); TS_ASSERT( !t.isPredicate() ); TS_ASSERT( !t.isSort() ); @@ -191,26 +190,6 @@ public: TS_ASSERT_EQUALS( bt, t); } - void testKindType() { - TypeNode t = d_nodeManager->kindType(); - TypeNode t2 = d_nodeManager->kindType(); - TypeNode t3 = d_nodeManager->mkSort("T"); - - TS_ASSERT( !t.isBoolean() ); - TS_ASSERT( !t.isFunction() ); - TS_ASSERT( t.isKind() ); - TS_ASSERT( !t.isNull() ); - TS_ASSERT( !t.isPredicate() ); - TS_ASSERT( !t.isSort() ); - - TS_ASSERT_EQUALS(t, t2); - TS_ASSERT( t != t3); - - TypeNode kt = t; - TS_ASSERT_EQUALS( kt, t ); - // TODO: Is there a way to get the type of otherType (it should == t)? - } - void testMkFunctionTypeBoolToBool() { TypeNode booleanType = d_nodeManager->booleanType(); TypeNode t = d_nodeManager->mkFunctionType(booleanType,booleanType); @@ -218,7 +197,6 @@ public: TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); - TS_ASSERT( !t.isKind() ); TS_ASSERT( !t.isNull() ); TS_ASSERT( t.isPredicate() ); TS_ASSERT( !t.isSort() ); @@ -247,7 +225,6 @@ public: TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); - TS_ASSERT( !t.isKind() ); TS_ASSERT( !t.isNull() ); TS_ASSERT( !t.isPredicate() ); TS_ASSERT( !t.isSort() ); @@ -278,7 +255,6 @@ public: TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); - TS_ASSERT( !t.isKind() ); TS_ASSERT( !t.isNull() ); TS_ASSERT( !t.isPredicate() ); TS_ASSERT( !t.isSort() ); @@ -309,7 +285,6 @@ public: TS_ASSERT( !t.isBoolean() ); TS_ASSERT( t.isFunction() ); - TS_ASSERT( !t.isKind() ); TS_ASSERT( !t.isNull() ); TS_ASSERT( t.isPredicate() ); TS_ASSERT( !t.isSort() ); -- 2.30.2