verit.drv 1.06 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1
(* Why3 driver for veriT solver *)
MARCHE Claude's avatar
docs  
MARCHE Claude committed
2 3

prelude ";;; this is a prelude for veriT"
MARCHE Claude's avatar
MARCHE Claude committed
4
prelude "(set-logic AUFLIRA)"
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8
(* A  : Array
   UF : Uninterpreted Function
   LIRA : Linear Integer Reals Arithmetic
*)
MARCHE Claude's avatar
docs  
MARCHE Claude committed
9

MARCHE Claude's avatar
MARCHE Claude committed
10 11
import "smt-libv2.drv"
import "discrimination.gen"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
12

MARCHE Claude's avatar
MARCHE Claude committed
13
(* specific message from veriT 201310 *)
MARCHE Claude's avatar
MARCHE Claude committed
14
unknown "non-linear reasoning desactivated" ""
MARCHE Claude's avatar
MARCHE Claude committed
15 16
(* specific message from veriT 201410 *)
unknown "error : Non linear expression with non-linear reasoning disabled" ""
MARCHE Claude's avatar
MARCHE Claude committed
17

MARCHE Claude's avatar
docs  
MARCHE Claude committed
18 19 20 21 22
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
23
transformation "eliminate_algebraic"
24
transformation "eliminate_epsilon"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
25 26

transformation "simplify_formula"
27
(*transformation "simplify_trivial_quantification"*)
MARCHE Claude's avatar
docs  
MARCHE Claude committed
28 29

transformation "encoding_smt"
30
transformation "encoding_sort"
MARCHE Claude's avatar
docs  
MARCHE Claude committed
31

32 33
(*
disabled: veriT seems more efficient with the axiomatic version
34
theory int.EuclideanDivision
Andrei Paskevich's avatar
Andrei Paskevich committed
35 36 37 38 39 40
  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
41
end
42
*)