cvc4_15.drv 2.09 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
(** Why3 driver for CVC4 >= 1.5 *)

prelude "(set-logic AUFBVDTLIRA)"
(*
    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
*)

15
(* Counterexamples: makes it possible to get rid of more quantifiers while introducing premises *)
16
17
18
(* transformation "split_intro" *)

(* Counterexamples: set model parser *)
19
model_parser "smtv2"
20
21

import "smt-libv2.drv"
22
import "smt-libv2-bv.gen"
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
import "discrimination.gen"

transformation "inline_trivial"
transformation "eliminate_builtin"
(* temporarily disabled: too much experimental
transformation "detect_polymorphism"
*)
transformation "eliminate_definition_if_poly"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"

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

David Hauzar's avatar
David Hauzar committed
38
(* Prepare for counter-example query: get rid of some quantifiers (makes it
39
40
41
possible to query model values of the variables in premises) and introduce
counter-example projections  *)
transformation "prepare_for_counterexmp"
42

43
44
45
46
47
48
49
50
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
51
52
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
53
steplimitexceeded "??"
54
*)
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

(** Extra theories supported by CVC4 *)

(* Disabled:
   CVC4 division seems to be neither the Euclidean one, nor the Computer one

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

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
*)

80
import "cvc4_bv.gen"