driver for Alt-Ergo with SMT-lib2 input format (not in provers-detection-data)

parent ceab2013
(* Why driver for Alt-Ergo with SMT-lib2 input format *)
prelude ";;; this is a prelude for Alt-Ergo"
printer "smtv2"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
time "why3cpulimit time : %s s"
transformation "simplify_recursive_definition"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
transformation "eliminate_let"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "encoding_smt"
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (=) "(= %1 %2)"
meta "encoding : kept" type int
end
theory int.Int
prelude ";;; this is a prelude for Alt-Ergo integer arithmetic"
syntax logic zero "0"
syntax logic one "1"
syntax logic (+) "(+ %1 %2)"
syntax logic (-) "(- %1 %2)"
syntax logic (*) "(* %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Total
remove prop Antisymm
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
theory int.EuclideanDivision
syntax logic div "(div %1 %2)"
syntax logic mod "(mod %1 %2)"
end
theory real.Real
prelude ";;; this is a prelude for Alt-Ergo real arithmetic"
syntax logic zero "0.0"
syntax logic one "1.0"
syntax logic (+) "(+ %1 %2)"
syntax logic (-) "(- %1 %2)"
syntax logic (*) "(* %1 %2)"
syntax logic (/) "(/ %1 %2)"
syntax logic (-_) "(- %1)"
syntax logic inv "(/ 1.0 %1)"
syntax logic (<=) "(<= %1 %2)"
syntax logic (<) "(< %1 %2)"
syntax logic (>=) "(>= %1 %2)"
syntax logic (>) "(> %1 %2)"
remove prop CommutativeGroup.Comm.Comm
remove prop CommutativeGroup.Assoc.Assoc
remove prop CommutativeGroup.Unit_def
remove prop CommutativeGroup.Inv_def
remove prop Assoc.Assoc
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Total
remove prop Antisymm
remove prop Inverse
remove prop NonTrivialRing
remove prop CompatOrderAdd
end
(*
Local Variables:
mode: why
compile-command: "make -C .. bench"
End:
*)
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