diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-26 03:07:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-26 03:07:01 +0000 |
commit | 7f84ff856af53047c2af2c1c1987340f9075ec7c (patch) | |
tree | 6e49732af41fccb76edbc004f6e62f1751cebc64 /src/expr/expr_manager_template.cpp | |
parent | 60c0b1855d20aeb67ac16312bb4dd00664e28f8f (diff) |
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.)
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
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)))); |