- added Set.jen example

 - fixed implementation for sets
 - generalized unification rules
 - added command line options
 - removed the "Exact" active pattern for strings (the same thing is already supported by F#)
 - added a ternary if-then-else expression to Jennisys langauge and IteExpr and SetExpr to AST

16 files changed, 470 insertions, 179 deletions

diff --git a/Jennisys/Analyzer.fs b/Jennisys/Analyzer.fs
index 8737ad86..7b6527f9 100644
--- a/Jennisys/Analyzer.fs
+++ b/Jennisys/Analyzer.fs
@@ -72,49 +72,87 @@ let MethodAnalysisPrinter onlyForThisCompMethod assertion comp mthd =
 

 let rec IsArgsOnly args expr = 

   match expr with                                                

-  | IntLiteral(_) -> true

-  | BoolLiteral(_) -> true

-  | 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)

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

-  | SelectExpr(e1, e2) -> (IsArgsOnly args e1) && (IsArgsOnly args e2)

-  | UpdateExpr(e1, e2, e3) -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3)

-  | SequenceExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true

-  | SeqLength(e) -> IsArgsOnly args e

-  | ForallExpr(vars,e) -> IsArgsOnly (List.concat [args; vars]) e

-  | Star -> true

+  | IntLiteral(_)                        -> true

+  | BoolLiteral(_)                       -> true

+  | Star                                 -> true

+  | 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)

+  | IteExpr(c,e1,e2)                     -> (IsArgsOnly args c) && (IsArgsOnly args e1) && (IsArgsOnly args e2)

+  | Dot(e,_)                             -> IsArgsOnly args e

+  | SelectExpr(e1, e2)                   -> (IsArgsOnly args e1) && (IsArgsOnly args e2)

+  | UpdateExpr(e1, e2, e3)               -> (IsArgsOnly args e1) && (IsArgsOnly args e2) && (IsArgsOnly args e3)

+  | SequenceExpr(exprs) | SetExpr(exprs) -> exprs |> List.fold (fun acc e -> acc && (IsArgsOnly args e)) true

+  | SeqLength(e)                         -> IsArgsOnly args e

+  | ForallExpr(vars,e)                   -> IsArgsOnly (List.concat [args; vars]) e

 

-let rec GetUnifications expr args (heap,env,ctx) = 

-  match expr with

-  | IntLiteral(_)

-  | BoolLiteral(_)

-  | IdLiteral(_)

-  | Star         

-  | Dot(_)

-  | SelectExpr(_)   // TODO: handle select expr

-  | UpdateExpr(_)   // TODO: handle update expr

-  | SequenceExpr(_) 

-  | SeqLength(_)    

-  | ForallExpr(_)   // TODO: handle forall expr

-  | UnaryExpr(_)   -> Set.empty

-  | BinaryExpr(strength,op,e0,e1) ->

-      if op = "=" then

-        let v0 = Eval (heap,env,ctx) e0

-        let v1 = Eval (heap,env,ctx) e1

-        let argsOnly0 = IsArgsOnly args e0

-        let argsOnly1 = IsArgsOnly args e1

-        match v0,argsOnly1,argsOnly0,v1 with

-        | Some(c0),true,_,_ -> 

-               Logger.DebugLine ("      - adding unification " + (PrintConst c0) + " <--> " + (PrintExpr 0 e1));

-               Set.ofList [c0, e1]

-        | _,_,true,Some(c1) -> 

