diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-25 06:56:14 +0000 |
commit | cb7363eef352200615e1a0d3729cea8b2c74d265 (patch) | |
tree | d57f6a9cfab879c1027e7282f63d0fae14fc0153 /src/theory/builtin | |
parent | e39882bd8a308711135a1ff644293fd9c46e6433 (diff) |
Weekend work. The main points:
* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 114 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 33 |
2 files changed, 140 insertions, 7 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 2831161c3..a170ba145 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -6,12 +6,58 @@ # The first non-blank, non-comment line in this file must be a theory # declaration: # -# theory [builtin] T header +# theory ID T header # -# The special tag "builtin" declares that this is the builtin theory. -# There can be only one and it should be processed first. +# Thereafter, ID is bound to your theory. It becomes part of an +# enumeration that identifies all theories. If your theory has +# several, distinct implementations, they still all share a kinds +# file, a theory ID, all the defined kinds/operators/types for the +# theory, typechecker, etc. They should also share a base class +# (that's the T above). The header is the header for this base +# class. # -# There are four basic commands for declaring kinds: +# The very end of this file should end with: +# +# endtheory +# +# There are several basic commands: +# +# properties PROPERTIES... +# +# This command declares properties of the theory. It can occur +# more than once, in which case the effect is additive. +# +# The current set of properties and their meanings are: +# +# finite the theory is finite +# stable-infinite the theory is stably infinite +# polite the theory is polite +# +# check the theory supports the check() function +# propagate the theory supports propagate() (and explain()) +# staticLearning the theory supports staticLearning() +# registerTerm the theory supports registerTerm() +# notifyRestart the theory supports notifyRestart() +# presolve the theory supports presolve() +# +# In the case of the "theory-supports-function" properties, you +# need to declare these for your theory or the functions will not +# be called! This is used to speed up the core where functionality +# is not needed. +# +# rewriter T header +# +# This declares a rewriter class T for your theory, declared in +# header. Your rewriter class provides four functions: +# +# static void init(); +# static void shutdown(); +# static RewriteResponse preRewrite(TNode node); +# static RewriteResponse postRewrite(TNode node); +# +# ...BUT please note that init() and shutdown() may be removed in +# future, so if possible, do not rely on them being called (and +# implement them as a no-op). # # variable K ["comment"] # @@ -76,6 +122,54 @@ # For consistency, constants taking a non-void payload should # start with "CONST_", but this is not enforced. # +# sort K cardinality ["comment"] +# +# This creates a kind K that represents a sort (a "type constant"). +# These kinds of types are "atomic" types; if you need to describe +# a complex type that takes type arguments (like arrays), use +# "operator"; if you need to describe one that takes "constant" +# arguments (like bitvectors), use "constant", and if you invent +# one that takes both, you could try "parameterized". In those +# cases, you'll want to provide a cardinality separately for your +# type. +# +# The cardinality argument is a nonnegative number (if the sort is +# finite), or Cardinality::INTEGERS if the sort has the same +# cardinality as the integers, or Cardinality::REALS if the sort +# has the same cardinality as the reals. +# +# For consistency, sorts should end with "_TYPE", but this is not +# enforced. +# +# cardinality K cardinality-computer [header] +# +# This command does not define a kind; the kind K needs to be +# defined by one of the other commands above. This command just +# provides a cardinality for types of kind K. The +# "cardinality-computer" is a C++ expression that will yield a +# Cardinality for the type. In that expression, the sequence of +# characters "%TYPE%" will be rewritten with a variable containing +# a TypeNode of kind K. The optional "header" argument is an +# include file necessary to compile the cardinality-computer +# expression. +# +# If the cardinality need not be computed per-type (i.e., it's the +# same for all types of kind K, but the "sort" gesture above could +# not be used---in which case it doesn't already have a registered +# cardinality), you can simply construct a Cardinality temporary. +# For example: +# +# cardinality MY_TYPE Cardinality(Cardinality::INTEGERS) +# +# If not, you might opt to use a computer; a common place to put it +# is with your type checker: +# +# cardinality MY_TYPE \ +# ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \ +# "theory/foo/theory_foo_type_rules.h" +# +# +# # Lines may be broken with a backslash between arguments; for example: # # constant CONST_INT \ @@ -108,12 +202,12 @@ theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" -properties stable-infinite +properties stable-infinite # Rewriter responisble for all the terms of the theory rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h" -sort BUILTIN_OPERATOR_TYPE "Built in type for built in operators" +sort BUILTIN_OPERATOR_TYPE Cardinality::INTEGERS "Built in type for built in operators" # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's @@ -140,6 +234,12 @@ constant TYPE_CONSTANT \ "expr/kind.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" +cardinality FUNCTION_TYPE \ + "::CVC4::theory::builtin::FunctionCardinality::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" operator TUPLE_TYPE 2: "tuple type" +cardinality TUPLE_TYPE \ + "::CVC4::theory::builtin::TupleCardinality::computeCardinality(%TYPE%)" \ + "theory/builtin/theory_builtin_type_rules.h" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 0d313594c..bebfca9ab 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -128,6 +128,39 @@ public: } };/* class TupleTypeRule */ +class FunctionCardinality { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::FUNCTION_TYPE); + + Cardinality argsCard(1); + // get the largest cardinality of function arguments/return type + for(unsigned i = 0, i_end = type.getNumChildren() - 1; i < i_end; ++i) { + argsCard *= type[i].getCardinality(); + } + + Cardinality valueCard = type[type.getNumChildren() - 1].getCardinality(); + + return valueCard ^ argsCard; + } +};/* class FuctionCardinality */ + +class TupleCardinality { +public: + inline static Cardinality computeCardinality(TypeNode type) { + Assert(type.getKind() == kind::TUPLE_TYPE); + + Cardinality card(1); + for(TypeNode::iterator i = type.begin(), + i_end = type.end(); + i != i_end; + ++i) { + card *= (*i).getCardinality(); + } + + return card; + } +};/* class TupleCardinality */ }/* CVC4::theory::builtin namespace */ }/* CVC4::theory namespace */ |