Poor attempt to support MathSAT5 prover

Too bad, it does not seem to support quantifiers...

CHANGES

 * marks an incompatible change
 
+  * [prover] support for mathematica
+  * [prover] support for MathSAT5
+
 version 0.80, Oct 31, 2012
 ==========================
   * [whyml] modified syntax for mlw programs; a summary of changes is

drivers/mathsat.drv

+(* Why driver for SMT2 syntax *)
+
+prelude ";;; this is a prelude for MathSAT5"
+prelude "(set-logic AUFNIRA)"
+
+printer "smtv2"
+filename "%f-%t-%g.smt"
+
+valid "^unsat"
+unknown "^\\(unknown\\|sat\\|Fail\\)" ""
+outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
+time "why3cpulimit time : %s s"
+
+
+(* À discuter *)
+(*transformation "simplify_recursive_definition"*)
+transformation "inline_trivial"
+
+
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+theory BuiltIn
+  syntax type int   "Int"
+  syntax type real  "Real"
+  syntax predicate (=)  "(= %1 %2)"
+
+  meta "encoding : kept" type int
+end
+
+theory int.Int
+
+  prelude ";;; this is a prelude for Z3 integer arithmetic"
+
+  syntax function zero "0"
+  syntax function one  "1"
+
+  syntax function (+)  "(+ %1 %2)"
+  syntax function (-)  "(- %1 %2)"
+  syntax function (*)  "(* %1 %2)"
+  syntax function (-_) "(- %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 Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop ZeroLessOne
+
+end
+
+
+theory real.Real
+
+  prelude ";;; this is a prelude for Z3 real arithmetic"
+
+  syntax function zero "0.0"
+  syntax function one  "1.0"
+
+  syntax function (+)  "(+ %1 %2)"
+  syntax function (-)  "(- %1 %2)"
+  syntax function (*)  "(* %1 %2)"
+  syntax function (/)  "(/ %1 %2)"
+  syntax function (-_) "(- %1)"
+  syntax function inv  "(/ 1.0 %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 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 real.FromInt
+  syntax function from_int "(to_real %1)"
+  remove prop Zero
+  remove prop One
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+end
+
+(*
+theory real.Truncate
+  syntax function floor "(to_int %1)"
+  remove prop Floor_down
+  remove prop Floor_monotonic
+end
+*)
+
+theory map.Map
+  syntax type map "(Array %1 %2)"
+  meta "encoding : lskept" function get
+  meta "encoding : lskept" function set
+  meta "encoding : lskept" function const
+
+  syntax function get   "(select %1 %2)"
+  syntax function set   "(store %1 %2 %3)"
+(*  syntax function const "(const[%t0] %1)" *)
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End:
+*)

share/provers-detection-data.conf.in

@@ -173,6 +173,16 @@ version_ok = "0.14.1"
 command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -Eprecision=70"
 driver = "drivers/gappa.drv"
 
+[ATP mathsat]
+name = "MathSAT5"
+exec = "mathsat"
+version_switch = "-version"
+version_regexp = "MathSAT5 version \\([^ \n]+\\)"
+version_ok  = "5.2.2"
+command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e -input=smt2 -model -random_seed=80 %f"
+driver = "drivers/mathsat.drv"
+
+
 [ATP simplify]
 name = "Simplify"
 exec = "Simplify"