Minor change to better support parameterized partial/total kinds (for upcoming dataty...

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 4dc2908a76a22c2c71d8a613553624f81e485106..5f003dcfb47acca829e976c4efeedd3e6e5cf837 100755 (executable)
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -203,7 +203,9 @@ function parameterized {
 
   check_theory_seen
   register_metakind PARAMETERIZED "$1" "$3"
-  registerOperatorToKind "$1" "$2"
+  if ! expr "$2" : '\[.*\]' &>/dev/null; then
+    registerOperatorToKind "$1" "$2"
+  fi
 }
 
 function constant {

diff --git a/src/options/base_options b/src/options/base_options
index dd4da0f31f3be6a949a5ad9e1ef62508f8293a26..f3ba38a6a4b5f2ea51b40492c0dc9fa36961abf4 100644 (file)
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -108,7 +108,7 @@ common-option statistics statistics --stats bool :predicate CVC4::smt::statsEnab
 undocumented-alias --statistics = --stats
 undocumented-alias --no-statistics = --no-stats
 option statsEveryQuery --stats-every-query bool :default false :link --stats
- in incremental mode, print stats after every satisfiability or validity query 
+ in incremental mode, print stats after every satisfiability or validity query
 undocumented-alias --statistics-every-query = --stats-every-query
 undocumented-alias --no-statistics-every-query = --no-stats-every-query
 

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index b51feea6d4c52be8ae6ddaa5d0d77e9ffda99f8f..b3383e6c42e1b611cc638369a8ad1ade51d88d27 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -97,9 +97,9 @@
 #
 #         operator PLUS 2: "addition on two or more arguments"
 #
-#   parameterized K #children ["comment"]
+#   parameterized K1 K2 #children ["comment"]
 #
-#     Declares a "built-in" parameterized operator kind K.  This is a
+#     Declares a "built-in" parameterized operator kind K1.  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
@@ -107,7 +107,10 @@
 #     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").
+#     itself (here, there are only two children "x" and "y").  The
+#     operator ("f") should have kind K2 (and this should be enforced
+#     by the custom typechecker, at present this isn't done uniformly
+#     by the expression package).
 #
 #     LB and UB are the same as documented for the operator command,
 #     except that parameterized operators may have zero children.  The