diff --git a/drivers/z3_smtv1.drv b/drivers/z3_smtv1.drv deleted file mode 100644 index 0088ace4379d687a0ccc7f4ca9199c4a7d27f63a..0000000000000000000000000000000000000000 --- a/drivers/z3_smtv1.drv +++ /dev/null @@ -1,168 +0,0 @@ -(* Why driver for SMT syntax *) - -prelude ";;; this is a prelude for Z3" -prelude "(set-logic AUFNIRA)" - -printer "smtv2" -filename "%f-%t-%g.smt" - -valid "^unsat" -unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown" -time "why3cpulimit time : %s s" - - -(* À discuter *) -transformation "simplify_recursive_definition" -transformation "inline_trivial" - -transformation "eliminate_builtin" -transformation "eliminate_definition" -transformation "eliminate_inductive" -transformation "eliminate_algebraic_smt" - -transformation "simplify_formula" -(*transformation "simplify_trivial_quantification"*) - -transformation "encoding_smt" - -theory BuiltIn - syntax type int "Int" - syntax type real "Real" - syntax logic (=) "(= %1 %2)" -end - -theory int.Int - - prelude ";;; this is a prelude for Z3 integer arithmetic" - - syntax logic zero "0" - syntax logic one "1" - - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (-_) "(- %1)" - - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" - - remove prop CommutativeGroup.Comm.Comm - remove prop CommutativeGroup.Assoc.Assoc - remove prop CommutativeGroup.Unit_def - remove prop CommutativeGroup.Inv_def - remove prop Assoc.Assoc - remove prop Mul_distr - remove prop Comm.Comm - remove prop Unitary - remove prop Refl - remove prop Trans - remove prop Antisymm - remove prop Total - remove prop NonTrivialRing - remove prop CompatOrderAdd - - meta "encoding : kept" type int - -end - - -theory real.Real - - prelude ";;; this is a prelude for Z3 real arithmetic" - - syntax logic zero "0.0" - syntax logic one "1.0" - - syntax logic (+) "(+ %1 %2)" - syntax logic (-) "(- %1 %2)" - syntax logic (*) "(* %1 %2)" - syntax logic (/) "(/ %1 %2)" - syntax logic (-_) "(- %1)" - syntax logic inv "(/ 1.0 %1)" - - syntax logic (<=) "(<= %1 %2)" - syntax logic (<) "(< %1 %2)" - syntax logic (>=) "(>= %1 %2)" - syntax logic (>) "(> %1 %2)" - - remove prop CommutativeGroup.Comm.Comm - remove prop CommutativeGroup.Assoc.Assoc - remove prop CommutativeGroup.Unit_def - remove prop CommutativeGroup.Inv_def - remove prop Inverse - remove prop Assoc.Assoc - remove prop Mul_distr - remove prop Comm.Comm - remove prop Unitary - remove prop Refl - remove prop Trans - remove prop Antisymm - remove prop Total - remove prop NonTrivialRing - remove prop CompatOrderAdd - - meta "encoding : kept" type real - -end - -(* -(* L'encodage des types sommes bloquent cette théorie builtin *) -theory bool.Bool - syntax type bool "bool" - syntax logic True "true" - syntax logic False "false" - syntax logic andb "(and %1 %2)" - syntax logic orb "(or %1 %2)" - syntax logic xorb "(xor %1 %2)" - syntax logic notb "(not %1)" - meta cloned "encoding_decorate : kept" type bool -end -*) - - -theory int.EuclideanDivision - syntax logic div "(div %1 %2)" - syntax logic mod "(mod %1 %2)" - remove prop Mod_bound - remove prop Div_mod - remove prop Mod_1 - remove prop Div_1 -end - -(* -theory real.FromInt - syntax logic from_int "(from_int %1)" - remove prop Add - remove prop Sub - remove prop Mul - remove prop Neg -end -*) - -(* -theory real.Truncate - syntax logic floor "(to_int %1)" - remove prop Floor_down - remove prop Floor_monotonic -end -*) - -theory array.Array - syntax type t "(Array %1 %2)" - meta "encoding : lskept" logic get - meta "encoding : lskept" logic set - meta "encoding : lskept" logic create_const - - meta "smt_dist_syntax" logic get, "(select %1 %2)" - meta "smt_dist_syntax" logic set, "(store %1 %2 %3)" - meta "smt_dist_syntax" logic create_const, "(const[%t0] %1)" -end - -(* -Local Variables: -mode: why -compile-command: "unset LANG; make -C .. bench" -End: -*) diff --git a/src/transform/encoding_arrays.mli b/src/transform/encoding_arrays.mli deleted file mode 100644 index 4ac471af3d6fa5d5a26aa89e406e4bb7243bb5a6..0000000000000000000000000000000000000000 --- a/src/transform/encoding_arrays.mli +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* *) -(* Copyright (C) 2010- *) -(* François Bobot *) -(* Jean-Christophe Filliâtre *) -(* Claude Marché *) -(* Andrei Paskevich *) -(* *) -(* This software is free software; you can redistribute it and/or *) -(* modify it under the terms of the GNU Library General Public *) -(* License version 2.1, with the special exception on linking *) -(* described in file LICENSE. *) -(* *) -(* This software is distributed in the hope that it will be useful, *) -(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) -(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *) -(* *) -(**************************************************************************) - - -val lsymbol_distinction : Task.task Trans.trans - -val phase0 : Task.task Trans.trans diff --git a/src/transform/encoding_distinction.mli b/src/transform/encoding_distinction.mli index 04a917d58db8998d8ea3cf1fd232edbf2bb4c8ef..a8aaf05302944faab15c655c82672ef7b6a8c37c 100644 --- a/src/transform/encoding_distinction.mli +++ b/src/transform/encoding_distinction.mli @@ -1,9 +1,9 @@ (**************************************************************************) (* *) (* Copyright (C) 2010- *) -(* François Bobot *) -(* Jean-Christophe Filliâtre *) -(* Claude Marché *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) (* Andrei Paskevich *) (* *) (* This software is free software; you can redistribute it and/or *) diff --git a/src/transform/encoding_select.ml b/src/transform/encoding_select.ml index 7678780262e35706bdf78a84382cc0d74ccd9ebf..50c411b564871cf168adc215fadaea8ede0cc114 100644 --- a/src/transform/encoding_select.ml +++ b/src/transform/encoding_select.ml @@ -184,6 +184,7 @@ let inst_nothing _env = Trans.identity (** goal *) let inst_goal _env = + Trans.compose (inst_nothing _env) $ Trans.tgoal (fun pr f -> let env = f_app_fold add_mono_instantiation Mls.empty f in metas_of_env env [create_decl (create_prop_decl Pgoal pr f)]) @@ -191,6 +192,7 @@ let inst_goal _env = (** goal + context *) let inst_all _env = + Trans.compose (inst_nothing _env) $ Trans.bind (Trans.fold fold_add_instantion Mls.empty) (fun env -> Trans.add_tdecls (metas_of_env env [])) diff --git a/src/transform/encoding_select.mli b/src/transform/encoding_select.mli index 96af8110e70ad85fca1adb63d18434d2eceac3d7..07a82e01e95f58695a2c6e8ba5197b7fc6990b48 100644 --- a/src/transform/encoding_select.mli +++ b/src/transform/encoding_select.mli @@ -1,9 +1,9 @@ (**************************************************************************) (* *) (* Copyright (C) 2010- *) -(* François Bobot *) -(* Jean-Christophe Filliâtre *) -(* Claude Marché *) +(* François Bobot *) +(* Jean-Christophe Filliâtre *) +(* Claude Marché *) (* Andrei Paskevich *) (* *) (* This software is free software; you can redistribute it and/or *)