new domain-specific language for kinds files: permits characterization of different...

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index 806f4f40255d6924ac7d625031cf36f91ab0466d..f687e3b819af2d8f8782fcbc493381caab193eb9 100644 (file)
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -1,5 +1,48 @@
-EQUAL
-ITE
-SKOLEM
-VARIABLE
-TUPLE
+# builtin_kinds                                                       -*- sh -*-
+#
+# This "kinds" file is written in a domain-specific language for
+# declaring CVC4 kinds.  Comments are marked with #, as this line is.
+# There are four basic commands:
+#
+#   special K ["comment"]
+#   operator K ["comment"]
+#   parameterized K ["comment"]
+#   constant K T ["comment"]
+#
+# special K (with an optional comment) declares a kind K that has no
+# operator (it's not conceptually an APPLY of an operator to
+# operands).  This is appropriate for special built-ins,
+# e.g. VARIABLE.
+#
+# operator K (with an optional comment) declares a "built-in"
+# operator.  Really this is the same as "special" except that it has
+# an operator (automatically generated by NodeManager).
+#
+# parameterized K (with an optional comment) declares a "built-in"
+# parameterized operator.  This is a theory-specific APPLY, e.g.,
+# APPLY_UF, which applies its first parameter (say, "f"), to its
+# operands (say, "x" and "y", making the full application "f(x,y)").
+# Nodes with such a kind will have an operator (Node::hasOperator()
+# returns true, and Node::getOperator() returns the Node of functional
+# type representing "f" here), and the "children" are defined to be
+# this operator's parameters, and don't include the operator itself
+# (here, there are only two children "x" and "y").  For consistency
+# these should probably start with "APPLY_", but this is not enforced.
+#
+# constant K T (with an optional comment) declares a constant kind.  T
+# is the C++ type representing the constant internally.  For
+# consistency, these should probably start with "CONST_", but this is
+# not enforced.
+#
+# This file is actually an executable Bourne shell script (sourced by
+# the processing scripts after defining functions called "special,"
+# "operator," "parameterized," and "constant").  So if you need a
+# multi-line comment string, do it the Bourne-like way.  Please don't
+# do anything else in this file than using these commands though.
+#
+
+operator EQUAL "equality"
+operator ITE "if-then-else"
+special SKOLEM "skolem var"
+special VARIABLE "variable"
+operator TUPLE "a tuple"

diff --git a/src/expr/mkkind b/src/expr/mkkind
index bc10f1e2c9d6b743dc73618fff85022eae26b630..cffdc0caa62aa1d7f6acbb07df8d6aaac785f0da 100755 (executable)
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -34,6 +34,28 @@ middle=$1; shift
 epilogue=$1; shift
 
 cases=
+
+function special {
+  r=$1
+  comment=$2
+
+  echo "  $r, /*! $comment */"
+  cases="$cases  case $r: out << \"$r\"; break;
+"
+}
+
+function operator {
+  special "$1" "$2"
+}
+
+function parameterized {
+  special "$1" "$2"
+}
+
+function constant {
+  special "$1" "$3"
+}
+
 cat "$prologue"
 while [ $# -gt 0 ]; do
   b=$(basename $(dirname "$1"))
@@ -42,11 +64,7 @@ while [ $# -gt 0 ]; do
   cases="$cases
   /* from $b */
 "
-  for r in `cat "$1"`; do
-    echo "  $r,"
-    cases="$cases  case $r: out << \"$r\"; break;
-"
-  done
+  source "$1"
   shift
 done
 cat "$middle"

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index fd784ccce2cf473e989ef9f5a991dc8fee80c7ef..f6540b9da04eff489c5dcea920cef8289b407781 100644 (file)
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -1,3 +1,12 @@
-PLUS
-MULT
-UMINUS
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/expr/builtin_kinds.
+#
+
+operator PLUS "arithmetic addition"
+operator MULT "arithmetic multiplication"
+operator UMINUS "arithmetic negation"
+
+constant CONST_RATIONAL ::CVC4::Rational "a multiple-precision rational constant"
+constant CONST_INTEGER ::CVC4::Integer "a multiple-precision integer constant"

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..63bff7ec9a8a969e742bd57a378978b7baa4e5f9 100644 (file)
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -0,0 +1,5 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/expr/builtin_kinds.
+#

diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 7f1267383f2271f92b5a597a9216f4af5f94434c..f70876ac55f22dceb21ca43bcb41d40427afce80 100644 (file)
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -1,8 +1,14 @@
-FALSE
-TRUE
-NOT
-AND
-IFF
-IMPLIES
-OR
-XOR
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/expr/builtin_kinds.
+#
+
+operator FALSE "falsity"
+operator TRUE "truth"
+operator NOT "logical not"
+operator AND "logical and"
+operator IFF "logical equivalence"
+operator IMPLIES "logical implication"
+operator OR "logical or"
+operator XOR "exclusive or"

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..63bff7ec9a8a969e742bd57a378978b7baa4e5f9 100644 (file)
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -0,0 +1,5 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/expr/builtin_kinds.
+#

diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
index 38c2153d6a7f37675f78ee617d4504815ac166b9..b80985c4711481d9d196e888c04bcb0ebc3a2c99 100755 (executable)
--- a/src/theory/mktheoryof
+++ b/src/theory/mktheoryof
@@ -34,6 +34,27 @@ middle=$1; shift
 epilogue=$1; shift
 
 registers=
+
+function special {
+  r=$1
+  comment=$2
+
+  registers="$registers    d_table[::CVC4::kind::$r] = th;
+"
+}
+
+function operator {
+  special "$1" "$2"
+}
+
+function parameterized {
+  special "$1" "$2"
+}
+
+function constant {
+  special "$1" "$3"
+}
+
 cat "$prologue"
 while [ $# -gt 0 ]; do
   b=$(basename $(dirname "$1"))
@@ -43,10 +64,7 @@ while [ $# -gt 0 ]; do
   /* from $b */
   void registerTheory(::CVC4::theory::$b::Theory$B* th) {
 "
-  for r in `cat "$1"`; do
-    registers="$registers    d_table[::CVC4::kind::$r] = th;
-"
-  done
+  source "$1"
   registers="$registers  }
 "
   shift

diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 5106136bcdf1ba31efd0740974924417dab57720..9280141ea9a68952b4db29e47a9145db2b8607be 100644 (file)
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -1 +1,7 @@
-APPLY
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/expr/builtin_kinds.
+#
+
+parameterized APPLY "uninterpreted function application"