From ec4d1e3753434f5d34a22e653dace14b87557aaf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 9 Apr 2014 11:18:18 -0400 Subject: [PATCH] Minor change to better support parameterized partial/total kinds (for upcoming datatypes work). --- src/expr/mkmetakind | 4 +++- src/options/base_options | 2 +- src/theory/builtin/kinds | 9 ++++++--- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 4dc2908a7..5f003dcfb 100755 --- 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 dd4da0f31..f3ba38a6a 100644 --- 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 b51feea6d..b3383e6c4 100644 --- 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 -- 2.30.2