1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
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
|
(** Why3 driver specific for checking BV theory consistency with CVC4 *)
prelude "(set-logic AUFBVDTNIRA)"
(*
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
*)
import "smt-libv2.gen"
filename "%f-%t-%g.smt2"
printer "smtv2"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
(* Performed introductions depending on whether counterexamples are
requested, as said by the meta "get_counterexmp". When this meta
set, this transformation introduces the model variables that are
still embedded in the goal. When it is not set, it removes all
these unused-ce-related variables, even in the context. *)
transformation "counterexamples_dependent_intros"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_conditionally"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_inductive"
transformation "eliminate_epsilon"
transformation "eliminate_algebraic_if_poly"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to CVC4 *)
outofmemory "(error \".*out of memory\")"
outofmemory "CVC4 suffered a segfault"
outofmemory "CVC4::BVMinisat::OutOfMemoryException"
outofmemory "std::bad_alloc"
outofmemory "Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
(* Disabled:
CVC4 seems less efficient with its built-in implementation than
with the axiomatic version
*)
(*
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
*)
import "cvc4_bv.gen"
|