-               Logger.DebugLine ("      - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0));

-               Set.ofList [c1, e0]

-        | _ -> Logger.TraceLine ("      - couldn't unify anything from " + (PrintExpr 0 expr));

-               Set.empty

-      else 

-        GetUnifications e0 args (heap,env,ctx) |> Set.union (GetUnifications e1 args (heap,env,ctx))

+let GetUnifications expr args (heap,env,ctx) =

+  // - first looks if the give expression talks only about method arguments (args)

+  // - then checks if it doesn't already exist in the unification map

+  // - then it tries to evaluate it to a constant

+  // - if all of these succeed, it adds a unification rule e <--> val(e) to the given unifMap map

+  let __AddUnif e unifMap =

+    let builder = new CascadingBuilder<_>(unifMap)

+    builder {

+      let! argsOnly = IsArgsOnly args e |> Utils.BoolToOption

+      let! notAlreadyAdded = Map.tryFind e unifMap |> Utils.IsNoneOption |> Utils.BoolToOption

+      let! v = Eval (heap,env,ctx) e                       

+      Logger.DebugLine ("      - adding unification " + (PrintExpr 0 e) + " <--> " + (PrintConst v));

+      return Map.add e v unifMap

+    }

+  // just recurses on all expressions

+  let rec __GetUnifications expr args unifs = 

+    let unifs = __AddUnif expr unifs

+    match expr with

+    | IntLiteral(_)

+    | BoolLiteral(_)

+    | IdLiteral(_)

+    | Star                   -> unifs

+    | Dot(e, _)

+    | SeqLength(e)

+    | ForallExpr(_,e)  

+    | UnaryExpr(_,e)         -> unifs |> __GetUnifications e args

+    | SelectExpr(e1, e2)      

+    | BinaryExpr(_,_,e1,e2)  -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args

+    | IteExpr(e1,e2,e3)

+    | UpdateExpr(e1, e2, e3) -> unifs |> __GetUnifications e1 args |> __GetUnifications e2 args |> __GetUnifications e3 args

+    | SetExpr(elst)

+    | SequenceExpr(elst)     -> elst |> List.fold (fun acc e -> acc |> __GetUnifications e args) unifs 

+                               

+  __GetUnifications expr args Map.empty

+

+//let rec GetUnifications expr args (heap,env,ctx) = 

+//  match expr with

+//  | IntLiteral(_)

+//  | BoolLiteral(_)

+//  | IdLiteral(_)

+//  | Star         

+//  | Dot(_)

+//  | SelectExpr(_)   // TODO: handle select expr

+//  | UpdateExpr(_)   // TODO: handle update expr

+//  | SequenceExpr(_) 

+//  | SeqLength(_)    

+//  | SetExpr(_)

+//  | ForallExpr(_)   // TODO: handle forall expr

+//  | UnaryExpr(_)   -> Map.empty

+//  | IteExpr(c,e0,e1) -> (GetUnifications e0 args (heap,env,ctx)) |> Utils.MapAddAll (GetUnifications e1 args (heap,env,ctx))

+//  | BinaryExpr(strength,op,e0,e1) ->

+//      if op = "=" then

+//        let v0 = Eval (heap,env,ctx) e0

+//        let v1 = Eval (heap,env,ctx) e1

+//        let argsOnly0 = IsArgsOnly args e0

+//        let argsOnly1 = IsArgsOnly args e1

+//        match v0,argsOnly1,argsOnly0,v1 with

+//        | Some(c0),true,_,_ -> 

+//               Logger.DebugLine ("      - adding unification " + (PrintConst c0) + " <--> " + (PrintExpr 0 e1));

+//               Map.ofList [e1, c0]

+//        | _,_,true,Some(c1) -> 

+//               Logger.DebugLine ("      - adding unification " + (PrintConst c1) + " <--> " + (PrintExpr 0 e0));

+//               Map.ofList [e0, c1]

+//        | _ -> Logger.TraceLine ("      - couldn't unify anything from " + (PrintExpr 0 expr));

+//               Map.empty

+//      else 

+//        GetUnifications e0 args (heap,env,ctx) |> Utils.MapAddAll (GetUnifications e1 args (heap,env,ctx))

 

 let rec GetArgValueUnifications args env = 

   match args with

@@ -122,9 +160,9 @@ let rec GetArgValueUnifications args env =
       match Map.tryFind (Unresolved(name)) env with

       | Some(c) ->

           Logger.DebugLine ("      - adding unification " + (PrintConst c) + " <--> " + name);

-          Set.ofList [c, IdLiteral(name)] |> Set.union (GetArgValueUnifications rest env)

+          Map.ofList [IdLiteral(name), c] |> Utils.MapAddAll (GetArgValueUnifications rest env)

       | None -> failwith ("couldn't find value for argument " + name)

-  | [] -> Set.empty

+  | [] -> Map.empty

 

 let rec _GetObjRefExpr o (heap,env,ctx) visited = 

   if Set.contains o visited then 

@@ -133,7 +171,7 @@ let rec _GetObjRefExpr o (heap,env,ctx) visited =
     let newVisited = Set.add o visited

     let refName = PrintObjRefName o (env,ctx)

     match refName with

-    | Exact "this" _ -> Some(IdLiteral(refName))

+    | "this" -> Some(IdLiteral(refName))

     | _ -> 

         let rec __fff lst = 

           match lst with

@@ -152,15 +190,18 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) =
   let __CheckUnif o f e idx =

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

     let fldName = PrintVarName f                             

-    let lhs = Dot(objRefExpr, fldName) |> Utils.IfDo1 (not (idx = -1)) (fun e -> SelectExpr(e, IntLiteral(idx)))

-    let assertionExpr = BinaryEq lhs e 

+    let lhs = Dot(objRefExpr, fldName)

+    let assertionExpr = match f with

+                        | Var(_, Some(SeqType(_))) when not (idx = -1) -> BinaryEq (SelectExpr(lhs, IntLiteral(idx))) e

+                        | Var(_, Some(SetType(_))) when not (idx = -1) -> BinaryIn e lhs

+                        | _                                            -> BinaryEq lhs e 

     // check if the assertion follows and if so update the env

     let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter (comp,mthd) assertionExpr)

     Logger.Debug("        - checking assertion: " + (PrintExpr 0 assertionExpr) + " ... ")

     CheckDafnyProgram code ("unif_" + (GetMethodFullName comp mthd))

 

   match unifs with

-  | (c,e) :: rest -> 

+  | (e,c) :: rest -> 

       let restHeap,env,ctx = UpdateHeapEnv prog comp mthd rest (heap,env,ctx)

       let newHeap = restHeap |> Map.fold (fun acc (o,f) l ->

                                             let value = TryResolve (env,ctx) l

@@ -174,10 +215,7 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) =
                                                 // don't change the value

                                                 acc |> Map.add (o,f) l

                                             else 

-                                              // see if it's a list, then try to match its elements, otherwise leave it as is

-                                              match value with

-                                              | SeqConst(clist) -> 

-                                                  let rec __UnifyOverLst lst cnt =

+                                              let rec __UnifyOverLst lst cnt =

                                                     match lst with

                                                     | lstElem :: rest when lstElem = c ->

                                                         if __CheckUnif o f e cnt then

@@ -189,8 +227,14 @@ let rec UpdateHeapEnv prog comp mthd unifs (heap,env,ctx) =
                                                     | lstElem :: rest ->

                                                         lstElem :: __UnifyOverLst rest (cnt+1)

                                                     | [] -> []

+                                              // see if it's a list, then try to match its elements, otherwise leave it as is

+                                              match value with

+                                              | SeqConst(clist) -> 

                                                   let newLstConst = __UnifyOverLst clist 0

                                                   acc |> Map.add (o,f) (SeqConst(newLstConst))

+                                              | SetConst(cset) ->

+                                                  let newLstConst = __UnifyOverLst (Set.toList cset) 0

+                                                  acc |> Map.add (o,f) (SetConst(newLstConst |> Set.ofList))

                                               | _ -> 

                                                   acc |> Map.add (o,f) l

                                          ) restHeap

