Ajout des reals en builtin pour cvc3 et z3

.gitignore

 *.o
 *.svn
 .*.swp
+
 # /
 /config.status
 /config.log
@@ -32,6 +33,7 @@
 /bin/whyide.byte
 /bin/whyide.opt
 /bin/why-cpulimit
+/bin/why3-cpulimit
 /bin/manager.byte
 /bin/manager.opt
 /bin/tptp2why.byte

drivers/cvc3.drv

@@ -59,6 +59,55 @@ theory int.Int
   remove prop Total
 end
 
+theory real.Real
+
+  prelude ";;; this is a prelude for Z3, 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 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 Inverse
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+
+end
+
+(*
+(* L'encodage des types sommes bloquent cette théorie builtin *)
+theory bool.Bool
+   syntax type bool "bool"
+   tag cloned type bool "encoding_decorate : kept"
+   syntax logic True "true"
+   syntax logic False "false"
+   syntax logic andb "(and %1 %2)"
+   syntax logic orb "(or %1 %2)"
+   syntax logic xorb "(xor %1 %2)"
+   syntax logic notb "(not %1)" 
+end
+*)
+
+
 theory transform.encoding_decorate.Kept
   tag cloned type t "encoding_decorate : kept"
 end

drivers/cvc3_inst.drv

+
+(* Why driver for SMT syntax *)
+
+prelude ";;; this is a prelude for CVC3 "
+
+printer "smtv1"
+filename "%f-%t-%g.smt"
+
+valid "unsat"
+unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
+
+(* À 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 "encoding_instantiate"
+
+theory BuiltIn
+  syntax type int "Int"
+  syntax type real "Real"
+  syntax logic (_=_) "(= %1 %2)"
+  syntax logic (_<>_) "(not (= %1 %2))"
+end
+
+theory int.Int
+
+  prelude ";;; this is a prelude for CVC3, Arithmetic"
+
+  syntax logic zero "0"
+
+  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 Antisymm
+  remove prop Total
+end
+
+theory real.Real
+
+  prelude ";;; this is a prelude for Z3, 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 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 Inverse
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+
+end
+
+(*
+(* L'encodage des types sommes bloquent cette théorie builtin *)
+theory bool.Bool
+   syntax type bool "bool"
+   tag cloned type bool "encoding_decorate : kept"
+   syntax logic True "true"
+   syntax logic False "false"
+   syntax logic andb "(and %1 %2)"
+   syntax logic orb "(or %1 %2)"
+   syntax logic xorb "(xor %1 %2)"
+   syntax logic notb "(not %1)" 
+end
+*)
+
+
+theory transform.encoding_decorate.Kept
+  tag cloned type t "encoding_decorate : kept"
+end
+
+(*
+Local Variables: 
+mode: why
+compile-command: "make -C ../.. bench"
+End: 
+*)

drivers/z3.drv

@@ -63,6 +63,56 @@ theory int.Int
 
 end
 
+
+theory real.Real
+
+  prelude ";;; this is a prelude for Z3, 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 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 Inverse
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+
+end
+
+(*
+(* L'encodage des types sommes bloquent cette théorie builtin *)
+theory bool.Bool
+   syntax type bool "bool"
+   tag cloned type bool "encoding_decorate : kept"
+   syntax logic True "true"
+   syntax logic False "false"
+   syntax logic andb "(and %1 %2)"
+   syntax logic orb "(or %1 %2)"
+   syntax logic xorb "(xor %1 %2)"
+   syntax logic notb "(not %1)" 
+end
+*)
+
+
 theory int.EuclideanDivision
    syntax logic div "(div %1 %2)"
    syntax logic mod "(mod %1 %2)"

drivers/z3_inst.drv

+
+(* Why driver for SMT syntax *)
+
+prelude ";;; this is a prelude for Z3"
+
+printer "smtv1"
+filename "%f-%t-%g.smt"
+
+valid "^unsat"
+unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
+
+(* À 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 "encoding_instantiate"
+(* transformation "encoding_decorate_every_simple" *)
+
+
+theory BuiltIn
+  syntax type int "Int"
+  syntax type real "Real"
+  syntax logic (_=_) "(= %1 %2)"
+  syntax logic (_<>_) "(not (= %1 %2))"
+end
+
+
+theory int.Int
+
+  prelude ";;; this is a prelude for Z3, Arithmetic"
+
+  syntax logic zero "0"
+
+  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 Antisymm
+  remove prop Total
+
+end
+
+
+theory real.Real
+
+  prelude ";;; this is a prelude for Z3, 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 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 Inverse
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+
+end
+
+(*
+(* L'encodage des types sommes bloquent cette théorie builtin *)
+theory bool.Bool
+   syntax type bool "bool"
+   tag cloned type bool "encoding_decorate : kept"
+   syntax logic True "true"
+   syntax logic False "false"
+   syntax logic andb "(and %1 %2)"
+   syntax logic orb "(or %1 %2)"
+   syntax logic xorb "(xor %1 %2)"
+   syntax logic notb "(not %1)" 
+end
+*)
+
+
+theory int.EuclideanDivision
+   syntax logic div "(div %1 %2)"
+   syntax logic mod "(mod %1 %2)"
+   remove prop Mod_bound
+   remove prop Div_mod
+   remove prop Mod_1
+   remove prop Div_1
+end
+
+theory transform.encoding_decorate.Kept
+  tag cloned type t "encoding_decorate : kept"
+end
+
+(*
+Local Variables: 
+mode: why
+compile-command: "unset LANG; make -C .. bench"
+End: 
+*)

src/printer/smt.ml

@@ -64,8 +64,10 @@ let print_type drv fmt = catch_unsupportedType (print_type drv fmt)
 
 let rec print_term drv fmt t = match t.t_node with
   | Tbvar _ -> assert false
-  | Tconst c ->
-      Pretty.print_const fmt c
+  | Tconst (ConstInt n) -> fprintf fmt "%s" n
+  | Tconst (ConstReal c) ->
+      Print_real.print_with_integers 
+	"%s.0" "(* %s.0 %s.0)" "(/ %s.0 %s.0)" fmt c
   | Tvar v -> print_var fmt v
   | Tapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
       | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl

tests/test-bobot.why

@@ -85,6 +85,19 @@ theory TestIte
   goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0 
 end
 
+theory TestBuiltin_real
+  use import real.Real
+  goal G1 : 5.5 * 10. = 55. 
+  goal G2 : 9. / 3. = 3. 
+  goal G3 : inv(5.) = 0.2
+end
+
+theory TestBuiltin_bool
+  use import bool.Bool
+  goal G : xorb(True,False) = True 
+end
+
+
 (*
 Local Variables: 
 compile-command: "make -C .. test"