Ajout de benchs pour AC et division euclidean

.gitignore

@@ -58,6 +58,24 @@
 /doc/*.hind
 /doc/*.htoc
 
+# /drivers/
+/drivers/cvc3_inst.drv
+/drivers/cvc3_inst_nbp.drv
+/drivers/cvc3_inst_def.drv
+/drivers/cvc3_inst_def_nbp.drv
+/drivers/cvc3_inst_goal.drv
+/drivers/cvc3_inst_goal_nbp.drv
+/drivers/cvc3_inst_mono.drv
+/drivers/cvc3_inst_mono_nbp.drv
+/drivers/z3_inst.drv
+/drivers/z3_inst_nbp.drv
+/drivers/z3_inst_def.drv
+/drivers/z3_inst_def_nbp.drv
+/drivers/z3_inst_goal.drv
+/drivers/z3_inst_goal_nbp.drv
+/drivers/z3_inst_mono.drv
+/drivers/z3_inst_mono_nbp.drv
+
 # /share/
 /share/*.cm*
 /share/*.annot

bench/valid/ac.why

+theory Test
+       type t
+       logic f(t,t) : t
+       clone algebra.AC with type t = t, logic op = f
+       goal G1 : forall x,y : t. f(x,y) = f(y,x)
+       goal G2 : forall x,y,z : t. f(f(x,y),z) = f(x,f(y,z))
+end
\ No newline at end of file

bench/valid/euclideandivision.why

+theory Test
+       use import int.EuclideanDivision
+       goal G1 : mod(10,3) = 1
+       goal G2 : div(10,3) = 3
+end
\ No newline at end of file

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_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: 
-*)