From 7f84ff856af53047c2af2c1c1987340f9075ec7c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 26 Sep 2012 03:07:01 +0000 Subject: [PATCH] The Tuesday Afternoon Catch-All Commit (TACAC): * --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.) --- src/expr/command.cpp | 2 +- src/expr/expr_manager_template.cpp | 11 +++- src/expr/expr_manager_template.h | 9 ++- src/expr/mkmetakind | 5 -- src/expr/node_manager.h | 22 ++++++- src/expr/type.cpp | 30 +++++++++ src/expr/type.h | 27 ++++++++ src/expr/type_node.cpp | 10 ++- src/expr/type_node.h | 12 ++++ src/main/driver_unified.cpp | 11 ++++ src/main/options | 3 + src/smt/options_handlers.h | 2 +- src/theory/builtin/kinds | 10 +++ .../builtin/theory_builtin_type_rules.h | 66 ++++++++++++++++++- 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& sorts) { TupleType ExprManager::mkTupleType(const std::vector& types) { NodeManagerScope nms(d_nodeManager); - Assert( types.size() >= 2 ); + Assert( types.size() >= 1 ); std::vector 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& types) { return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); } +SExprType ExprManager::mkSExprType(const std::vector& types) { + NodeManagerScope nms(d_nodeManager); + std::vector 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 * types[0..types.size()-1]. types must - * have at least 2 elements. + * have at least one element. */ TupleType mkTupleType(const std::vector& types); + /** + * Make a symbolic expressiontype with types from + * types[0..types.size()-1]. types may + * have any number of elements. + */ + SExprType mkSExprType(const std::vector& 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 - * types. types must have at least two - * elements. + * types. types 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& types); + /** + * Make a symbolic expression type with types from + * types. types 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& types); + /** Make the type of bitvectors of size size */ inline TypeNode mkBitVectorType(unsigned size); @@ -1060,6 +1070,14 @@ inline TypeNode NodeManager::mkTupleType(const std::vector& types) { return mkTypeNode(kind::TUPLE_TYPE, typeNodes); } +inline TypeNode NodeManager::mkSExprType(const std::vector& types) { + std::vector 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(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 TupleType::getTypes() const { return types; } +vector SExprType::getTypes() const { + NodeManagerScope nms(d_nodeManager); + vector types; + vector typeNodes = d_typeNode->getSExprTypes(); + vector::iterator it = typeNodes.begin(); + vector::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; @@ -318,6 +319,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 @@ -513,6 +526,20 @@ public: std::vector 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 getTypes() const; +};/* class SExprType */ + /** * Class encapsulating an array 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::getParamTypes() const { return params; } -/** Is this a tuple type? */ vector TypeNode::getTupleTypes() const { Assert(isTuple()); vector types; @@ -154,6 +153,15 @@ vector TypeNode::getTupleTypes() const { return types; } +vector TypeNode::getSExprTypes() const { + Assert(isSExpr()); + vector 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 getTupleTypes() const; + /** Is this a symbolic expression type? */ + bool isSExpr() const; + + /** Get the constituent types of a symbolic expression type */ + std::vector 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 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 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: -- 2.30.2