diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:58:37 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-11 17:15:59 -0400 |
| commit | e80b93ca958bdbeb28959029868f6193b39a3f19 (patch) | |
| tree | 92218adf47348cb8011a41599e158b371f5659de /src/theory/builtin/kinds | |
| parent | b76afedab3a23525da478ba4a8687c882793ea81 (diff) | |
Support for TPTP's TFF0 (with arithmetic)
This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).
This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made. These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
Diffstat (limited to 'src/theory/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index fca79aff0..6a6fb2e31 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -300,7 +300,12 @@ operator SEXPR 0: "a symbolic expression" operator LAMBDA 2 "lambda" -parameterized CHAIN BUILTIN 2: "chain operator" +parameterized CHAIN CHAIN_OP 2: "chained operator" +constant CHAIN_OP \ + ::CVC4::Chain \ + ::CVC4::ChainHashFunction \ + "util/chain.h" \ + "the chained operator" constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ @@ -344,6 +349,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule +typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule constant SUBTYPE_TYPE \ ::CVC4::Predicate \ |