Commit 07a740bb authored by Andrei Paskevich's avatar Andrei Paskevich

tff0 doesn't support sort constructors

parent eb552e9d
(* Why driver for first-order tptp provers supporting TFF1 *) (* Why driver for first-order tptp provers supporting TFF0 *)
printer "tptp-tff" printer "tptp-tff"
filename "%f-%t-%g.p" filename "%f-%t-%g.p"
...@@ -31,6 +31,7 @@ transformation "eliminate_inductive" ...@@ -31,6 +31,7 @@ transformation "eliminate_inductive"
transformation "eliminate_algebraic" transformation "eliminate_algebraic"
transformation "encoding_smt" transformation "encoding_smt"
transformation "encoding_sort"
theory BuiltIn theory BuiltIn
syntax predicate (=) "(%1 = %2)" syntax predicate (=) "(%1 = %2)"
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment