Commit 4bcdf5ad authored by Andrei Paskevich's avatar Andrei Paskevich

TPTP: fix representation of "inv" for rationals in drivers

parent 2e165465
......@@ -183,7 +183,7 @@ theory tptp.Rat
syntax function (-_) "$uminus(%1)"
syntax function (/) "$quotient(%1,%2)"
syntax function inv "$quotient(1.0,%1)"
syntax function inv "$quotient(1/1,%1)"
syntax predicate (<=) "$lesseq(%1,%2)"
syntax predicate (<) "$less(%1,%2)"
......
......@@ -180,7 +180,7 @@ theory tptp.Rat
syntax function (-_) "$uminus(%1)"
syntax function (/) "$quotient(%1,%2)"
syntax function inv "$quotient(1.0,%1)"
syntax function inv "$quotient(1/1,%1)"
syntax predicate (<=) "$lesseq(%1,%2)"
syntax predicate (<) "$less(%1,%2)"
......
......@@ -175,7 +175,7 @@ theory tptp.Rat
syntax function (-_) "$uminus(%1)"
syntax function (/) "$quotient(%1,%2)"
syntax function inv "$quotient(1.0,%1)"
syntax function inv "$quotient(1/1,%1)"
syntax predicate (<=) "$lesseq(%1,%2)"
syntax predicate (<) "$less(%1,%2)"
......
......@@ -166,7 +166,7 @@ theory tptp.Rat
syntax function (-_) "$uminus(%1)"
syntax function (/) "$quotient(%1,%2)"
syntax function inv "$quotient(1.0,%1)"
syntax function inv "$quotient(1/1,%1)"
syntax predicate (<=) "$lesseq(%1,%2)"
syntax predicate (<) "$less(%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