Commit ade3c20a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

drivers maintenant dans drivers/

parent 82e362d1
(* Why driver for Alt-Ergo *)
prelude "(* this is a prelude for Alt-Ergo*)"
printer "alt-ergo"
filename "%f-%t-%s.why"
call_on_file "alt-ergo %s"
valid "Valid"
invalid "Invalid"
unknown "I don't know" "Unknown"
fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
(* À discuter *)
transformations
"simplify_recursive_definition"
(*"split_goal_pos"*) "split_goal_pos_neg"
"inline_trivial"
end
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
end
theory prelude.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
syntax logic zero "0"
syntax logic (_+_) "(%1 + %2)"
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 One_neutral
remove prop Add_assoc
remove prop Add_comm
remove prop Zero_neutral
remove prop Neg
remove prop Mul_comm
remove prop Mul_assoc
remove prop Mul_distr
end
theory algebra.AC
tag cloned logic op "AC"
remove cloned prop Comm
remove cloned prop Assoc
end
(*
Local Variables:
mode: why
compile-command: "make -C ../.. bench"
End:
*)
(* Why driver for SMT syntax *)
prelude "(* this is a prelude for smtlib*)"
printer "smtv1"
filename "%f-%t-%s.smt"
call_on_stdin "cvc3 -lang smt"
valid "unsat"
unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
(* À discuter *)
transformations
"simplify_recursive_definition"
(*"split_goal_pos"*) "split_goal_pos_neg"
"inline_trivial"
"remove_logic_definition"
"encoding_decorate"
end
theory BuiltIn
syntax type int "Int"
syntax type real "Real"
syntax logic (_=_) "(= %1 %2)"
syntax logic (_<>_) "(not (= %1 %2))"
end
theory prelude.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
syntax logic zero "0"
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (_/_) "(div_int %1 %2)"
syntax logic (-_) "(-%1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
syntax logic (_>=_) "(>= %1 %2)"
syntax logic (_> _) "(> %1 %2)"
remove prop One_neutral
remove prop Add_assoc
remove prop Add_comm
remove prop Zero_neutral
remove prop Neg
remove prop Mul_comm
remove prop Mul_assoc
remove prop Mul_distr
end
theory algebra.AC
tag cloned logic op "AC"
remove cloned prop Comm
remove cloned prop Assoc
end
(*
Local Variables:
mode: why
compile-command: "make -C ../.. bench"
End:
*)
printer "why3"
filename "%f-%t-%s.why"
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
end
printer "why3"
filename "%f-%t-%s.why"
transformations
"remove_logic_definition"
"encoding_decorate"
end
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
end
printer "why3"
filename "%f-%t-%s.why"
(* À discuter *)
transformations
"simplify_recursive_definition"
"inline_all"
end
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
end
printer "why3"
filename "%f-%t-%s.why"
(* À discuter *)
transformations
"split_goal_pos_neg"
end
theory BuiltIn
syntax type int "int"
syntax type real "real"
syntax logic (_=_) "(%1 = %2)"
syntax logic (_<>_) "(%1 <> %2)"
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