cvc4_15.drv 1.98 KB
Newer Older
1 2
(** Why3 driver for CVC4 >= 1.5 *)

Sylvain Dailler's avatar
Sylvain Dailler committed
3
prelude "(set-logic AUFBVDTNIRA)"
4 5 6 7 8 9 10 11 12 13 14 15
(*
    A  : Array
    UF : Uninterpreted Function
    BV : BitVectors
    DT : Datatypes
    NIRA : NonLinear Integer Reals Arithmetic
*)
(* prelude "(set-logic ALL_SUPPORTED)"
   does not seem to include DT
*)

(* Counterexamples: set model parser *)
16
model_parser "smtv2"
17

Sylvain Dailler's avatar
Sylvain Dailler committed
18
import "smt-libv2.drv"
19
import "smt-libv2-bv.gen"
20 21 22 23 24 25 26 27
import "discrimination.gen"

transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
MARCHE Claude's avatar
MARCHE Claude committed
28
transformation "eliminate_literal"
29 30 31 32 33
transformation "eliminate_epsilon"

transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)

David Hauzar's avatar
David Hauzar committed
34
(* Prepare for counter-example query: get rid of some quantifiers (makes it
35
possible to query model values of the variables in premises) and introduce
MARCHE Claude's avatar
MARCHE Claude committed
36 37
counter-example projections.
Note: does nothing if meta get_counterexmp is not set *)
38
transformation "prepare_for_counterexmp"
39

40 41 42 43 44 45 46 47
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"

(** Error messages specific to CVC4 *)

outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
48 49
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
50
steplimitexceeded "??"
51
*)
52 53 54

(** Extra theories supported by CVC4 *)

MARCHE Claude's avatar
MARCHE Claude committed
55
(* CVC4 division seems to be the Euclidean one, not the Computer one *)
56 57 58 59 60 61 62 63 64
theory int.EuclideanDivision
   syntax function div "(div %1 %2)"
   syntax function mod "(mod %1 %2)"
   remove prop Mod_bound
   remove prop Div_mod
   remove prop Mod_1
   remove prop Div_1
end

MARCHE Claude's avatar
MARCHE Claude committed
65
(*
66 67 68 69 70 71 72 73 74 75
theory int.ComputerDivision
   syntax function div "(div %1 %2)"
   syntax function mod "(mod %1 %2)"
   remove prop Mod_bound
   remove prop Div_mod
   remove prop Mod_1
   remove prop Div_1
end
*)

76
import "cvc4_bv.gen"