- still working on infering branching structure

9 files changed, 258 insertions, 127 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index c02e290e..e14d2d06 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -75,6 +75,7 @@ let rec IsArgsOnly args expr =
   | IntLiteral(_)                        -> true

   | BoolLiteral(_)                       -> true

   | Star                                 -> true

+  | VarLiteral(id)

   | IdLiteral(id)                        -> args |> List.exists (function Var(varName,_) when varName = id -> true | _ -> false)

   | UnaryExpr(_,e)                       -> IsArgsOnly args e

   | BinaryExpr(_,_,e1,e2)                -> (IsArgsOnly args e1) && (IsArgsOnly args e2)

@@ -106,6 +107,7 @@ let GetUnifications expr args (heap,env,ctx) =
     match expr with

     | IntLiteral(_)

     | BoolLiteral(_)

+    | VarLiteral(_)

     | IdLiteral(_)

     | Star                   -> unifs

     | Dot(e, _)

@@ -191,7 +193,7 @@ let GetObjRefExpr o (heap,env,ctx) =
 //  =======================================================

 let rec ApplyUnifications prog comp mthd unifs (heap,env,ctx) conservative = 

   let __CheckUnif o f e idx =

-    if not conservative then 

+    if not conservative || not Options.CONFIG.checkUnifications then 

       true 

     else

       let objRefExpr = GetObjRefExpr o (heap,env,ctx) |> Utils.ExtractOptionMsg ("Couldn't find a path from 'this' to " + (PrintObjRefName o (env,ctx)))

@@ -262,9 +264,26 @@ let VerifySolution prog comp mthd (heap,env,ctx) =
 let TryInferConditionals prog comp m unifs (heap,env,ctx) = 

   let heap2,env2,ctx2 = ApplyUnifications prog comp m unifs (heap,env,ctx) false

   // get expressions to evaluate:

-  //   - go through all objects on the heap and assert its invariant

   //   - add pre and post conditions

-

+  //   - go through all objects on the heap and assert its invariant  

+  let pre,post = GetMethodPrePost m

+  let prepostExpr = post |> RewriteMethodArgs (GetMethodArgs m) //TODO: do we need the "pre" here as well?

+  let heapObjs = heap |> Map.fold (fun acc (o,_) _ -> acc |> Set.add o) Set.empty

+  let expr = heapObjs |> Set.fold (fun acc o -> 

+                                     let receiverOpt = GetObjRefExpr o (heap,env,ctx) 

+                                     let receiver = Utils.ExtractOption receiverOpt

+                                     match Resolve (env,ctx) o with

+                                     | NewObj(_,tOpt) | ThisConst(_,tOpt) ->

+                                         let t = Utils.ExtractOptionMsg "Type missing for heap object" tOpt

+                                         let objComp = FindComponent prog (GetTypeShortName t) |> Utils.ExtractOption

+                                         let objInvs = GetInvariantsAsList objComp

+                                         let objInvsUpdated = objInvs |> List.map (ChangeThisReceiver receiver)

+                                         objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

+                                     | _ -> failwith "not supposed to happen"

+                                  ) prepostExpr

+  expr |> SplitIntoConjunts |> List.iter (fun e -> printfn "%s" (PrintExpr 0 e); printfn "")

+  // now evaluate and see what's left

+  let c = Eval (heap,env,ctx) expr

   Some(heap2,env2,ctx2)

    

 //  ============================================================================

diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index 86f6861f..eeb34a8d 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -21,10 +21,15 @@ type Type =
 type VarDecl =

   | Var of string * Type option

 

+(* 

+   the difference between IdLiteral and VarLiteral is that the VarLiteral is more specific, 

+   it always referes to a local variable (either method parameter or quantification variable)  

+ *)

 type Expr =

   | IntLiteral of int

   | BoolLiteral of bool

-  | IdLiteral of string

+  | VarLiteral of string  

+  | IdLiteral of string  

   | Star

   | Dot of Expr * string

   | UnaryExpr of string * Expr

@@ -72,5 +77,6 @@ type Const =
   | NoneConst

   | ThisConst  of (* loc id *) string * Type option

   | NewObj     of (* loc id *) string * Type option

+  | VarConst   of (* loc id *) string * Type option

   | ExprConst  of Expr

   | Unresolved of (* loc id *) string 
\ No newline at end of file
diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 4f8b4099..b81fd807 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -15,17 +15,19 @@ let rec VisitExpr visitorFunc expr acc =
   match expr with

   | IntLiteral(_)

   | BoolLiteral(_)

-  | IdLiteral(_)

+  | VarLiteral(_)

+  | IdLiteral(_)  

   | Star                             -> acc |> visitorFunc expr

-  | Dot(e, _)                        -> acc |> visitorFunc expr |> VisitExpr visitorFunc e

-  | SelectExpr(e1, e2)               -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2

-  | UpdateExpr(e1, e2, e3)           -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3

-  | SequenceExpr(exs) | SetExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)

+  | Dot(e, _)

+  | ForallExpr(_,e)                  

+  | UnaryExpr(_,e)                   

   | SeqLength(e)                     -> acc |> visitorFunc expr |> VisitExpr visitorFunc e

-  | ForallExpr(_,e)                  -> acc |> visitorFunc expr |> VisitExpr visitorFunc e

-  | UnaryExpr(_,e)                   -> acc |> visitorFunc expr |> VisitExpr visitorFunc e

+  | SelectExpr(e1, e2)               

   | BinaryExpr(_,_,e1,e2)            -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2

-  | IteExpr(c,e1,e2)                 -> acc |> visitorFunc expr |> VisitExpr visitorFunc c |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2

+  | IteExpr(e1,e2,e3)                 

+  | UpdateExpr(e1,e2,e3)             -> acc |> visitorFunc expr |> VisitExpr visitorFunc e1 |> VisitExpr visitorFunc e2 |> VisitExpr visitorFunc e3

+  | SequenceExpr(exs) | SetExpr(exs) -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)

+  

 

 // ------------------------------- End Visitor Stuff -------------------------------------------

 

@@ -33,110 +35,155 @@ exception EvalFailed
 

 let DefaultResolver e = ExprConst(e)

 

-let rec EvalSym resolverFunc expr = 

-  match expr with

-  | IntLiteral(n) -> IntConst(n)

-  | IdLiteral(_) | Dot(_) -> resolverFunc expr

-  | SeqLength(e) -> 

-      match EvalSym resolverFunc e with

-      | SeqConst(clist) -> IntConst(List.length clist)

-      | _ -> resolverFunc expr

-  | SequenceExpr(elist) -> 

-      let clist = elist |> List.fold (fun acc e -> EvalSym resolverFunc e :: acc) [] |> List.rev

-      SeqConst(clist)

-  | SelectExpr(lst, idx) ->

-      match EvalSym resolverFunc lst, EvalSym resolverFunc idx with

-      | SeqConst(clist), IntConst(n) -> clist.[n] 

-      | _ -> resolverFunc expr

-  | UpdateExpr(lst,idx,v) ->

-      match EvalSym resolverFunc lst, EvalSym resolverFunc idx, EvalSym resolverFunc v with

-      | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist)

-      | _ -> resolverFunc expr

-  | BinaryExpr(_,op,e1,e2) ->

-      match op with

-      | "=" ->

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)

-          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 = n2)

-          | ExprConst(e1), ExprConst(e2)   -> BoolConst(e1 = e2)

-          | _ -> resolverFunc expr

-      | "!=" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2))

-          | IntConst(n1), IntConst(n2)   -> BoolConst(not (n1 = n2))

-          | ExprConst(e1), ExprConst(e2)   -> BoolConst(not (e1 = e2))

-          | _ -> resolverFunc expr

-      | "<" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 < n2)

-          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) < (Set.count s2))

-          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) < (List.length s2))

-          | _ -> resolverFunc expr

-      | "<=" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 <= n2)

-          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) <= (Set.count s2))

-          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) <= (List.length s2))

-          | _ -> resolverFunc expr

-      | ">" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 > n2)

-          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) > (Set.count s2))

-          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) > (List.length s2))

-          | _ -> resolverFunc expr

-      | ">=" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2)   -> BoolConst(n1 >= n2)

-          | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) >= (Set.count s2))

-          | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) >= (List.length s2))

-          | _ -> resolverFunc expr

-      | "in" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | _ as c, SetConst(s)   -> BoolConst(Set.contains c s)

-          | _ as c, SeqConst(s)   -> BoolConst(Utils.ListContains c s)

-          | _ -> resolverFunc expr

-      | "!in" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | _ as c, SetConst(s)   -> BoolConst(not (Set.contains c s))

-          | _ as c, SeqConst(s)   -> BoolConst(not (Utils.ListContains c s))

-          | _ -> resolverFunc expr

-      | "+" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)

-          | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)

-          | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)

-          | q,w -> resolverFunc expr

-      | "-" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)

-          | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2)

-          | _ -> resolverFunc expr

-      | "*" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2)

-          | _ -> resolverFunc expr

-      | "div" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2)

-          | _ -> resolverFunc expr

-      | "mod" -> 

-          match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

-          | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2)

-          | _ -> resolverFunc expr

-      | _ -> resolverFunc expr

-  | UnaryExpr(op, e) ->

-      match op with

-      | "!" -> 

-          match EvalSym resolverFunc e with

-          | BoolConst(b) -> BoolConst(not b)

-          | _ -> resolverFunc expr

-      | "-" -> 

-          match EvalSym resolverFunc e with

-          | IntConst(n) -> IntConst(-n)

-          | _ -> resolverFunc expr

-      | _ -> resolverFunc expr

-  | _ -> resolverFunc expr

- 

+let EvalSym resolverFunc expr = 

+  let rec __EvalSym ctx expr = 

+    match expr with

+    | IntLiteral(n) -> IntConst(n)

+    | IdLiteral(_) | Dot(_) -> resolverFunc expr

+    | SeqLength(e) -> 

+        match __EvalSym ctx e with

+        | SeqConst(clist) -> IntConst(List.length clist)

+        | _ -> resolverFunc expr

+    | SequenceExpr(elist) -> 

+        let clist = elist |> List.fold (fun acc e -> __EvalSym ctx e :: acc) [] |> List.rev

+        SeqConst(clist)

+    | SetExpr(eset) -> 

+        let cset = eset |> List.fold (fun acc e -> Set.add (__EvalSym ctx e) acc) Set.empty

+        SetConst(cset)

+    | SelectExpr(lst, idx) ->

+        match __EvalSym ctx lst, __EvalSym ctx idx with

+        | SeqConst(clist), IntConst(n) -> clist.[n] 

+        | _ -> resolverFunc expr

+    | UpdateExpr(lst,idx,v) ->

+        match __EvalSym ctx lst, __EvalSym ctx idx, __EvalSym ctx v with

+        | SeqConst(clist), IntConst(n), (_ as c) -> SeqConst(Utils.ListSet n (c) clist)

+        | _ -> resolverFunc expr

+    | IteExpr(c, e1, e2) ->

+       match __EvalSym ctx c with

+       | BoolConst(b) -> if b then __EvalSym ctx e1 else __EvalSym ctx e2

+       | _ -> resolverFunc expr

+    | BinaryExpr(_,op,e1,e2) ->

+        match op with

+        | "=" ->

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)

+            | IntConst(n1), IntConst(n2)   -> BoolConst(n1 = n2)

+            | ExprConst(e1), ExprConst(e2)   -> BoolConst(e1 = e2)

+            | _ -> resolverFunc expr

+        | "!=" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | BoolConst(b1), BoolConst(b2) -> BoolConst(not (b1 = b2))

+            | IntConst(n1), IntConst(n2)   -> BoolConst(not (n1 = n2))

+            | ExprConst(e1), ExprConst(e2)   -> BoolConst(not (e1 = e2))

+            | _ -> resolverFunc expr

+        | "<" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2)   -> BoolConst(n1 < n2)

+            | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) < (Set.count s2))

+            | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) < (List.length s2))

+            | _ -> resolverFunc expr

+        | "<=" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2)   -> BoolConst(n1 <= n2)

+            | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) <= (Set.count s2))

+            | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) <= (List.length s2))

+            | _ -> resolverFunc expr

+        | ">" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2)   -> BoolConst(n1 > n2)

+            | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) > (Set.count s2))

+            | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) > (List.length s2))

+            | _ -> resolverFunc expr

+        | ">=" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2)   -> BoolConst(n1 >= n2)

+            | SetConst(s1), SetConst(s2)   -> BoolConst((Set.count s1) >= (Set.count s2))

+            | SeqConst(s1), SeqConst(s2)   -> BoolConst((List.length s1) >= (List.length s2))

+            | _ -> resolverFunc expr

+        | "in" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | _ as c, SetConst(s)   -> BoolConst(Set.contains c s)

+            | _ as c, SeqConst(s)   -> BoolConst(Utils.ListContains c s)

+            | _ -> resolverFunc expr

+        | "!in" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | _ as c, SetConst(s)   -> BoolConst(not (Set.contains c s))

+            | _ as c, SeqConst(s)   -> BoolConst(not (Utils.ListContains c s))

+            | _ -> resolverFunc expr

+        | "+" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)

+            | SeqConst(l1), SeqConst(l2) -> SeqConst(List.append l1 l2)

+            | SetConst(s1), SetConst(s2) -> SetConst(Set.union s1 s2)

+            | q,w -> resolverFunc expr

+        | "-" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2) -> IntConst(n1 + n2)

+            | SetConst(s1), SetConst(s2) -> SetConst(Set.difference s1 s2)

+            | _ -> resolverFunc expr

+        | "*" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2) -> IntConst(n1 * n2)

+            | _ -> resolverFunc expr

+        | "div" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2) -> IntConst(n1 / n2)

+            | _ -> resolverFunc expr

+        | "mod" -> 

+            match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | IntConst(n1), IntConst(n2) -> IntConst(n1 % n2)

+            | _ -> resolverFunc expr

+        | "&&" -> 

+           match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 && b2)

+            | _ -> resolverFunc expr

+        | "||" -> 

+           match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 || b2)

+            | _ -> resolverFunc expr

+        | "==>" -> 

+           match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | BoolConst(b1), BoolConst(b2) -> BoolConst((not b1) || b2)

+            | _ -> resolverFunc expr

+        | "<==>" -> 

+           match __EvalSym ctx e1, __EvalSym ctx e2 with

+            | BoolConst(b1), BoolConst(b2) -> BoolConst(b1 = b2)

+            | _ -> resolverFunc expr

+        | _ -> resolverFunc expr

+    | UnaryExpr(op, e) ->

+        match op with

+        | "!" -> 

+            match __EvalSym ctx e with

+            | BoolConst(b) -> BoolConst(not b)

+            | _ -> resolverFunc expr

+        | "-" -> 

+            match __EvalSym ctx e with

+            | IntConst(n) -> IntConst(-n)

+            | _ -> resolverFunc expr

+        | _ -> resolverFunc expr

+    | ForallExpr(vars, e) -> 

+        let rec PrintSep sep f list =
+          match list with
+          | [] -> ""
+          | [a] -> f a
+          | a :: more -> (f a) + sep + (PrintSep sep f more)

+        let rec PrintType ty =
+          match ty with
+          | IntType                   -> "int"
+          | BoolType                  -> "bool"
+          | NamedType(id, args)       -> if List.isEmpty args then id else (PrintSep ", " (fun s -> s) args)
+          | SeqType(t)                -> sprintf "seq[%s]" (PrintType t)
+          | SetType(t)                -> sprintf "set[%s]" (PrintType t)
+          | InstantiatedType(id,args) -> sprintf "%s[%s]" id (PrintSep ", " (fun a -> PrintType a) args)

+        let PrintVarDecl vd =
+          match vd with
+          | Var(id,None) -> id
+          | Var(id,Some(ty)) -> sprintf "%s: %s" id (PrintType ty)

+        vars |> List.iter (fun v -> printfn "%s" (PrintVarDecl v))

+        resolverFunc expr

+    | _ -> resolverFunc expr  

+  __EvalSym [] expr 

+

 //  =======================================

 /// Converts a given constant to expression

 //  =======================================

@@ -319,8 +366,7 @@ let rec GetTypeShortName ty =
   | BoolType -> "bool"

   | SetType(_) -> "set"

   | SeqType(_) -> "seq"

-  | NamedType(n,_) -> n

-  | InstantiatedType(n,_) -> n

+  | NamedType(n,_) | InstantiatedType(n,_) -> n

 

 //  ==============================================================

 /// Returns all invariants of a component as a list of expressions

@@ -384,7 +430,8 @@ let rec Desugar expr =
   match expr with

   | IntLiteral(_)          

   | BoolLiteral(_)  

-  | IdLiteral(_)           

+  | IdLiteral(_)   

+  | VarLiteral(_)        

   | Star                   

   | Dot(_)                 

   | SelectExpr(_) 

@@ -425,3 +472,49 @@ let rec DesugarLst exprLst =
   | expr :: rest -> Desugar expr :: DesugarLst rest

   | [] -> []

 

+let ChangeThisReceiver receiver expr = 

+  let rec __ChangeThis locals expr = 

+    match expr with

+    | IntLiteral(_)

+    | BoolLiteral(_)                   

+    | Star                             

+    | VarLiteral(_)

+    | IdLiteral("null")                -> expr

+    | IdLiteral("this")                -> receiver

+    | IdLiteral(id)                    -> if Set.contains id locals then VarLiteral(id) else __ChangeThis locals (Dot(IdLiteral("this"), id))

+    | Dot(e, id)                       -> Dot(__ChangeThis locals e, id)

+    | ForallExpr(vars,e)               -> let newLocals = vars |> List.map (function Var(name,_) -> name) |> Set.ofList |> Set.union locals

+                                          ForallExpr(vars, __ChangeThis newLocals e)   

+    | UnaryExpr(op,e)                  -> UnaryExpr(op, __ChangeThis locals e)

+    | SeqLength(e)                     -> SeqLength(__ChangeThis locals e)

+    | SelectExpr(e1, e2)               -> SelectExpr(__ChangeThis locals e1, __ChangeThis locals e2)

+    | BinaryExpr(p,op,e1,e2)           -> BinaryExpr(p, op, __ChangeThis locals e1, __ChangeThis locals e2)

+    | IteExpr(e1,e2,e3)                -> IteExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

+    | UpdateExpr(e1,e2,e3)             -> UpdateExpr(__ChangeThis locals e1, __ChangeThis locals e2, __ChangeThis locals e3) 

+    | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map (__ChangeThis locals))

+    | SetExpr(exs)                     -> SetExpr(exs |> List.map (__ChangeThis locals))

+  (* function body starts here *)

+  __ChangeThis Set.empty expr

+

+let rec Rewrite rewriterFunc expr = 

+  match expr with

+  | IntLiteral(_)

+  | BoolLiteral(_)                   

+  | Star      

+  | VarLiteral(_)                       

+  | IdLiteral(_)                     -> rewriterFunc expr

+  | Dot(e, id)                       -> Dot(rewriterFunc e, id)

+  | ForallExpr(vars,e)               -> ForallExpr(vars, rewriterFunc e)   

+  | UnaryExpr(op,e)                  -> UnaryExpr(op, rewriterFunc e)

+  | SeqLength(e)                     -> SeqLength(rewriterFunc e)

+  | SelectExpr(e1, e2)               -> SelectExpr(rewriterFunc e1, rewriterFunc e2)

+  | BinaryExpr(p,op,e1,e2)           -> BinaryExpr(p, op, rewriterFunc e1, rewriterFunc e2)

+  | IteExpr(e1,e2,e3)                -> IteExpr(rewriterFunc e1, rewriterFunc e2, rewriterFunc e3) 

+  | UpdateExpr(e1,e2,e3)             -> UpdateExpr(rewriterFunc e1, rewriterFunc e2, rewriterFunc e3) 

+  | SequenceExpr(exs)                -> SequenceExpr(exs |> List.map rewriterFunc)

+  | SetExpr(exs)                     -> SetExpr(exs |> List.map rewriterFunc)

+

+let RewriteMethodArgs args expr = 

+  let __IdIsArg id = args |> List.exists (function Var(name,_) -> name = id)

+  Rewrite (function IdLiteral(id) when __IdIsArg id -> VarLiteral(id) | _ as e -> e) expr

+              
\ No newline at end of file
diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index c13b94d2..f0e59d3b 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -150,5 +150,4 @@ let PrintImplCode prog solutions methodsToPrintFunc =
                                                   | _ -> "    //unable to synthesize" + newline

                                    (GenConstructorCode mthd mthdBody) + newline

                                  else

-                                   ""

-                              )
\ No newline at end of file
+                                   "")
\ No newline at end of file
diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index 9ef9e74a..05f333d1 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -16,6 +16,7 @@ let rec PrintExpr ctx expr =
   match expr with
   | IntLiteral(n) -> sprintf "%d" n
   | BoolLiteral(b) -> sprintf "%b" b
+  | VarLiteral(id)
   | IdLiteral(id) -> id
   | Star -> assert false; "" // I hope this won't happen
   | Dot(e,id) -> sprintf "%s.%s" (PrintExpr 100 e) id
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 17c74563..832176fd 100644
--- a/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

     <DocumentationFile>bin\Debug\Language.XML</DocumentationFile>

-    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double</StartArguments>

+    <StartArguments>C:\boogie\Jennisys\Jennisys\examples\Set.jen /method:Set.Double /noCheckUnifs</StartArguments>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|x86' ">

     <DebugType>pdbonly</DebugType>

diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs
index 291bd678..4a1487ce 100644
--- a/Jennisys/Options.fs
+++ b/Jennisys/Options.fs
@@ -12,14 +12,16 @@ type Config = {
    inputFilename: string;

    methodToSynth: string;

    verifySolutions: bool;

+   checkUnifications: bool;

    timeout: int;

 }

 

 let defaultConfig: Config = {

-  inputFilename   = "";

-  methodToSynth   = "*";

-  verifySolutions = true;

-  timeout         = 0;

+  inputFilename     = "";

+  methodToSynth     = "*";

+  verifySolutions   = true;

+  checkUnifications = true;

+  timeout           = 0;

 }

 

 let mutable CONFIG = defaultConfig

@@ -79,6 +81,15 @@ let ParseCmdLineArgs args =
         | "verifySol" -> 

             let b = __CheckBool value opt

             __Parse rest { cfg with verifySolutions = b }

+        | "noVerifySol" -> 

+            let b = __CheckBool value opt

+            __Parse rest { cfg with verifySolutions = not b }

+        | "checkUnifs" -> 

+            let b = __CheckBool value opt

+            __Parse rest { cfg with checkUnifications = b }

+        | "noCheckUnifs" -> 

+            let b = __CheckBool value opt

+            __Parse rest { cfg with checkUnifications = not b }

         | "timeout" ->

             let t = __CheckInt value opt

             __Parse rest { cfg with timeout = t }

diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index 53bf6b6d..54d0dc43 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -36,6 +36,7 @@ let rec PrintExpr ctx expr =
   match expr with
   | IntLiteral(n)     -> sprintf "%d" n
   | BoolLiteral(b)    -> sprintf "%b" b
+  | VarLiteral(id) 
   | IdLiteral(id)     -> id
   | Star              -> "*"
   | Dot(e,id)         -> sprintf "%s.%s" (PrintExpr 100 e) id
diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index 59c6904d..fac29fba 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -70,7 +70,8 @@ let Resolve (env,ctx) cst =
 let Eval (heap,env,ctx) expr = 

   let rec __EvalResolver expr = 

     match expr with

-    | IdLiteral(id) when id = "this" -> GetThisLoc env

+    | VarLiteral(id) -> ExprConst(expr)

+    | IdLiteral("this") -> GetThisLoc env

     | IdLiteral(id) ->

         match TryResolve (env,ctx) (Unresolved(id)) with 

         | Unresolved(_) -> __EvalResolver (Dot(IdLiteral("this"), id))