Commit 496c821f authored by François Bobot's avatar François Bobot

Add colibri

parent 24cb7442
(** Why3 driver for Colibri (with floating point support) *)
prelude ";; produced by colibri.drv ;;"
prelude "(set-logic QF_NIRABVFP)"
prelude "(set-info :smt-lib-version 2.6)"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "smt-libv2-floats.gen"
(* import "discrimination.gen" *)
theory BuiltIn
meta "select_inst_default" "all"
meta "select_lskept_default" "all"
meta "select_lsinst_default" "all"
meta "select_kept_default" "all"
end
transformation "inline_trivial"
transformation "eliminate_builtin"
(* transformation "detect_polymorphism" because eliminate algebraic
add polymorphism *)
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
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 "introduce_premises"
transformation "instantiate_predicate"
transformation "abstract_quantifiers"
transformation "discriminate"
transformation "encoding_smt"
transformation "abstract_quantifiers"
(** Extra theories supported by COLIBRI *)
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 "(colibri_cdiv %1 %2)"
syntax function mod "(colibri_crem %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory real.Truncate
syntax function floor "(to_int %1)"
syntax function truncate "(to_int (colibri_truncate %1))"
syntax function ceil "(to_int (colibri_ceil %1))"
remove prop Floor_down
remove prop Floor_monotonic
end
theory real.FromInt
syntax function from_int "(to_real %1)"
end
theory real.Abs
syntax function abs "(colibri_abs_real %1)"
end
theory int.Abs
syntax function abs "(colibri_abs_int %1)"
end
theory real.PowerInt
syntax function power "(colibri_pow_real_int %1 %2)"
end
theory int.Power
syntax function power "(colibri_pow_int_int %1 %2)"
end
theory real.ExpLog
syntax function exp "(colibri_exp %1)"
(* syntax function log "(colibri_ln %1)" *)
end
theory real.MinMax
syntax function min "(colibri_min %1)"
syntax function max "(colibri_max %1)"
end
theory int.MinMax
syntax function min "(colibri_min %1)"
syntax function max "(colibri_max %1)"
end
(** TODO *)
(**
- colibri_floor
- colibri_abs_int
- colibri_abs_real
- colibri_truncate
- colibri_pow_real_int
- colibri_max
- colibri_min
- is_int
- to_int
- to_real
*)
......@@ -129,6 +129,29 @@ version_old = "1.0"
driver = "cvc4"
command = "%e --lang=smt2 %f"
# COLIBRI with counterexamples
[ATP colibri-ce]
name = "COLIBRI"
alternative = "counterexamples"
exec = "colibri"
version_switch = "--version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok = "2137"
driver = "colibri"
command = "%e --memlimit %m %f"
# COLIBRI
[ATP colibri]
name = "COLIBRI"
exec = "colibri"
version_switch = "--version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok = "2137"
driver = "colibri"
command = "%e --memlimit %m %f"
# Psyche version 2.x
[ATP psyche]
name = "Psyche"
......
......@@ -34,5 +34,5 @@ let elim_less (d:decl) =
let () =
Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None)
~desc:"Abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context \
~desc:"Weaken quantifiers@ by replacing them by true or false in@ the@ axioms@ of@ the@ context \
and@ the@ goals."
Markdown is supported
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