Commit 13b02f7e authored by Sylvain Dailler's avatar Sylvain Dailler

ce-bench: Add algebraic and polymorphism examples

parent 03735a10
......@@ -5,6 +5,33 @@ module M
goal G : forall x : int_type. match x with Integer y -> y > 0 end
type t = A | B int
goal g2: forall x. x = A
goal g4: forall x. x = B 0
type u = Au int int
goal g5: forall x. x = Au 0 0
type mylist = | Nil | Cons int mylist
let rec function len l = match l with
| Nil -> 0
| Cons _ l' -> 1 + len l'
end
goal g1: forall l: mylist. len l = 0
goal g7: forall l: mylist. l = Nil
(* use list.List
use list.Length
goal g: forall l: list int. length l = 0
*)
(*
(*********************************
** Non-terminating projections **
......
......@@ -5,3 +5,21 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g2: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Timeout or Unknown
bench/ce/algebraic_type.mlw M g5: Timeout or Unknown
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "0" },
{"type" : "Integer" ,
"val" : "1" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
......@@ -5,3 +5,21 @@ x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Integer" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g2: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 10:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g4: Unknown (sat)
bench/ce/algebraic_type.mlw M g5: Unknown (sat)
Counter-example model:File algebraic_type.mlw:
Line 16:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "Au" , "list" : [{"type" : "Integer" , "val" : "1" },
{"type" : "Integer" ,
"val" : "0" }] } }
bench/ce/algebraic_type.mlw M g1: Timeout or Unknown
bench/ce/algebraic_type.mlw M g7: Timeout or Unknown
module Test
type mono = B int
goal gm: forall x: mono. x = B 0
type mono2 = C int bool
goal gm2: forall x. x = C 0 false
type poly 'a = A 'a
goal g: forall x: poly int. x = A 0
end
\ No newline at end of file
bench/ce/polymorphism.mlw Test gm: Unknown (sat)
Counter-example model:File polymorphism.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "1" }] } }
bench/ce/polymorphism.mlw Test gm2: Unknown (sat)
Counter-example model:File polymorphism.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "C" , "list" : [{"type" : "Integer" , "val" : "0" },
{"type" : "Boolean" ,
"val" : true }] } }
bench/ce/polymorphism.mlw Test g: Timeout or Unknown
bench/ce/polymorphism.mlw Test gm: Unknown (sat)
Counter-example model:File polymorphism.mlw:
Line 7:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "B" , "list" : [{"type" : "Integer" ,
"val" : "1" }] } }
bench/ce/polymorphism.mlw Test gm2: Unknown (sat)
Counter-example model:File polymorphism.mlw:
Line 11:
x, [[@introduced], [@model_trace:x]] = {"type" : "Apply" ,
"val" : {"apply" : "C" , "list" : [{"type" : "Integer" , "val" : "1" },
{"type" : "Boolean" ,
"val" : false }] } }
bench/ce/polymorphism.mlw Test g: Timeout or Unknown
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