diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
| commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
| tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src/theory/uf/kinds | |
| parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) | |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 8cd6aec70..a1fcac1df 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -4,9 +4,17 @@ # src/theory/builtin/kinds. # -theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" +theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" + +properties stable-infinite check propagate staticLearning presolve + +rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" + +sort KIND_TYPE "Uninterpreted Sort" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" variable SORT_TAG "sort tag" parameterized SORT_TYPE SORT_TAG 0: "sort type" + +endtheory
\ No newline at end of file |