diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-09 11:18:18 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-09 17:46:21 -0400 |
| commit | ec4d1e3753434f5d34a22e653dace14b87557aaf (patch) | |
| tree | 9cfa4fc484dd5e27373277751887e50558a458df | |
| parent | e93d0be650b9f349fe8be3a56ce2fc7cb20fddf0 (diff) | |
Minor change to better support parameterized partial/total kinds (for upcoming datatypes work).
| -rwxr-xr-x | src/expr/mkmetakind | 4 | ||||
| -rw-r--r-- | src/options/base_options | 2 | ||||
| -rw-r--r-- | 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 |