diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-03 22:46:36 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-02-03 22:46:36 +0000 |
| commit | cf8b81553abf579d151b04a40cd82dec48bfd6ff (patch) | |
| tree | 275c457d85fa2a0d4843343ad1d7d25017f13cdd /src/expr/kind.h | |
| parent | 64d530e5b9096e66398f92d93cf7bc4268df0e70 (diff) | |
Adding functions/predicates to SMT grammar
Diffstat (limited to 'src/expr/kind.h')
| -rw-r--r-- | src/expr/kind.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/expr/kind.h b/src/expr/kind.h index 8ba282f0f..64991c71c 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -36,6 +36,7 @@ enum Kind { ITE, SKOLEM, VARIABLE, + APPLY, /* propositional connectives */ FALSE, @@ -53,7 +54,6 @@ enum Kind { PLUS, MINUS, MULT - };/* enum Kind */ inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC; @@ -70,6 +70,7 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) { case ITE: out << "ITE"; break; case SKOLEM: out << "SKOLEM"; break; case VARIABLE: out << "VARIABLE"; break; + case APPLY: out << "APPLY"; break; /* propositional connectives */ case FALSE: out << "FALSE"; break; |