Commit 230d4f2b authored by MARCHE Claude's avatar MARCHE Claude

make driver mst-libv2 generique since it does not contains printer anymore

parent d0bd45de
......@@ -12,7 +12,7 @@ prelude "(set-logic AUFBVDTNIRA)"
does not seem to include DT
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
......
......@@ -7,7 +7,7 @@ prelude "(set-logic AUFNIRA)"
NIRA : NonLinear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "no-bv.gen"
import "discrimination.gen"
......
......@@ -10,7 +10,7 @@ prelude "(set-logic AUFBVDTNIRA)"
NIRA : NonLinear Integer+Real Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
......
......@@ -10,7 +10,7 @@ prelude "(set-logic AUFBVDTNIRA)"
NIRA : NonLinear Integer+Real Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
......
......@@ -12,7 +12,7 @@ prelude "(set-logic AUFBVFPDTNIRA)"
NIRA : NonLinear Integer+Real Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2.6"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
......
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_int *)
theory bv.BV_Gen
......
......@@ -7,7 +7,7 @@ prelude "(set-logic AUFLIRA)"
LIRA : Linear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "discrimination.gen"
......
......@@ -7,7 +7,7 @@ prelude "(set-logic QF_AUFLIRA)"
LIRA : Linear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "discrimination.gen"
......
......@@ -6,7 +6,7 @@ prelude "(set-logic AUFNIRA)"
NIRA : NonLinear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "discrimination.gen"
......
......@@ -7,7 +7,7 @@
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "no-bv.gen"
import "discrimination.gen"
......@@ -80,7 +80,7 @@ end
(* REMOVED: we do not use BV theory from Z3 in 4.3.2 but starting from 4.4.0
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
......
......@@ -7,7 +7,7 @@
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "z3_bv.gen"
......
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV_Gen
......
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