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/theory/builtin | |
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/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 10 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 66 |
2 files changed, 75 insertions, 1 deletions
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: |