Commit 9b8b5f11 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix driver for cvc4 1.5

parent 6fd72eea
(** Why3 driver for CVC4 >= 1.4 *) (** Why3 driver for CVC4 1.4 *)
prelude "(set-logic AUFBVDTNIRA)" prelude "(set-logic AUFBVDTNIRA)"
(* (*
......
...@@ -25,6 +25,7 @@ transformation "detect_polymorphism" ...@@ -25,6 +25,7 @@ transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly" transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive" transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly" transformation "eliminate_algebraic_if_poly"
transformation "eliminate_literal"
transformation "eliminate_epsilon" transformation "eliminate_epsilon"
transformation "simplify_formula" transformation "simplify_formula"
...@@ -32,7 +33,8 @@ transformation "simplify_formula" ...@@ -32,7 +33,8 @@ transformation "simplify_formula"
(* Prepare for counter-example query: get rid of some quantifiers (makes it (* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce possible to query model values of the variables in premises) and introduce
counter-example projections *) counter-example projections.
Note: does nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp" transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly" transformation "discriminate_if_poly"
...@@ -50,9 +52,7 @@ steplimitexceeded "??" ...@@ -50,9 +52,7 @@ steplimitexceeded "??"
(** Extra theories supported by CVC4 *) (** Extra theories supported by CVC4 *)
(* Disabled: (* CVC4 division seems to be the Euclidean one, not the Computer one *)
CVC4 division seems to be neither the Euclidean one, nor the Computer one
theory int.EuclideanDivision theory int.EuclideanDivision
syntax function div "(div %1 %2)" syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)" syntax function mod "(mod %1 %2)"
...@@ -62,6 +62,7 @@ theory int.EuclideanDivision ...@@ -62,6 +62,7 @@ theory int.EuclideanDivision
remove prop Div_1 remove prop Div_1
end end
(*
theory int.ComputerDivision theory int.ComputerDivision
syntax function div "(div %1 %2)" syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)" syntax function mod "(mod %1 %2)"
......
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
<prover id="3" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="3" name="Alt-Ergo" version="1.20.prv" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.10.prv" timelimit="2" steplimit="0" memlimit="1000"/> <prover id="4" name="Alt-Ergo" version="1.10.prv" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="5" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="5" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="6" name="CVC4" version="1.5" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/> <prover id="7" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.1" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="8" name="Z3" version="4.3.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="9" name="Spass" version="3.7" timelimit="1" steplimit="0" memlimit="1000"/> <prover id="9" name="Spass" version="3.7" timelimit="1" steplimit="0" memlimit="1000"/>
......
...@@ -143,6 +143,7 @@ let p1 = path_of_file "/bin/bash" ...@@ -143,6 +143,7 @@ let p1 = path_of_file "/bin/bash"
let p1 = path_of_file "../src/f.why" let p1 = path_of_file "../src/f.why"
*) *)
(*
let normalize_filename f = let normalize_filename f =
let rec aux af acc = let rec aux af acc =
match af, acc with match af, acc with
...@@ -161,6 +162,7 @@ let normalize_filename f = ...@@ -161,6 +162,7 @@ let normalize_filename f =
| [], _ -> acc | [], _ -> acc
in in
file_of_path (List.rev (aux (path_of_file f) [])) file_of_path (List.rev (aux (path_of_file f) []))
*)
let relativize_filename base f = let relativize_filename base f =
let rec aux ab af = let rec aux ab af =
......
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