diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
| commit | 349131957e91150c24a9c69f5e1f04e34494b0c6 (patch) | |
| tree | 8012c2475dde1f1177f693643fb1a07e89c29538 /src/expr/mkkind | |
| parent | ac8b46fe3b5256e387da724b7c3abfb59d25531e (diff) | |
Added the capability to construct expressions by passing the operator instead of the kind, i.e.
Expr op = ..."f"...
em.mkExpr(op, children);
Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.
Diffstat (limited to 'src/expr/mkkind')
| -rwxr-xr-x | src/expr/mkkind | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind index 294dc5d7e..d9c64b660 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -93,12 +93,12 @@ function nonatomic_operator { } function parameterized { - # parameterized K #children ["comment"] + # parameterized K1 K2 #children ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_kind "$1" "$2" "$3" + register_kind "$1" "$3" "$4" } function constant { |