diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-10-06 08:31:35 +0000 |
| commit | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (patch) | |
| tree | 4ff6643e38469ceb84cd6791c5cbc295f625a735 /src/theory/builtin/kinds | |
| parent | 4c9f8d2b58d274e5bfea5fa28b02f005af71ef39 (diff) | |
declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)
Diffstat (limited to 'src/theory/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index d3b9d12fb..47ee8cbfc 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -112,8 +112,14 @@ theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h" # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's # not stored that way. If you ask for the operator of (EQUAL a b), # you'll get a special, singleton (BUILTIN EQUAL) Node. -constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \ - "expr/kind.h" "The kind of nodes representing built-in operators" +constant BUILTIN \ + ::CVC4::Kind \ + ::CVC4::kind::KindHashStrategy \ + "expr/kind.h" \ + "The kind of nodes representing built-in operators" + +variable FUNCTION "function" +parameterized APPLY FUNCTION 1: "defined function application" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" |