@@ -204,9 +248,9 @@ let GeneralizeSolution prog comp mthd (heap,env,ctx) =
       match args with 

       | [] -> (heap,env,ctx)

       | _  -> 

-          let unifs = GetUnifications (BinaryAnd pre post |> Desugar) args (heap,env,ctx)    //TODO: we shouldn't use desugar here, but in UpdateHeapEnv

-                    |> Set.union (GetArgValueUnifications args env)

-          UpdateHeapEnv prog comp mthd (Set.toList unifs) (heap,env,ctx)

+          let unifs = GetUnifications (BinaryAnd pre post) args (heap,env,ctx)    //TODO: we shouldn't use desugar here, but in UpdateHeapEnv

+                      |> Utils.MapAddAll (GetArgValueUnifications args env)

+          UpdateHeapEnv prog comp mthd (Map.toList unifs) (heap,env,ctx)

   | _ -> failwith ("not a method: " + mthd.ToString())

 

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

@@ -242,7 +286,7 @@ let AnalyzeConstructor prog comp m =
     let model = models.[0]

     let heap,env,ctx = ReadFieldValuesFromModel model prog comp m

                        |> GeneralizeSolution prog comp m

-    if _opt_verifySolutions then

+    if Options.CONFIG.verifySolutions then

       Logger.InfoLine "      - verifying synthesized solution ... "

       let verified = VerifySolution prog comp m (heap,env,ctx)

       Logger.Info "      "      

diff --git a/Jennisys/Ast.fs b/Jennisys/Ast.fs
index 167a5eef..86f6861f 100644
--- a/Jennisys/Ast.fs
+++ b/Jennisys/Ast.fs
@@ -29,10 +29,12 @@ type Expr =
   | Dot of Expr * string

   | UnaryExpr of string * Expr

   | BinaryExpr of int * string * Expr * Expr

+  | IteExpr of (* cond *) Expr * (* thenExpr *) Expr * (* elseExpr *) Expr

   | SelectExpr of Expr * Expr

   | UpdateExpr of Expr * Expr * Expr

   | SequenceExpr of Expr list

   | SeqLength of Expr

+  | SetExpr of Expr list

   | ForallExpr of VarDecl list * Expr

 

 type Stmt =

diff --git a/Jennisys/AstUtils.fs b/Jennisys/AstUtils.fs
index 26544f65..32d58ec7 100644
--- a/Jennisys/AstUtils.fs
+++ b/Jennisys/AstUtils.fs
@@ -16,15 +16,16 @@ let rec VisitExpr visitorFunc expr acc =
   | IntLiteral(_)

   | BoolLiteral(_)

   | 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)      -> exs |> List.fold (fun acc2 e -> acc2 |> VisitExpr visitorFunc e) (visitorFunc expr acc)

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

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

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

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

+  | 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)

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

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

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

+  | 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

 

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

 

@@ -53,83 +54,83 @@ let rec EvalSym resolverFunc expr =
       | _ -> resolverFunc expr

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

       match op with

-      | Exact "=" _ ->

+      | "=" ->

           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

-      | Exact "!=" _ -> 

+      | "!=" -> 

           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

-      | Exact "<" _ -> 

+      | "<" -> 

           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

-      | Exact "<=" _ -> 

+      | "<=" -> 

           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

-      | Exact ">" _ -> 

+      | ">" -> 

           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

-      | Exact ">=" _ -> 

+      | ">=" -> 

           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

-      | Exact "in" _ -> 

+      | "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

-      | Exact "!in" _ -> 

+      | "!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

-      | Exact "+" _ -> 

+      | "+" -> 

           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)

-          | _ -> resolverFunc expr

-      | Exact "-" _ -> 

+          | 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

-      | Exact "*" _ -> 

+      | "*" -> 

           match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

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

           | _ -> resolverFunc expr

-      | Exact "div" _ -> 

+      | "div" -> 

           match EvalSym resolverFunc e1, EvalSym resolverFunc e2 with

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

           | _ -> resolverFunc expr

-      | Exact "mod" _ -> 

+      | "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

-      | Exact "!" _ -> 

+      | "!" -> 

           match EvalSym resolverFunc e with

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

           | _ -> resolverFunc expr

-      | Exact "-" _ -> 

+      | "-" -> 

           match EvalSym resolverFunc e with

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

           | _ -> resolverFunc expr

@@ -179,16 +180,18 @@ let BinaryOr (lhs: Expr) (rhs: Expr) =
 //  ===================================================================================

 let BinaryImplies lhs rhs = BinaryExpr(20, "==>", lhs, rhs)

 

-//  =================================================

-/// Returns a binary NEQ of the two given expressions

-//  =================================================

+//  =======================================================

+/// Constructors for binary EQ/NEQ of two given expressions

+//  =======================================================

 let BinaryNeq lhs rhs = BinaryExpr(40, "!=", lhs, rhs)

-

-//  =================================================

-/// Returns a binary EQ of the two given expressions

-//  =================================================

 let BinaryEq lhs rhs = BinaryExpr(40, "=", lhs, rhs)

 

+//  =======================================================

+/// Constructors for binary IN/!IN of two given expressions

+//  =======================================================

+let BinaryIn lhs rhs = BinaryExpr(40, "in", lhs, rhs)

+let BinaryNotIn lhs rhs = BinaryExpr(40, "!in", lhs, rhs)

+

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

 /// Returns TRUE literal

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

@@ -378,16 +381,18 @@ let rec Desugar expr =
   | Star                   

   | Dot(_)                 

   | SelectExpr(_) 

-  | SeqLength(_)           -> expr

-  | UpdateExpr(_)          -> expr //TODO

-  | SequenceExpr(exs)      -> expr //TODO

