Commit 8515d7d1 authored by Andrei Paskevich's avatar Andrei Paskevich

minor corrections in drivers

parent c0e146fa
......@@ -28,18 +28,12 @@ trigger they can't appear since = can't appear *)
(*transformation "filter_trigger_builtin"*)
(* this is sound as long as int is the only kept type *)
transformation "encoding_smt"
transformation "encoding_tptp"
theory BuiltIn
syntax predicate (=) "(EQ %1 %2)"
meta "encoding : base" type int
(* no symbol discrimination, no kept types *)
meta "select_inst" "none"
meta "select_lskept" "none"
meta "select_lsinst" "none"
meta "select_kept" "none"
end
theory int.Int
......
......@@ -34,8 +34,6 @@ theory BuiltIn
syntax type int "$int"
syntax type real "$real"
meta "encoding : kept" type int
meta "encoding : kept" type real
meta "eliminate_algebraic" "no_index"
end
......@@ -131,8 +129,6 @@ end
theory tptp.Univ
syntax type iType "$i"
meta "encoding : kept" type iType
end
theory tptp.IntTrunc
......@@ -199,8 +195,6 @@ theory tptp.Rat
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type rat
end
theory tptp.RatTrunc
......
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