summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/command.cpp2
-rw-r--r--src/expr/expr_manager_template.cpp11
-rw-r--r--src/expr/expr_manager_template.h9
-rwxr-xr-xsrc/expr/mkmetakind5
-rw-r--r--src/expr/node_manager.h22
-rw-r--r--src/expr/type.cpp30
-rw-r--r--src/expr/type.h27
-rw-r--r--src/expr/type_node.cpp10
-rw-r--r--src/expr/type_node.h12
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()) ) ||
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback