asymetric split in split_goal; syntax /\ and \/ for asymetric and and or

examples/programs/vacid_0_sparse_array.mlw

@@ -79,9 +79,9 @@ back  +-+-+-+-------------------+
     forall a : sparse_array . invariant a -> 
         let (SA val idx back sz n) = a in
         n = sz -> 
-            permutation sz back and
+            permutation sz back /\
             forall i : int. 0 <= i < sz ->
-                idx#i = dirichlet sz back i and is_elt a i
+                idx#i = dirichlet sz back i /\ is_elt a i
 }
 
 

src/parser/lexer.mll

@@ -189,6 +189,10 @@ rule token = parse
       { ARROW }
   | "<->"
       { LRARROW }
+  | "/\\"
+      { ASYM_AND }
+  | "\\/"
+      { ASYM_OR }
   | "."
       { DOT }
   | "|"

src/parser/parser.mly

@@ -67,7 +67,7 @@
 
 /* symbols */
 
-%token ARROW
+%token ARROW ASYM_AND ASYM_OR
 %token BAR
 %token COLON COMMA
 %token DOT EQUAL
@@ -90,8 +90,8 @@
 
 %nonassoc prec_named
 %right ARROW LRARROW
-%right OR
-%right AND
+%right OR ASYM_OR
+%right AND ASYM_AND
 %nonassoc NOT
 %left EQUAL OP1
 %left OP2
@@ -346,8 +346,12 @@ lexpr:
    { infix_pp $1 PPiff $3 }
 | lexpr OR lexpr
    { infix_pp $1 PPor $3 }
+| lexpr ASYM_OR lexpr
+   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPor $3)) }
 | lexpr AND lexpr
    { infix_pp $1 PPand $3 }
+| lexpr ASYM_AND lexpr
+   { mk_pp (PPnamed ("asym_split", infix_pp $1 PPand $3)) }
 | NOT lexpr
    { prefix_pp PPnot $2 }
 | lexpr EQUAL lexpr

src/programs/pgm_wp.ml

@@ -39,8 +39,9 @@ let debug = ref false
    TODO: use simp forms / tag with label "WP" *)
 
 let wp_and ?(sym=false) f1 f2 = 
-  (* TODO: tag instead? *)
-  if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2) 
+(*   if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2)  *)
+  let f = f_and_simp f1 f2 in
+  if sym then f else f_label [Split_goal.asym_split] f
 
 let wp_ands ?(sym=false) fl =
   List.fold_left (wp_and ~sym) f_true fl

src/transform/split_goal.ml

@@ -33,10 +33,14 @@ let split_case spl c acc tl bl =
   in
   apply_append (f_case tl) acc bll
 
+let asym_split = "asym_split"
+
 let rec split_pos acc f = match f.f_node with
   | Ftrue -> acc
   | Ffalse -> f::acc
   | Fapp _ -> f::acc
+  | Fbinop (Fand,f1,f2) when List.mem asym_split f.f_label ->
+      split_pos (split_pos acc (f_implies f1 f2)) f1
   | Fbinop (Fand,f1,f2) ->
       split_pos (split_pos acc f2) f1
   | Fbinop (Fimplies,f1,f2) ->
@@ -64,10 +68,14 @@ and split_neg acc f = match f.f_node with
   | Fapp _ -> f::acc
   | Fbinop (Fand,f1,f2) ->
       apply_append2 f_and acc (split_neg [] f1) (split_neg [] f2)
+  | Fbinop (Fimplies,f1,f2) when List.mem asym_split f.f_label ->
+      split_neg (split_neg acc (f_and f1 f2)) (f_not f1)
   | Fbinop (Fimplies,f1,f2) ->
       split_neg (split_neg acc f2) (f_not f1)
   | Fbinop (Fiff,f1,f2) ->
       split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f2 f1)
+  | Fbinop (For,f1,f2) when List.mem asym_split f.f_label ->
+      split_neg (split_neg acc (f_and (f_not f1) f2)) f1
   | Fbinop (For,f1,f2) ->
       split_neg (split_neg acc f2) f1
   | Fnot f ->

src/transform/split_goal.mli

@@ -17,6 +17,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val asym_split : Term.label
+
 val split_pos : Term.fmla list -> Term.fmla -> Term.fmla list
 val split_neg : Term.fmla list -> Term.fmla -> Term.fmla list
 

tests/test-jcf.why

 
 (* test file *)
 
-theory Test
-  use export int.Int
-  logic f(int) : int
-  logic q(int, int)
-  axiom A : forall x:int. q (-x) (f x)
-  goal G : 3.14 = 3.15
-end
-
-theory Test2
-  use export list.List
-  goal G : let x = Nil in let t = (Cons 1 x, Cons 3.14 x) in t=t
+theory S
+  use import int.Int
+  logic p int
+  goal G : forall x:int. (p 1 \/ p 2) -> p 3
 end