+  | SeqLength(_)           

+  | UpdateExpr(_)     

+  | SetExpr(_)     

+  | SequenceExpr(_)        -> expr 

   | ForallExpr(v,e)        -> ForallExpr(v, Desugar e)

   | UnaryExpr(op,e)        -> UnaryExpr(op, Desugar e)

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

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

       let be = BinaryExpr(p, op, Desugar e1, Desugar e2)

       try

         match op with

-        | Exact "=" _ ->           

+        | "=" ->           

             match EvalSym DefaultResolver e1, EvalSym DefaultResolver e2 with

             | SeqConst(cl1), SeqConst(cl2) -> 

                 let rec __fff lst1 lst2 cnt = 

diff --git a/Jennisys/CodeGen.fs b/Jennisys/CodeGen.fs
index 80b180be..f59215ed 100644
--- a/Jennisys/CodeGen.fs
+++ b/Jennisys/CodeGen.fs
@@ -111,7 +111,7 @@ let PrintVarAssignments (heap,env,ctx) indent =
   heap |> Map.fold (fun acc (o,f) l ->

                       let objRef = PrintObjRefName o (env,ctx)

                       let fldName = PrintVarName f

-                      let value = Resolve (env,ctx) l |> PrintConst

+                      let value = TryResolve (env,ctx) l |> PrintConst

                       acc + (sprintf "%s%s.%s := %s;" idt objRef fldName value) + newline

                    ) ""

 

@@ -137,14 +137,21 @@ let GenConstructorCode mthd body =
 

 // NOTE: insert here coto to say which methods to analyze

 let GetMethodsToAnalyze prog =

-  (* exactly one *)

-//  let c = FindComponent prog "IntList" |> Utils.ExtractOption

-//  let m = FindMethod c "Singleton" |> Utils.ExtractOption

-//  [c, m]

-  (* all *)

-  FilterMembers prog FilterConstructorMembers 

-  (* only with parameters *)

-//  FilterMembers prog FilterConstructorMembersWithParams 

+  let m = Options.CONFIG.methodToSynth;

+  if m = "*" then

+    (* all *)

+    FilterMembers prog FilterConstructorMembers   

+  elif m = "paramsOnly" then

+    (* only with parameters *)

+    FilterMembers prog FilterConstructorMembersWithParams 

+  else

+    (* exactly one *)

+    let compName = m.Substring(0, m.LastIndexOf("."))

+    let methName = m.Substring(m.LastIndexOf(".") + 1)

+    let c = FindComponent prog compName |> Utils.ExtractOptionMsg ("Cannot find component " + compName)

+    let m = FindMethod c methName |> Utils.ExtractOptionMsg ("Cannot find method " + methName + " in component " + compName)

+    [c, m]            

+  

 

 // solutions: (comp, constructor) |--> (heap, env, ctx) 

 let PrintImplCode prog solutions methodsToPrintFunc =

diff --git a/Jennisys/DafnyModelUtils.fs b/Jennisys/DafnyModelUtils.fs
index b862ffe3..4cc517f2 100644
--- a/Jennisys/DafnyModelUtils.fs
+++ b/Jennisys/DafnyModelUtils.fs
@@ -67,7 +67,7 @@ let GetType (e: Model.Element) prog =
   let fNameOpt = GetElemFullName e

   match fNameOpt with

   | Some(fname) -> match fname with

-                   | Exact "intType" _       -> Some(IntType)

+                   | "intType"               -> Some(IntType)

                    | Prefix "class." clsName -> 

                        match FindComponent prog clsName with

                        | Some(comp) -> Some(GetClassType comp)

@@ -78,10 +78,16 @@ let GetType (e: Model.Element) prog =
 let GetLoc (e: Model.Element) =

   Unresolved(GetRefName e)

 

-let GetSeqFromEnv env key = 

+let FindSeqInEnv env key =

   match Map.find key env with

   | SeqConst(lst) -> lst

   | _ as x-> failwith ("not a SeqConst but: " + x.ToString())

+

+let TryFindSetInEnv env key = 

+  match Map.tryFind key env with

+  | Some(SetConst(s)) -> Some(s)

+  | Some(x) -> failwith ("not a SetConst but: " + x.ToString())

+  | None -> None

                                    

 let AddConstr c1 c2 ctx = 

   if c1 = c2 then

@@ -185,7 +191,7 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
     match idx_tuples with

     | ft :: rest -> 

         let srcLstKey = GetLoc ft.Args.[0]

-        let oldLst = GetSeqFromEnv envMap srcLstKey

+        let oldLst = FindSeqInEnv envMap srcLstKey

         let idx = GetInt ft.Args.[1]

         let lstElem = UnboxIfNeeded model ft.Result

         let newLst = Utils.ListSet idx lstElem oldLst

@@ -200,10 +206,10 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
     | ft :: rest -> 

         let srcLstLoc = GetLoc ft.Args.[0]

         let dstLstLoc = GetLoc ft.Result

-        let oldLst = GetSeqFromEnv envMap srcLstLoc

+        let oldLst = FindSeqInEnv envMap srcLstLoc

         let idx = GetInt ft.Args.[1]

         let lstElemVal = UnboxIfNeeded model ft.Args.[2]

-        let dstLst = GetSeqFromEnv envMap dstLstLoc

+        let dstLst = FindSeqInEnv envMap dstLstLoc

         let newLst = Utils.ListBuild oldLst idx lstElemVal dstLst

         let newCtx = UpdateContext dstLst newLst ctx

         let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))

@@ -217,9 +223,9 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
         let srcLst1Loc = GetLoc ft.Args.[0]

         let srcLst2Loc = GetLoc ft.Args.[1]

         let dstLstLoc = GetLoc ft.Result

-        let oldLst1 = GetSeqFromEnv envMap srcLst1Loc

-        let oldLst2 = GetSeqFromEnv envMap srcLst2Loc

-        let dstLst = GetSeqFromEnv envMap dstLstLoc

+        let oldLst1 = FindSeqInEnv envMap srcLst1Loc

+        let oldLst2 = FindSeqInEnv envMap srcLst2Loc

+        let dstLst = FindSeqInEnv envMap dstLstLoc

         let newLst = List.append oldLst1 oldLst2

         let newCtx = UpdateContext dstLst newLst ctx

         let newEnv = envMap |> Map.add dstLstLoc (SeqConst(newLst))

@@ -238,10 +244,102 @@ let ReadSeq (model: Microsoft.Boogie.Model) (envMap,ctx) =
 

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

 /// Reads stuff about sets from a given model and adds it 

-/// to the given "envMap" map and "ctx" set. (TODO)

+/// to the given "envMap" map and "ctx" set.

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

 let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =

-  (envMap,ctx)

+  // reads stuff from Set#Empty

+  let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) =

+    match empty_tuples with

+    | ft :: rest -> 

+        let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty))

+        __ReadSetEmpty rest (newMap,ctx)

+    | [] -> (envMap,ctx)

+

+  // reads stuff from [2]

+  let __ReadSetMembership (set_tuples: Model.FuncTuple list) (env,ctx) = 

+    match set_tuples with

+    | ft :: rest when GetBool ft.Result -> 

+        let srcSetKey = GetLoc ft.Args.[0]

+        let srcSet = match TryFindSetInEnv env srcSetKey with

+                     | Some(s) -> s

+                     | None -> Set.empty

+        let elem = UnboxIfNeeded model ft.Args.[1]

+        let newEnv = env |> Map.add srcSetKey (SetConst(Set.add elem srcSet))

+        (newEnv,ctx)

+    | _ -> (env,ctx)

+

+  let t_set_empty = Seq.toList (model.MkFunc("Set#Empty", 1).Apps)    

+  let t_set = Seq.toList (model.MkFunc("[2]", 2).Apps)

+  (envMap,ctx) |> __ReadSetEmpty t_set_empty

+               |> __ReadSetMembership t_set

+

+(* More complicated way which now doesn't seem to be necessary *)

+//let ReadSet (model: Microsoft.Boogie.Model) (envMap,ctx) =

+//  // reads stuff from Set#Empty

+//  let rec __ReadSetEmpty (empty_tuples: Model.FuncTuple list) (envMap,ctx) =

+//    match empty_tuples with

+//    | ft :: rest -> 

+//        let newMap = envMap |> Map.add (GetLoc ft.Result) (SetConst(Set.empty))

+//        __ReadSetEmpty rest (newMap,ctx)

+//    | [] -> (envMap,ctx)

+//

+//  // reads stuff from Set#UnionOne and Set#Union

+//  let rec __ReadSetUnions (envMap,ctx) = 

+//    // this one goes through a given list of "UnionOne" tuples, updates 

+//    // the env for those set that it was able to resolve, and returns a 

+//    // list of tuples for which it wasn't able to resolve sets

+//    let rec ___RSU1 (tuples: Model.FuncTuple list) env unprocessed =

+//      match tuples with

+//      | ft :: rest -> 

+//          let srcSetKey = GetLoc ft.Args.[0]

+//          match TryFindSetInEnv env srcSetKey with

+//          | Some(oldSet) ->

+//              let elem = UnboxIfNeeded model ft.Args.[1]

+//              let newSet = Set.add elem oldSet

+//              // update contex?

+//              let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet))

+//              ___RSU1 rest newEnv unprocessed

+//          | None -> ___RSU1 rest env (ft :: unprocessed)          

+//      | [] -> (env,unprocessed)

+//    // this one goes through a given list of "Union" tuples, updates 

+//    // the env for those set that it was able to resolve, and returns a 

+//    // list of tuples for which it wasn't able to resolve sets

+//    let rec ___RSU (tuples: Model.FuncTuple list) env unprocessed =

+//      match tuples with

+//      | ft :: rest -> 

+//          let set1Key = GetLoc ft.Args.[0]

+//          let set2Key = GetLoc ft.Args.[1]

+//          match TryFindSetInEnv env set1Key, TryFindSetInEnv env set2Key with

+//          | Some(oldSet1), Some(oldSet2) ->

+//              let newSet = Set.union oldSet1 oldSet2

+//              // update contex?

+//              let newEnv = env |> Map.add (GetLoc ft.Result) (SetConst(newSet))

+//              ___RSU rest newEnv unprocessed

+//          | _ -> ___RSU rest env (ft :: unprocessed)          

+//      | [] -> (env,unprocessed)

+//    // this one keeps looping as loong as the list of unprocessed tuples

+//    // is decreasing, it ends when if falls down to 0, or fails if 

+//    // the list stops decreasing

+//    let rec ___RSU_until_fixpoint u1tuples utuples env =      

+//      let newEnv1,unprocessed1 = ___RSU1 u1tuples env []

+//      let newEnv2,unprocessed2 = ___RSU utuples newEnv1 []

+//      let oldLen = (List.length u1tuples) + (List.length utuples)

+//      let totalUnprocLen = (List.length unprocessed1) + (List.length unprocessed2)

+//      if totalUnprocLen = 0 then

+//        newEnv2

+//      elif totalUnprocLen < oldLen then

+//        ___RSU_until_fixpoint unprocessed1 unprocessed2 newEnv2

+//      else

+//        failwith "cannot resolve all sets in Set#UnionOne/Set#Union"

+//    // finally, just invoke the fixpoint function for UnionOne and Union tuples

+//    let t_union_one = Seq.toList (model.MkFunc("Set#UnionOne", 2).Apps)

+//    let t_union = Seq.toList (model.MkFunc("Set#Union", 2).Apps)

+//    let newEnv = ___RSU_until_fixpoint t_union_one t_union envMap

+//    (newEnv,ctx)

+//

+//  let f_set_empty = model.MkFunc("Set#Empty", 1)    

+//  (envMap,ctx) |> __ReadSetEmpty (List.ofSeq f_set_empty.Apps)

+//               |> __ReadSetUnions

 

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

 /// Reads staff about the null constant from a given model 

diff --git a/Jennisys/DafnyPrinter.fs b/Jennisys/DafnyPrinter.fs
index bf63f453..9ef9e74a 100644
--- a/Jennisys/DafnyPrinter.fs
+++ b/Jennisys/DafnyPrinter.fs
@@ -31,10 +31,12 @@ let rec PrintExpr ctx expr =
       let openParen = if needParens then "(" else ""
       let closeParen = if needParens then ")" else ""
       sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen
+  | IteExpr(c,e1,e2)  -> sprintf "(if %s then %s else %s)" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)
   | SelectExpr(e,i)   -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i)
   | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)
   | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0))
   | SeqLength(e)      -> sprintf "|%s|" (PrintExpr 0 e)
