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/expr/Makefile.am | |
| 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/expr/Makefile.am')
| -rw-r--r-- | src/expr/Makefile.am | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 1d7af717b..4ed5a3ac7 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -31,6 +31,7 @@ libexpr_la_SOURCES = \ nodist_libexpr_la_SOURCES = \ kind.h \ metakind.h \ + type_properties.h \ expr.h \ expr.cpp \ expr_manager.h \ @@ -39,6 +40,7 @@ nodist_libexpr_la_SOURCES = \ EXTRA_DIST = \ kind_template.h \ metakind_template.h \ + type_properties_template.h \ expr_manager_template.h \ expr_manager_template.cpp \ expr_template.h \ @@ -50,6 +52,7 @@ EXTRA_DIST = \ BUILT_SOURCES = \ kind.h \ metakind.h \ + type_properties.h \ expr.h \ expr.cpp \ expr_manager.h \ @@ -83,6 +86,14 @@ metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @t `cat @top_builddir@/src/theory/.subdirs` \ > $@) || (rm -f $@ && exit 1) +type_properties.h: type_properties_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkkind + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkkind \ + $< \ + `cat @top_builddir@/src/theory/.subdirs` \ + > $@) || (rm -f $@ && exit 1) + expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkexpr $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true |