Commit 7283d40a authored by Daisuke Ishii's avatar Daisuke Ishii

add the Mathematica driver.

parent 89ad1fe4
......@@ -128,7 +128,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
eval_match instantiate_predicate smoke_detector
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs \
simplify gappa cvc3 yices
simplify gappa cvc3 yices mathematica
LIB_SESSION = xml termcode session session_tools session_scheduler
......
/Users/ishii/workspace/whybrid/tmp/math_driver/drivers/mathematica.drv
\ No newline at end of file
......@@ -313,6 +313,16 @@ command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e --fof true --out_options none \
\"eprover --cnf --tstp-format \" %f"
driver = "drivers/iprover.drv"
[ATP mathematica]
name = "Mathematica"
exec = "math"
version_switch = "-run \"Exit[]\""
version_regexp = "Mathematica \\([0-9.]+\\)"
version_ok = "8.0"
version_ok = "7.0"
command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -noprompt < %f"
driver = "drivers/mathematica.drv"
[ITP coq]
name = "Coq"
exec = "coqtop -batch"
......
/Users/ishii/workspace/whybrid/tmp/math_driver/src/printer/mathematica.ml
\ No newline at end of file
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