+  | SetExpr(ee)       -> sprintf "{%s}" (ee |> PrintSep ", " (PrintExpr 0))
   | ForallExpr(vv,e)  ->
       let needParens = true
       let openParen = if needParens then "(" else ""
diff --git a/Jennisys/Jennisys.fs b/Jennisys/Jennisys.fs
index 32827f39..ca1ab1ad 100644
--- a/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys.fs
@@ -10,60 +10,42 @@ open Microsoft.FSharp.Text.Lexing
 
 open Ast
 open Lexer
+open Options
 open Parser
 open Printer
 open TypeChecker
 open Analyzer
 
-let readAndProcess tracing analyzing (filename: string) =
+let readAndProcess (filename: string) =
+  try
+    printfn "// Jennisys, Copyright (c) 2011, Microsoft."
+    // lex
+    let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
+    let lexbuf = LexBuffer<char>.FromTextReader(f)
+    lexbuf.EndPos <- { pos_bol = 0;
+                       pos_fname=if filename = null then "stdin" else filename; 
+                       pos_cnum=0;
+                       pos_lnum=1 }
     try
-        printfn "// Jennisys, Copyright (c) 2011, Microsoft."
-        // lex
-        let f = if filename = null then Console.In else new StreamReader(filename) :> TextReader
-        let lexbuf = LexBuffer<char>.FromTextReader(f)
-        lexbuf.EndPos <- { pos_bol = 0;
-                           pos_fname=if filename = null then "stdin" else filename; 
-                           pos_cnum=0;
-                           pos_lnum=1 }
-        try
-            // parse
-            let sprog = Parser.start Lexer.tokenize lexbuf
-            // print the given Jennisys program
-            if tracing then
-                printfn "---------- Given Jennisys program ----------"
-                printfn "%s" (Print sprog)
-            else ()
-            match TypeCheck sprog with
-              | None -> ()  // errors have already been reported
-              | Some(prog) ->
-                  if analyzing then
-                    // output a Dafny program with the constraints to be solved
-                    Analyze prog filename
-                  else ()
-            // that's it
-            if tracing then printfn "----------" else ()
-        with
-          | ex ->
-              let pos = lexbuf.EndPos
-              printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
-              printfn "%s" (ex.StackTrace.ToString())
-
+      // parse
+      let sprog = Parser.start Lexer.tokenize lexbuf
+      match TypeCheck sprog with
+      | None -> ()  // errors have already been reported
+      | Some(prog) ->
+          Analyze prog filename
     with
-     | ex ->
+      | ex ->
+          let pos = lexbuf.EndPos
+          printfn "%s(%d,%d): %s" pos.FileName pos.Line pos.Column ex.Message
+          printfn "%s" (ex.StackTrace.ToString())
+  with
+    | ex ->
         printfn "Unhandled Exception: %s" ex.Message
         printfn "%s" (ex.StackTrace.ToString())
 
-let rec start n (args: string []) tracing analyzing filename =
-  if n < args.Length then
-    let arg = args.[n]
-    if arg = "/break" then ignore (System.Diagnostics.Debugger.Launch()) else ()
-    let filename = if arg.StartsWith "/" then filename else arg
-    start (n+1) args (tracing || arg = "/trace") (analyzing && arg <> "/noAnalysis") filename
-  else
-    readAndProcess tracing analyzing filename
-
-let args = Environment.GetCommandLineArgs()
 try 
-  start 1 args false true null
-with 
-  | Failure(msg) as e -> printfn "WHYYYYYYYYYYYYYYY: %s" msg; printfn "%s" e.StackTrace
\ No newline at end of file
+  let args = Environment.GetCommandLineArgs()
+  ParseCmdLineArgs (List.ofArray args)
+  readAndProcess CONFIG.inputFilename
+with
+  | InvalidCmdLineOption(msg) as ex -> printfn "%s" msg; printfn "%s" ex.StackTrace
\ No newline at end of file
diff --git a/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys.fsproj
index 7f0e7ff0..1c87ba4d 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\List2.jen</StartArguments>

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

   </PropertyGroup>

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

     <DebugType>pdbonly</DebugType>

@@ -42,8 +42,8 @@
     <FsYaccOutputFolder>$(IntermediateOutputPath)</FsYaccOutputFolder>

   </PropertyGroup>

   <ItemGroup>

-    <Compile Include="Options.fs" />

     <Compile Include="Utils.fs" />

+    <Compile Include="Options.fs" />

     <Compile Include="PipelineUtils.fs" />

     <Compile Include="Ast.fs" />

     <Compile Include="AstUtils.fs" />

