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.

4 files changed, 166 insertions, 0 deletions

diff --git a/test/regress/regress0/tptp/Axioms/BOO004-0.ax b/test/regress/regress0/tptp/Axioms/BOO004-0.ax
new file mode 100644
index 000000000..e02b4c2f8
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/BOO004-0.ax
@@ -0,0 +1,48 @@
+%--------------------------------------------------------------------------
+% File     : BOO004-0 : TPTP v5.5.0. Released v1.0.0.
+% Domain   : Boolean Algebra
+% Axioms   : Boolean algebra (equality) axioms
+% Version  : [Ver94] (equality) axioms.
+% English  :
+
+% Refs     : [Ver94] Veroff (1994), Problem Set
+% Source   : [Ver94]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of clauses    :    8 (   0 non-Horn;   8 unit;   0 RR)
+%            Number of atoms      :    8 (   8 equality)
+%            Maximal clause size  :    1 (   1 average)
+%            Number of predicates :    1 (   0 propositional; 2-2 arity)
+%            Number of functors   :    5 (   2 constant; 0-2 arity)
+%            Number of variables  :   14 (   0 singleton)
+%            Maximal term depth   :    3 (   2 average)
+% SPC      : 
+
+% Comments :
+%--------------------------------------------------------------------------
+cnf(commutativity_of_add,axiom,
+    ( add(X,Y) = add(Y,X) )).
+
+cnf(commutativity_of_multiply,axiom,
+    ( multiply(X,Y) = multiply(Y,X) )).
+
+cnf(distributivity1,axiom,
+    ( add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)) )).
+
+cnf(distributivity2,axiom,
+    ( multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) )).
+
+cnf(additive_id1,axiom,
+    ( add(X,additive_identity) = X )).
+
+cnf(multiplicative_id1,axiom,
+    ( multiply(X,multiplicative_identity) = X )).
+
+cnf(additive_inverse1,axiom,
+    ( add(X,inverse(X)) = multiplicative_identity )).
+
+cnf(multiplicative_inverse1,axiom,
+    ( multiply(X,inverse(X)) = additive_identity )).
+
+%--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Axioms/SYN000+0.ax b/test/regress/regress0/tptp/Axioms/SYN000+0.ax
new file mode 100644
index 000000000..24ef682b7
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/SYN000+0.ax
@@ -0,0 +1,37 @@
+%------------------------------------------------------------------------------
+% File     : SYN000+0 : TPTP v5.5.0. Released v3.6.0.
+% Domain   : Syntactic
+% Axioms   : A simple include file for FOF
+% Version  : Biased.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of formulae    :    3 (   3 unit)
+%            Number of atoms       :    3 (   0 equality)
+%            Maximal formula depth :    1 (   1 average)
+%            Number of connectives :    0 (   0 ~  ;   0  |;   0  &)
+%                                         (   0 <=>;   0 =>;   0 <=)
+%                                         (   0 <~>;   0 ~|;   0 ~&)
+%            Number of predicates  :    3 (   3 propositional; 0-0 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    0 (   0 singleton;   0 !;   0 ?)
+%            Maximal term depth    :    0 (   0 average)
+% SPC      : 
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+fof(ia1,axiom,
+    ia1).
+
+fof(ia2,axiom,
+    ia2).
+
+fof(ia3,axiom,
+    ia3).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Axioms/SYN000-0.ax b/test/regress/regress0/tptp/Axioms/SYN000-0.ax
new file mode 100644
index 000000000..d67e61aee
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/SYN000-0.ax
@@ -0,0 +1,34 @@
+%------------------------------------------------------------------------------
+% File     : SYN000-0 : TPTP v5.5.0. Released v3.6.0.
+% Domain   : Syntactic
+% Axioms   : A simple include file for CNF
+% Version  : Biased.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of clauses     :    3 (   0 non-Horn;   3 unit;   3 RR)
+%            Number of atoms       :    3 (   0 equality)
+%            Maximal clause size   :    1 (   1 average)
+%            Number of predicates  :    3 (   3 propositional; 0-0 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    0 (   0 singleton)
+%            Maximal term depth    :    0 (   0 average)
+% SPC      : 
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+cnf(ia1,axiom,
+    ia1).
+
+cnf(ia2,axiom,
+    ia2).
+
+cnf(ia3,axiom,
+    ia3).
+
+%------------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/Axioms/SYN000_0.ax b/test/regress/regress0/tptp/Axioms/SYN000_0.ax
new file mode 100644
index 000000000..acb557ef4
--- /dev/null
+++ b/test/regress/regress0/tptp/Axioms/SYN000_0.ax
@@ -0,0 +1,47 @@
+%------------------------------------------------------------------------------
+% File     : SYN000_0 : TPTP v5.5.0. Released v5.0.0.
+% Domain   : Syntactic
+% Axioms   : A simple include file for TFF
+% Version  : Biased.
+% English  :
+
+% Refs     :
+% Source   : [TPTP]
+% Names    :
+
+% Status   : Satisfiable
+% Syntax   : Number of formulae    :    6 (   6 unit;   3 type)
+%            Number of atoms       :    6 (   0 equality)
+%            Maximal formula depth :    2 (   2 average)
+%            Number of connectives :    0 (   0   ~;   0   |;   0   &)
+%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
+%                                         (   0  ~|;   0  ~&)
+%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
+%            Number of predicates  :    4 (   4 propositional; 0-0 arity)
+%            Number of functors    :    0 (   0 constant; --- arity)
+%            Number of variables   :    0 (   0 sgn;   0   !;   0   ?)
+%            Maximal term depth    :    0 (   0 average)
+% SPC      : 
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+tff(ia1_type,type,(
+    ia1: $o )).
+
+tff(ia2_type,type,(
+    ia2: $o )).
+
+tff(ia3_type,type,(
+    ia3: $o )).
+
+tff(ia1,axiom,(
+    ia1 )).
+
+tff(ia2,axiom,(
+    ia2 )).
+
+tff(ia3,axiom,(
+    ia3 )).
+
+%------------------------------------------------------------------------------