From cb7363eef352200615e1a0d3729cea8b2c74d265 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 25 Apr 2011 06:56:14 +0000 Subject: 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 --- src/expr/expr_template.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/expr/expr_template.h') diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 24cb6dc5d..43d40105e 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -758,7 +758,7 @@ public: ${getConst_instantiations} -#line 758 "${template}" +#line 762 "${template}" namespace expr { -- cgit v1.2.3