@@ -64,8 +64,8 @@
       <OtherFlags>--unicode</OtherFlags>

     </FsLex>

     <Compile Include="Printer.fs" />

-    <Compile Include="Logger.fs" />

     <Compile Include="DafnyPrinter.fs" />

+    <Compile Include="Logger.fs" />

     <Compile Include="TypeChecker.fs" />

     <Compile Include="Resolver.fs" />

     <Compile Include="CodeGen.fs" />

diff --git a/Jennisys/Lexer.fsl b/Jennisys/Lexer.fsl
index 91c3239c..9eaf7421 100644
--- a/Jennisys/Lexer.fsl
+++ b/Jennisys/Lexer.fsl
@@ -69,6 +69,7 @@ rule tokenize = parse
 | ":"      { COLON }

 | "::"     { COLONCOLON }

 | ","      { COMMA }

+| "?"      { QMARK }

 // Numberic constants

 | digit+        { INTEGER (System.Convert.ToInt32(lexeme lexbuf)) }

 // identifiers

diff --git a/Jennisys/Logger.fs b/Jennisys/Logger.fs
index bb784ba2..2801354d 100644
--- a/Jennisys/Logger.fs
+++ b/Jennisys/Logger.fs
@@ -1,6 +1,8 @@
-/// Simple logging facility

+//  #######################################################

+///   Simple logging facility

 ///

-/// author: Aleksandar Milicevic (t-alekm@microsoft.com)

+///   author: Aleksandar Milicevic (t-alekm@microsoft.com)

+//  #######################################################

 

 module Logger

 

diff --git a/Jennisys/Options.fs b/Jennisys/Options.fs
index d98607b2..355ada6e 100644
--- a/Jennisys/Options.fs
+++ b/Jennisys/Options.fs
@@ -6,5 +6,62 @@
 

 module Options

 

-/// attempt to verify synthesized code

-let _opt_verifySolutions = true
\ No newline at end of file
+open Utils

+

+type Config = {

+   inputFilename: string;

+   methodToSynth: string;

+   verifySolutions: bool;

+}

+

+let defaultConfig: Config = {

+  inputFilename   = "";

+  methodToSynth   = "*";

+  verifySolutions = true;

+}

+

+let mutable CONFIG = defaultConfig

+

+exception InvalidCmdLineArg of string

+exception InvalidCmdLineOption of string

+

+let ParseCmdLineArgs args = 

+  let __StripSwitches str =

+    match str with 

+    | Prefix "--" x 

+    | Prefix "-" x

+    | Prefix "/" x -> x

+    | _ -> str

+

+  let __Split (str: string) =

+    let stripped = __StripSwitches str

+    if stripped = str then

+      ("",str) 

+    else

+      let splits = stripped.Split([| ':' |])

+      if splits.Length > 2 then raise (InvalidCmdLineOption("more than 2 colons in " + str))

+      if splits.Length = 2 then

+        let opt = splits.[0]

+        let value = splits.[1]

+        (opt,value)

+      else

+        let x = __StripSwitches splits.[0]

+        (x, "")

+               

+  let rec __Parse args cfg =

+    match args with

+    | fs :: rest -> 

+        let opt,value = __Split fs

+        match opt with

+        | "method"    -> 

+            if value = "" then raise (InvalidCmdLineArg("Must provide method name"))

+            __Parse rest { cfg with methodToSynth = value }

+        | "verifySol" -> 

+            __Parse rest { cfg with verifySolutions = true }

+        | "" -> 

+            __Parse rest { cfg with inputFilename = value }

+        | _ -> 

+            raise (InvalidCmdLineOption("Unknown option: " + opt))

+    | [] -> cfg    

+  CONFIG <- __Parse args defaultConfig

+

diff --git a/Jennisys/Parser.fsy b/Jennisys/Parser.fsy
index 5053bd18..395ee223 100644
--- a/Jennisys/Parser.fsy
+++ b/Jennisys/Parser.fsy
@@ -26,7 +26,7 @@ let rec MyFold ee acc =
 %token IMPLIES

 %token IFF

 %token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR

-%token GETS COLON COLONCOLON COMMA

+%token GETS COLON COLONCOLON COMMA QMARK

 %token CLASS MODEL CODE

 %token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL

 %token INTTYPE BOOLTYPE SEQTYPE SETTYPE

@@ -134,9 +134,12 @@ Expr10:
     | Expr10 IFF Expr20 { BinaryExpr(10,"<==>",$1,$3) }

 

 Expr20:

-    | Expr30                { $1 }

-    | Expr30 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) }

+    | Expr25                { $1 }

+    | Expr25 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) }

 

+Expr25: 

+    | Expr30                { $1 }

+    | Expr30 QMARK Expr25 COLON Expr25 { IteExpr($1,$3,$5) }

 Expr30:

     | Expr40               { $1 }

     | Expr40 AND Expr30and { BinaryAnd $1 $3 }

@@ -183,6 +186,7 @@ Expr100:
   | Expr100 LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) }

   | LPAREN Expr RPAREN                       { $2 }

   | LBRACKET ExprList RBRACKET               { SequenceExpr($2) }

+  | LCURLY ExprList RCURLY                   { SetExpr($2) }

   | VERTBAR Expr VERTBAR                     { SeqLength($2) }

   | FORALL VarDeclList COLONCOLON Expr       { ForallExpr($2, $4) }

 

diff --git a/Jennisys/Printer.fs b/Jennisys/Printer.fs
index f2cbf30f..53bf6b6d 100644
--- a/Jennisys/Printer.fs
+++ b/Jennisys/Printer.fs
@@ -45,10 +45,12 @@ let rec PrintExpr ctx expr =
       let openParen = if needParens then "(" else ""
       let closeParen = if needParens then ")" else ""
       sprintf "%s%s %s %s%s" openParen (PrintExpr strength e0) op (PrintExpr strength e1) closeParen
+  | IteExpr(c,e1,e2)  -> sprintf "%s ? %s : %s" (PrintExpr 25 c) (PrintExpr 25 e1) (PrintExpr 25 e2)
   | SelectExpr(e,i)   -> sprintf "%s[%s]" (PrintExpr 100 e) (PrintExpr 0 i) 
   | UpdateExpr(e,i,v) -> sprintf "%s[%s := %s]" (PrintExpr 100 e) (PrintExpr 0 i) (PrintExpr 0 v)
-  | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep ", " (PrintExpr 0))
+  | SequenceExpr(ee)  -> sprintf "[%s]" (ee |> PrintSep " " (PrintExpr 0))
   | SeqLength(e)      -> sprintf "|%s|" (PrintExpr 0 e)
+  | SetExpr(ee)       -> sprintf "{%s}" (ee |> PrintSep " " (PrintExpr 0))
   | ForallExpr(vv,e)  ->
       let needParens = ctx <> 0
       let openParen = if needParens then "(" else ""
@@ -120,7 +122,7 @@ let rec PrintConst cst =
   match cst with 
   | IntConst(v)        -> sprintf "%d" v
   | BoolConst(b)       -> sprintf "%b" b
-  | SetConst(cset)     -> cset.ToString() //TODO: this won't work
+  | SetConst(cset)     -> sprintf "{%s}" (PrintSep ", " (fun c -> PrintConst c) (Set.toList cset))
   | SeqConst(cseq)     -> 
       let seqCont = cseq |> List.fold (fun acc c ->
                                          let sep = if acc = "" then "" else ", "
diff --git a/Jennisys/Resolver.fs b/Jennisys/Resolver.fs
index 2ac6b96a..59c6904d 100644
--- a/Jennisys/Resolver.fs
+++ b/Jennisys/Resolver.fs
@@ -71,7 +71,10 @@ let Eval (heap,env,ctx) expr =
   let rec __EvalResolver expr = 

     match expr with

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

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

+    | IdLiteral(id) ->

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

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

+        | _ as c -> c

     | Dot(e, str) -> 

         let discr = __EvalResolver e

         let h2 = Map.filter (fun (loc,Var(fldName,_)) v -> loc = discr && fldName = str) heap |> Map.toList

diff --git a/Jennisys/Utils.fs b/Jennisys/Utils.fs
index 7c55e1e8..b7db5706 100644
--- a/Jennisys/Utils.fs
+++ b/Jennisys/Utils.fs
@@ -11,6 +11,28 @@ module Utils
 // -------------------------------------------

 

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

+/// ensures: ret = b ? Some(b) : None

+//  =====================================

+let BoolToOption b =

+  if b then

+    Some(b)

+  else

+    None

+

+//  =====================================

+/// ensures: ret = (opt == Some(_))

+//  =====================================

+let IsSomeOption opt = 

+  match opt with

+  | Some(_) -> true

+  | None -> false

+

+//  =====================================

+/// ensures: ret = (opt == None)

+//  =====================================

+let IsNoneOption opt = IsSomeOption opt |> not

+

+//  =====================================

 /// requres: x = Some(a) or failswith msg

 /// ensures: ret = a

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

@@ -172,15 +194,9 @@ let (|Prefix|_|) (p:string) (s:string) =
     Some(s.Substring(p.Length))

   else

     None

-

-let (|Exact|_|) (p:string) (s:string) =

-  if s = p then

-    Some(s)

-  else

-    None

-

+                 

 // -------------------------------------------

-// ----------------- random ------------------

+// --------------- workflow ------------------

 // -------------------------------------------

 

 let IfDo1 cond func1 a =

@@ -193,4 +209,17 @@ let IfDo2 cond func2 (a1,a2) =
   if cond then

     func2 a1 a2

   else

-    a1,a2 
\ No newline at end of file
+    a1,a2 

+

+type CascadingBuilder<'a>(failVal: 'a) = 

+  member this.Bind(v, f) =

+    match v with

+    | Some(x) -> f x

+    | None -> failVal

+  member this.Return(v) = v

+

+// -------------------------------------------

+// --------------- random --------------------

+// -------------------------------------------

+

+let Iden x = x
\ No newline at end of file
diff --git a/Jennisys/examples/Set.jen b/Jennisys/examples/Set.jen
new file mode 100644
index 00000000..5626babb
--- /dev/null
+++ b/Jennisys/examples/Set.jen
@@ -0,0 +1,53 @@
+class Set {
+  var elems: set[int]
+
+  constructor Empty()
+    ensures elems = {}
+
+  constructor Singleton(t: int)
+    ensures elems = {t}
+
+  constructor Sum(p: int, q: int)
+    ensures elems = {p + q}
+
+  constructor Double(p: int, q: int)
+    requires p != q
+    ensures elems = {p q}
+}
+
+model Set {
+  var root: SetNode
+
+  frame
+    root * root.elems[*]
+
+  invariant
+    root = null ==> elems = {}
+    root != null ==> elems = root.elems
+}
+
+class SetNode {
+  var elems: set[int]
+
+  constructor Init(t: int)
+    ensures elems = {t}
+
+  constructor Double(p: int, q: int)
+    requires p != q
+    ensures elems = {p q}
+}
+
+model SetNode {
+  var data: int
+  var left: SetNode
+  var right: SetNode
+
+  frame 
+    data * left * right
+
+  invariant
+    left = null && right = null ==> elems = {data}
+    elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {})
+    left != null  ==> forall e :: e in left.elems ==> e < data
+    right != null ==> forall e :: e in right.elems ==> e > data
+}