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/uf | |
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/uf')
-rw-r--r-- | src/theory/uf/kinds | 13 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 9 |
2 files changed, 19 insertions, 3 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index a1fcac1df..d7f542038 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -6,15 +6,22 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" -properties stable-infinite check propagate staticLearning presolve +properties stable-infinite +properties check propagate staticLearning presolve notifyRestart rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" -sort KIND_TYPE "Uninterpreted Sort" +# Justified because we can have an unbounded-but-finite number of +# sorts. Assuming we have |Z| is probably ok for now.. +sort KIND_TYPE Cardinality::INTEGERS "Uninterpreted Sort" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" variable SORT_TAG "sort tag" parameterized SORT_TYPE SORT_TAG 0: "sort type" +# This is really "unknown" cardinality, but maybe this will be good +# enough (for now) ? Once we support quantifiers, maybe reconsider +# this.. +cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)" -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 9746b38ab..34d6df881 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -40,6 +40,15 @@ public: TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation) : Theory(THEORY_UF, ctxt, out, valuation) { } + // We declare these here (even though it's not terribly useful) for + // documentation reasons, and to keep mktheorytraits from issuing a + // spurious warning. + virtual void check(Effort) = 0; + virtual void propagate(Effort) {} + virtual void staticLearning(TNode in, NodeBuilder<>& learned) {} + virtual void notifyRestart() {} + virtual void presolve() {} + };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |