preliminary support for Psyche

parent 6e1bd669
(* Why driver for Psyche *)
prelude "(set-logic FO)"
printer "smtv2"
filename "%f-%t-%g.smt2"
valid "^PROVABLE"
invalid "^NOT PROVABLE"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"
(* À discuter *)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate"
transformation "encoding_smt"
theory BuiltIn
syntax type real "Real"
syntax predicate (=) "(= %1 %2)"
meta "eliminate_algebraic" "no_index"
end
theory real.Real
prelude ";;; this is a prelude for smt-lib v2 real arithmetic"
syntax function zero "0"
syntax function one "1"
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function ( * ) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
syntax function (-_) "(- %1)"
syntax function inv "(/ 1 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
syntax predicate (>=) "(>= %1 %2)"
syntax predicate (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc
remove prop CommutativeGroup.Unit_def_l
remove prop CommutativeGroup.Unit_def_r
remove prop CommutativeGroup.Inv_def_l
remove prop CommutativeGroup.Inv_def_r
remove prop Assoc.Assoc
remove prop Mul_distr_l
remove prop Mul_distr_r
remove prop Comm.Comm
remove prop Unitary
remove prop Inverse
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop ZeroLessOne
meta "encoding : kept" type real
end
(*
theory Bool
syntax type bool "Bool"
syntax function True "true"
syntax function False "false"
meta "encoding : kept" type bool
end
theory bool.Bool
syntax function andb "(and %1 %2)"
syntax function orb "(or %1 %2)"
syntax function xorb "(xor %1 %2)"
syntax function notb "(not %1)"
syntax function implb "(=> %1 %2)"
end
theory bool.Ite
syntax function ite "(ite %1 %2 %3)"
meta "encoding : lskept" function ite
end
*)
import "discrimination.gen"
......@@ -105,6 +105,17 @@ version_old = "1.0"
driver = "drivers/cvc4.drv"
command = "%l/why3-cpulimit %t %m -s %e --lang=smt2 %f"
# Psyche version 2.x
[ATP psyche]
name = "Psyche"
exec = "psyche"
exec = "psyche-2.02"
version_switch = "-version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok = "2.0"
driver = "drivers/psyche.drv"
command = "%l/why3-cpulimit %t %m -s %e -gplugin dpll_wl %f"
# CVC3 versions 2.4.x
[ATP cvc3]
name = "CVC3"
......
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