diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 11 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 9 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 5 | ||||
-rw-r--r-- | src/expr/node_manager.h | 22 | ||||
-rw-r--r-- | src/expr/type.cpp | 30 | ||||
-rw-r--r-- | src/expr/type.h | 27 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 10 | ||||
-rw-r--r-- | src/expr/type_node.h | 12 |
9 files changed, 117 insertions, 11 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8b61e92d3..99662cb99 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -960,7 +960,7 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() { d_commandStatus = new CommandFailure(e.what()); } */ - d_commandStatus = new CommandFailure("unsat cores not supported yet"); + d_commandStatus = new CommandUnsupported(); } void GetUnsatCoreCommand::printResult(std::ostream& out) const throw() { diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5e1ec0221..516930bcd 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -507,7 +507,7 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { NodeManagerScope nms(d_nodeManager); - Assert( types.size() >= 2 ); + Assert( types.size() >= 1 ); std::vector<TypeNode> typeNodes; for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { typeNodes.push_back(*types[i].d_typeNode); @@ -515,6 +515,15 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); } +SExprType ExprManager::mkSExprType(const std::vector<Type>& types) { + NodeManagerScope nms(d_nodeManager); + std::vector<TypeNode> typeNodes; + for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { + typeNodes.push_back(*types[i].d_typeNode); + } + return SExprType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSExprType(typeNodes)))); +} + BitVectorType ExprManager::mkBitVectorType(unsigned size) const { NodeManagerScope nms(d_nodeManager); return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index e20edfb42..460e3f1dc 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -345,10 +345,17 @@ public: /** * Make a tuple type with types from * <code>types[0..types.size()-1]</code>. <code>types</code> must - * have at least 2 elements. + * have at least one element. */ TupleType mkTupleType(const std::vector<Type>& types); + /** + * Make a symbolic expressiontype with types from + * <code>types[0..types.size()-1]</code>. <code>types</code> may + * have any number of elements. + */ + SExprType mkSExprType(const std::vector<Type>& types); + /** Make a type representing a bit-vector of the given size. */ BitVectorType mkBitVectorType(unsigned size) const; diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 647c1af8e..4582bfeda 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -302,11 +302,6 @@ function register_metakind { exit 1 fi - if [ $mk = OPERATOR -a $lb = 0 ]; then - echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2 - exit 1 - fi - metakind_lbchildren="${metakind_lbchildren} $lb, /* $k */" metakind_ubchildren="${metakind_ubchildren} diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 4a05b174d..8e61415e8 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -711,14 +711,24 @@ public: /** * Make a tuple type with types from - * <code>types</code>. <code>types</code> must have at least two - * elements. + * <code>types</code>. <code>types</code> must have at least one + * element. * * @param types a vector of types * @returns the tuple type (types[0], ..., types[n]) */ inline TypeNode mkTupleType(const std::vector<TypeNode>& types); + /** + * Make a symbolic expression type with types from + * <code>types</code>. <code>types</code> may have any number of + * elements. + * + * @param types a vector of types + * @returns the symbolic expression type (types[0], ..., types[n]) + */ + inline TypeNode mkSExprType(const std::vector<TypeNode>& types); + /** Make the type of bitvectors of size <code>size</code> */ inline TypeNode mkBitVectorType(unsigned size); @@ -1060,6 +1070,14 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { return mkTypeNode(kind::TUPLE_TYPE, typeNodes); } +inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) { + std::vector<TypeNode> typeNodes; + for (unsigned i = 0; i < types.size(); ++ i) { + typeNodes.push_back(types[i]); + } + return mkTypeNode(kind::SEXPR_TYPE, typeNodes); +} + inline TypeNode NodeManager::mkBitVectorType(unsigned size) { return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size))); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index b55d33dcf..5a00a538c 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -347,6 +347,19 @@ Type::operator TupleType() const throw(AssertionException) { return TupleType(*this); } +/** Is this a symbolic expression type? */ +bool Type::isSExpr() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isSExpr(); +} + +/** Cast to a symbolic expression type */ +Type::operator SExprType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isNull() || isSExpr()); + return SExprType(*this); +} + /** Is this an array type? */ bool Type::isArray() const { NodeManagerScope nms(d_nodeManager); @@ -441,6 +454,18 @@ vector<Type> TupleType::getTypes() const { return types; } +vector<Type> SExprType::getTypes() const { + NodeManagerScope nms(d_nodeManager); + vector<Type> types; + vector<TypeNode> typeNodes = d_typeNode->getSExprTypes(); + vector<TypeNode>::iterator it = typeNodes.begin(); + vector<TypeNode>::iterator it_end = typeNodes.end(); + for(; it != it_end; ++ it) { + types.push_back(makeType(*it)); + } + return types; +} + string SortType::getName() const { NodeManagerScope nms(d_nodeManager); return d_typeNode->getAttribute(expr::VarNameAttr()); @@ -533,6 +558,11 @@ TupleType::TupleType(const Type& t) throw(AssertionException) : Assert(isNull() || isTuple()); } +SExprType::SExprType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isNull() || isSExpr()); +} + ArrayType::ArrayType(const Type& t) throw(AssertionException) : Type(t) { Assert(isNull() || isArray()); diff --git a/src/expr/type.h b/src/expr/type.h index 513a4d60a..caaf256f5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -57,6 +57,7 @@ class SelectorType; class TesterType; class FunctionType; class TupleType; +class SExprType; class SortType; class SortConstructorType; class PredicateSubtype; @@ -319,6 +320,18 @@ public: operator TupleType() const throw(AssertionException); /** + * Is this a symbolic expression type? + * @return true if the type is a symbolic expression type + */ + bool isSExpr() const; + + /** + * Cast this type to a symbolic expression type + * @return the SExprType + */ + operator SExprType() const throw(AssertionException); + + /** * Is this an array type? * @return true if the type is a array type */ @@ -514,6 +527,20 @@ public: };/* class TupleType */ /** + * Class encapsulating a tuple type. + */ +class CVC4_PUBLIC SExprType : public Type { + +public: + + /** Construct from the base type */ + SExprType(const Type& type = Type()) throw(AssertionException); + + /** Get the constituent types */ + std::vector<Type> getTypes() const; +};/* class SExprType */ + +/** * Class encapsulating an array type. */ class CVC4_PUBLIC ArrayType : public Type { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index e35d55e28..2676fd6b2 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -144,7 +144,6 @@ std::vector<TypeNode> TypeNode::getParamTypes() const { return params; } -/** Is this a tuple type? */ vector<TypeNode> TypeNode::getTupleTypes() const { Assert(isTuple()); vector<TypeNode> types; @@ -154,6 +153,15 @@ vector<TypeNode> TypeNode::getTupleTypes() const { return types; } +vector<TypeNode> TypeNode::getSExprTypes() const { + Assert(isSExpr()); + vector<TypeNode> types; + for(unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) { + types.push_back((*this)[i]); + } + return types; +} + /** Is this an instantiated datatype type */ bool TypeNode::isInstantiatedDatatype() const { if(getKind() == kind::DATATYPE_TYPE) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index af0734575..a0397e0bd 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -541,6 +541,12 @@ public: /** Get the constituent types of a tuple type */ std::vector<TypeNode> getTupleTypes() const; + /** Is this a symbolic expression type? */ + bool isSExpr() const; + + /** Get the constituent types of a symbolic expression type */ + std::vector<TypeNode> getSExprTypes() const; + /** Is this a bit-vector type */ bool isBitVector() const; @@ -873,6 +879,12 @@ inline bool TypeNode::isTuple() const { ( isPredicateSubtype() && getSubtypeBaseType().isTuple() ); } +/** Is this a symbolic expression type? */ +inline bool TypeNode::isSExpr() const { + return getKind() == kind::SEXPR_TYPE || + ( isPredicateSubtype() && getSubtypeBaseType().isSExpr() ); +} + /** Is this a sort kind */ inline bool TypeNode::isSort() const { return ( getKind() == kind::SORT_TYPE && !hasAttribute(expr::SortArityAttr()) ) || |