summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--src/main/driver_unified.cpp11
-rw-r--r--src/main/options3
-rw-r--r--src/smt/options_handlers.h2
-rw-r--r--src/theory/builtin/kinds10
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h66
14 files changed, 207 insertions, 13 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()) ) ||
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 4ac137ef1..20b4c2bc2 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -314,5 +314,16 @@ int runCvc4(int argc, char* argv[], Options& opts) {
if(opts[options::statistics]) {
cmdExecutor.flushStatistics(*opts[options::err]);
}
+
+#ifdef CVC4_DEBUG
+ if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
+ _exit(returnValue);
+ }
+#else /* CVC4_DEBUG */
+ if(opts[options::earlyExit]) {
+ _exit(returnValue);
+ }
+#endif /* CVC4_DEBUG */
+
return returnValue;
}
diff --git a/src/main/options b/src/main/options
index 47d8da598..58ea5e544 100644
--- a/src/main/options
+++ b/src/main/options
@@ -19,6 +19,9 @@ option - --show-debug-tags void :handler CVC4::main::showDebugTags :handler-incl
option - --show-trace-tags void :handler CVC4::main::showTraceTags :handler-include "main/options_handlers.h"
show all available tags for tracing
+expert-option earlyExit --early-exit bool :default true
+ do not run destructors at exit; default on except in debug mode
+
# portfolio options
option printWinner bool
enable printing the winning thread (pcvc4 only)
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 4f214ddd1..7d5dd56c9 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -288,7 +288,7 @@ inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) th
inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
if(value) {
- throw OptionException("CVC4 does not yet have support for unsatisfiable cores");
+ throw UnrecognizedOptionException("CVC4 does not yet have support for unsatisfiable cores");
}
}
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 8eff22ed4..86efac2f0 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -290,6 +290,7 @@ variable VARIABLE "variable"
variable BOUND_VARIABLE "bound variable"
variable SKOLEM "skolem var"
operator TUPLE 1: "a tuple"
+operator SEXPR 0: "a symbolic expression"
operator LAMBDA 2 "lambda"
@@ -313,6 +314,14 @@ well-founded TUPLE_TYPE \
"::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
"::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
"theory/builtin/theory_builtin_type_rules.h"
+operator SEXPR_TYPE 0: "symbolic expression type"
+cardinality SEXPR_TYPE \
+ "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
+well-founded SEXPR_TYPE \
+ "::CVC4::theory::builtin::SExprProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \
+ "theory/builtin/theory_builtin_type_rules.h"
# These will eventually move to a theory of strings.
#
@@ -335,6 +344,7 @@ typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
+typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 97af23f67..939c52f31 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -117,7 +117,6 @@ public:
}
};/* class DistinctTypeRule */
-
class TupleTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
@@ -131,6 +130,19 @@ public:
}
};/* class TupleTypeRule */
+class SExprTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+ std::vector<TypeNode> types;
+ for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
+ child_it != child_it_end;
+ ++child_it) {
+ types.push_back((*child_it).getType(check));
+ }
+ return nodeManager->mkSExprType(types);
+ }
+};/* class SExprTypeRule */
+
class UninterpretedConstantTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
@@ -300,6 +312,58 @@ public:
}
};/* class TupleProperties */
+class SExprProperties {
+public:
+ inline static Cardinality computeCardinality(TypeNode type) {
+ // Don't assert this; allow other theories to use this cardinality
+ // computation.
+ //
+ // Assert(type.getKind() == kind::SEXPR_TYPE);
+
+ Cardinality card(1);
+ for(TypeNode::iterator i = type.begin(),
+ i_end = type.end();
+ i != i_end;
+ ++i) {
+ card *= (*i).getCardinality();
+ }
+
+ return card;
+ }
+
+ inline static bool isWellFounded(TypeNode type) {
+ // Don't assert this; allow other theories to use this
+ // wellfoundedness computation.
+ //
+ // Assert(type.getKind() == kind::SEXPR_TYPE);
+
+ for(TypeNode::iterator i = type.begin(),
+ i_end = type.end();
+ i != i_end;
+ ++i) {
+ if(! (*i).isWellFounded()) {
+ return false;
+ }
+ }
+
+ return true;
+ }
+
+ inline static Node mkGroundTerm(TypeNode type) {
+ Assert(type.getKind() == kind::SEXPR_TYPE);
+
+ std::vector<Node> children;
+ for(TypeNode::iterator i = type.begin(),
+ i_end = type.end();
+ i != i_end;
+ ++i) {
+ children.push_back((*i).mkGroundTerm());
+ }
+
+ return NodeManager::currentNM()->mkNode(kind::SEXPR, children);
+ }
+};/* class SExprProperties */
+
class SubtypeProperties {
public:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback