* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)
* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).
* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)
(this commit was certified error- and warning-free by the test-and-commit script.)
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() {
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);
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))));
/**
* 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;
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}
/**
* 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);
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)));
}
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);
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());
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());
class TesterType;
class FunctionType;
class TupleType;
+class SExprType;
class SortType;
class SortConstructorType;
class PredicateSubtype;
*/
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
std::vector<Type> getTypes() const;
};/* 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.
*/
return params;
}
-/** Is this a tuple type? */
vector<TypeNode> TypeNode::getTupleTypes() const {
Assert(isTuple());
vector<TypeNode> types;
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) {
/** 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;
( 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()) ) ||
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;
}
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)
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");
}
}
variable BOUND_VARIABLE "bound variable"
variable SKOLEM "skolem var"
operator TUPLE 1: "a tuple"
+operator SEXPR 0: "a symbolic expression"
operator LAMBDA 2 "lambda"
"::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.
#
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
}
};/* class DistinctTypeRule */
-
class TupleTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
}
};/* 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) {
}
};/* 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:
projects / cvc5.git / commitdiff