Commit acc2634b authored by Jonathan Moerman's avatar Jonathan Moerman
Browse files

Add cvc4 1.6 driver

parent 6c953819
(** Why3 driver for CVC4 >= 1.6 (with floating point support) *)
prelude ";; produced by cvc4_16.drv ;;"
prelude "(set-info :smt-lib-version 2.6)"
prelude "(set-logic AUFFPDTNIRA)"
(*
A : Array
UF : Uninterpreted Function
FP : FloatingPoint
DT : Datatypes
NIRA : NonLinear Integer+Real Arithmetic
*)
import "smt-libv2.gen"
printer "smtv2.6"
import "no-bv.gen"
import "smt-libv2-floats.gen"
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"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(* Prepare for counter-example query: get rid of some quantifiers
(makes it possible to query model values of the variables in
premises) and introduce counter-example projections. Note: does
nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
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
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
(* CVC4 division seems to be the Euclidean one, not 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
*)
Supports Markdown
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