Jennisys:

   - moved modularization and method unification stuff to their own modules
   - improved the modular synthesis so that whole branches can be delegated
     to existing methods.

8 files changed, 485 insertions, 424 deletions

diff --git a/Jennisys/Jennisys/Analyzer.fs b/Jennisys/Jennisys/Analyzer.fs
index fff6b395..ccc1e4ab 100644
--- a/Jennisys/Jennisys/Analyzer.fs
+++ b/Jennisys/Jennisys/Analyzer.fs
@@ -4,6 +4,8 @@ open Ast
 open AstUtils

 open CodeGen

 open DafnyModelUtils

+open MethodUnifier

+open Modularizer

 open PipelineUtils

 open Options

 open Printer

@@ -13,27 +15,6 @@ open Utils
 

 open Microsoft.Boogie

 

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

-/// Merges two solution maps so that if there are multiple entries for a

-/// single (comp,method) pair it concatenates them (corresponds to multiple 

-/// branches).

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

-let MergeSolutions sol1 sol2 = 

-  let rec __Merge sol1map sol2lst res =

-    match sol2lst with

-    | ((c2,m2), lst2) :: rest -> 

-        match sol1map |> Map.tryFindKey (fun (c1,m1) lst1 -> CheckSameMethods (c1,m1) (c2,m2)) with

-        | Some(c1,m1) -> 

-            let lst1 = sol1map |> Map.find(c1,m1)

-            let newRes = res |> Map.add (c1,m1) (lst1@lst2)

-            __Merge sol1map rest newRes

-        | None -> 

-            let newRes = res |> Map.add (c2,m2) lst2

-            __Merge sol1map rest newRes

-    | [] -> res

-  (* --- function body starts here --- *)

-  __Merge sol1 (sol2 |> Map.toList) sol1 

-                   

 let Rename suffix vars =

   vars |> List.map (function Var(nm,tp) -> nm, Var(nm + suffix, tp))

 

@@ -306,269 +287,26 @@ let GetHeapExpr prog mthd heapInst =
                           objInvsUpdated |> List.fold (fun a e -> BinaryAnd a e) acc

                       ) prepostExpr

 

-// ------------------------------- Modularization stuff ---------------------------------

-

-exception CannotUnify

-

-let GetModularBranch prog comp meth hInst = 

-  let rec __AddDirectChildren e acc = 

-    match e with

-    | ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e

-    | SequenceExpr(elist)

-    | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc

-    | _ -> acc

-

-  let __GetDirectChildren = 

-    let thisRhsExprs = hInst.assignments |> List.choose (function ((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None)

-    thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty 

-                 |> Set.toList

-

-  let directChildren = lazy (__GetDirectChildren)

-

-  let __IsAbstractField ty var = 

-    let builder = CascadingBuilder<_>(false)

-    let varName = GetVarName var

-    builder {

-      let! comp = FindComponent prog (GetTypeShortName ty)

-      let! fld = GetAbstractFields comp |> List.fold (fun acc v -> if GetVarName v = varName then Some(varName) else acc) None

-      return true

-    }

-

-  let __FindObj objName = 

-    try 

-      hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst

-    with

-      | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)

-

-  let __GetObjLitType objLitName = 

-    (__FindObj objLitName).objType

-

-  let __GetAbsFldAssignments objLitName = 

-    hInst.assignments |> List.choose (fun ((obj,var),e) ->

-                                        if obj.name = objLitName && __IsAbstractField obj.objType var then

-                                          Some(var,e)

-                                        else

-                                          None)

-  let rec __ExamineAndFix x e = 

-    match e with

-    | ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) -> 

-        let absFlds = __GetAbsFldAssignments id

-        absFlds |> List.fold (fun acc (Var(vname,_),vval) -> BinaryAnd acc (BinaryEq (Dot(x, vname)) vval)) TrueLiteral

-    | SequenceExpr(elist) ->

-        let rec __fff lst acc cnt = 

-          match lst with

-          | fsExpr :: rest -> 

-              let acc = BinaryAnd acc (__ExamineAndFix (SelectExpr(x, IntLiteral(cnt))) fsExpr)

-              __fff rest acc (cnt+1)

-          | [] -> 

-              let lenExpr = BinaryEq (SeqLength(x)) (IntLiteral(cnt)) 

-              BinaryAnd lenExpr acc

-        __fff elist TrueLiteral 0

-    | _ -> BinaryEq x e

-

-  let __GetSpecFor objLitName =

-    let absFieldAssignments = __GetAbsFldAssignments objLitName

-    absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral

-  

-  let __GetArgsUsed expr = 

-    let args = GetMethodArgs meth

-    let argSet = DescendExpr2 (fun e acc ->

-                                 match e with

-                                 | VarLiteral(vname) ->

-                                     match args |> List.tryFind (function Var(name,_) when vname = name -> true | _ -> false) with

-                                     | Some(var) -> acc |> Set.add var

-                                     | None -> acc

-                                 | _ -> acc

-                               ) expr Set.empty

-    argSet |> Set.toList

-

-  let rec __UnifyImplies lhs rhs unifs = 

-    let ___AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)

-

-    if lhs = FalseLiteral || rhs = TrueLiteral then

-      Some(unifs)

-    else 

-      try 

-        match lhs, rhs with

-        | VarLiteral(vname), rhs -> ___AddOrNone unifs vname rhs

-        | IntLiteral(nL), IntLiteral(nR) when nL = nR -> 

-            Some(unifs)

-        | BoolLiteral(bL), BoolLiteral(bR) when bL = bR -> 

-            Some(unifs)

-        | SetExpr(elistL),  SetExpr(elistR) 

-        | SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR ->

-            let unifs2 = List.fold2 (fun acc elL elR -> match __UnifyImplies elL elR acc with

-                                                        | Some(u) -> u

-                                                        | None -> raise CannotUnify) unifs elistL elistR

-            Some(unifs2)

-        | _ when lhs = rhs ->

-            Some(unifs)

-        | _ ->

-

-            let rec ___f2 target candidate unifs = 

-              match target, candidate with

-              | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opT = opC ->

-                  let builder = new CascadingBuilder<_>(None)

-                  builder {

-                    let! unifsLhs = __UnifyImplies lhsC lhsT unifs

-                    let! unifsRhs = __UnifyImplies rhsC rhsT unifsLhs

-                    return Some(unifsRhs)

-                  }

-              | _ -> None                     

-

-            let rec ___f1 rhsLst lhsLst unifs = 

-              match rhsLst, lhsLst with

-              | targetExpr :: rhsRest, candExpr :: lhsRest -> 

-                  // trying to find a unification for "targetExpr"

-                  let uOpt = match ___f2 targetExpr candExpr unifs with

-                             // found -> just return

-                             | Some(unifs2) -> Some(unifs2)

-                             // not found -> keep looking in the rest of the candidate expressions

-                             | None -> ___f1 [targetExpr] lhsRest unifs

-                  match uOpt with

-                  // found -> try find for the rest of the target expressions

-                  | Some(unifs2) -> ___f1 rhsRest lhsLst unifs2

-                  // not found -> fail

-                  | None -> None

-              | targetExpr :: _, [] ->

-                  // no more candidates for unification for this targetExpr -> fail

-                  None

-              | [], _ ->

-                  // we've found unifications for all target expressions -> return the current unifications map

-                  Some(unifs)

-                  

-//        let candExprs = lhsLst |> List.choose (function BinaryExpr(_,cop,cl,cr) as e when cop = top -> Some(e) | _ -> None)

-//                      candExprs |> List.fold (fun acc candExpr -> 

-//                                                match candExpr with

-//                                                | BinaryExpr(_,_,cl,cr) -> 

-

-//            let rec ___f1 lhsLst rhsLst unifs = 

-//              match rhsLst with

-//              | targetExpr :: rhsRest -> 

-//                  match targetExpr with

-//                  | BinaryExpr(_,"=",l,SequenceExpr(_)) -> 

-//                      // this one has already been desugared so it's ok to skip it

-//                      ___f1 lhsLst rhsRest unifs

-//                  | BinaryExpr(_,top,tl,tr) ->

-//                      let candExprs = lhsLst |> List.choose (function BinaryExpr(_,cop,cl,cr) when cop = top -> Some(cr) | _ -> None)

-//                      match candExprs with

-//                      | [] -> None

-//                      | cand :: _ -> 

-//                          let unifs2Opt = __UnifyImplies cand tr unifs

-//                          match unifs2Opt with

-//                          | Some(unifs2) -> ___f1 lhsLst rhsRest unifs2

-//                          | None -> None

-//                  | _ -> None          

-//              | [] -> Some(unifs)  

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

-            let lhsConjs = lhs |> DesugarRemove |> SplitIntoConjunts

-            let rhsConjs = rhs |> DesugarRemove |> SplitIntoConjunts

-            ___f1 rhsConjs lhsConjs unifs

-      with

-      | KeyAlreadyExists

-      | CannotUnify -> None

-

-  let __TryUnify targetMthd candMethod = 

-    let targetPre,targetPost = GetMethodPrePost targetMthd

-    let candPre,candPost = GetMethodPrePost candMethod

-    let builder = new CascadingBuilder<_>(None)

-    builder {

-      let! unifs1 = __UnifyImplies targetPre candPre Map.empty

-      let! unifs2 = __UnifyImplies candPost targetPost unifs1

-      return Some(unifs2)

-    }

-

-  let rec __TryFindAMatch targetMthd candidateMethods = 

-    match candidateMethods with

-    | candMthd :: rest ->

-        match __TryUnify targetMthd candMthd with

-        | Some(unifs) -> Some(candMthd,unifs)

-        | None -> __TryFindAMatch targetMthd rest

-    | [] -> None

-  

-  let __TryFindExisting comp targetMthd = 

-    Logger.TraceLine "Trying"

-    match __TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with

-    | Some(m,unifs) -> m,unifs

-    | None -> 

-        let argsExprs = GetMethodArgs targetMthd |> List.fold (fun acc (Var(name,_)) -> acc |> Map.add name (VarLiteral(name))) Map.empty

-        targetMthd,argsExprs

-

-  let rec __GetDelegateMethods objs acc = 

-    match objs with

-    | ObjLiteral(name) as obj :: rest ->

-        let mName = sprintf "_synth_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name

-        let pre,_ = GetMethodPrePost meth //TrueLiteral

-        let post = __GetSpecFor name

-        let ins = __GetArgsUsed (BinaryAnd pre post)

-        let sgn = Sig(ins, [])

-        let m = Method(mName, sgn, pre, post, true)

-        let c = FindComponent prog (name |> __GetObjLitType |> GetTypeShortName) |> Utils.ExtractOption

-        let m',unifs = __TryFindExisting c m

-        let args = GetMethodArgs m' |> List.map (fun (Var(name,_)) -> Map.find name unifs)

-        __GetDelegateMethods rest (acc |> Map.add obj (c,m',args))

-    | _ :: rest -> failwith "internal error: expected to see only ObjLiterals"

-    | [] -> acc

-

-  (* --- function body starts here --- *)

-  let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty

-  let initChildrenExprList = delegateMethods |> Map.toList

-                                             |> List.map (fun (receiver, (cmp,mthd,args)) -> 

-                                                            let key = __FindObj (PrintExpr 0 receiver), Var("", None)

-                                                            let e = MethodCall(receiver, GetMethodName mthd, args)

-                                                            (key, e)

-                                                         )

-  let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)

-  let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->

-                                                                       let obj = __FindObj (PrintExpr 0 receiver)

-                                                                       match acc with

-                                                                       | accProg, accComp, accmList ->

-                                                                           let oldComp = FindComponent accProg (GetTypeShortName obj.objType) |> Utils.ExtractOption

-                                                                           let prog', mcomp' = AddReplaceMethod accProg oldComp newMthd None

-                                                                           let mList' = (mcomp', newMthd) :: accmList

-                                                                           let comp' = if accComp = oldComp then mcomp' else accComp

-                                                                           prog', comp', mList'

-                                                                    ) (prog, comp, [])

-  newProg, newComp, newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }

-

-let rec MakeModular indent prog comp m cond heapInst = 

-  let idt = Indent indent

-  if Options.CONFIG.genMod then   

-    Logger.InfoLine (idt + "    - delegating to method calls     ...")

-    let newProg, newComp, newMthdLst, newHeapInst = GetModularBranch prog comp m heapInst

-    let msol = Utils.MapSingleton (newComp,m) [cond, newHeapInst]

-    newMthdLst |> List.fold (fun acc (c,m) -> 

-                               acc |> MergeSolutions (Utils.MapSingleton (c,m) []) 

-                             ) msol     

+let FindExisting indent comp m cond =

+  if not Options.CONFIG.genMod then

+    None

   else 

-    Utils.MapSingleton (comp,m) [cond, heapInst]

-

-//let GetModularSol prog sol = 

-//  let comp = fst (fst sol)

-//  let meth = snd (fst sol)

-//  let rec __xxx prog lst = 

-//    match lst with

-//    | (cond, hInst) :: rest -> 

-//        let newProg, newComp, newMthdLst, newhInst = GetModularBranch prog comp meth hInst

-//        let newProg, newRest = __xxx newProg rest

-//        newProg, ((cond, newhInst) :: newRest)

-//    | [] -> prog, []

-//  let newProg, newSolutions = __xxx prog (snd sol)

-//  let newComp = FindComponent newProg (GetComponentName comp) |> Utils.ExtractOption

-//  newProg, ((newComp, meth), newSolutions)

-//

-//let Modularize prog solutions = 

-//  let rec __Modularize prog sols acc = 

-//    match sols with

-//    | sol :: rest -> 

-//        let (newProg, newSol) = GetModularSol prog sol

-//        let newAcc = acc |> Map.add (fst newSol) (snd newSol)

-//        __Modularize newProg rest newAcc 

-//    | [] -> (prog, acc)

-//  (* --- function body starts here --- *) 

-//  __Modularize prog (Map.toList solutions) Map.empty 

-

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

+    let idt = Indent indent

+    match TryFindAMatch m (GetMembers comp |> FilterMethodMembers) with

+    | Some(m',unifs) -> 

+        Logger.InfoLine (idt + "    - substitution method found:")

+        Logger.InfoLine (PrintMethodSignFull (indent+6) comp m')

+        let args = ApplyMethodUnifs m' unifs

+        let delegateCall = MethodCall(ThisLiteral, GetMethodName m', args)

+        let obj = { name = "this"; objType = GetClassType comp }

+        let var = Var("", None)

+        let body = [(obj,var), delegateCall]

+        let hInst = { assignments = body; 

+                      methodArgs  = Map.empty; 

+                      globals     = Map.empty }

+        Some(Map.empty |> Map.add (comp,m) [cond, hInst]

+                       |> Map.add (comp,m') [])

+    | None -> None

 

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

 /// Attempts to synthesize the initialization code for the given constructor "m"

@@ -576,18 +314,15 @@ let rec MakeModular indent prog comp m cond heapInst =
 /// Returns a (heap,env,ctx) tuple

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

 let rec AnalyzeConstructor indent prog comp m =

-  // TODO: first check maybe there's already a method with this spec

-  

-

   let idt = Indent indent

-  let methodName = GetMethodName m

-  let pre,post = GetMethodPrePost m

-  // generate Dafny code for analysis first

-  let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral) false

   Logger.InfoLine (idt + "[*] Analyzing constructor")

   Logger.InfoLine (idt + "------------------------------------------")

   Logger.InfoLine (PrintMethodSignFull (indent + 4) comp m)

   Logger.InfoLine (idt + "------------------------------------------")

+  let methodName = GetMethodName m

+  let pre,post = GetMethodPrePost m

+  // generate Dafny code for analysis first

+  let code = PrintDafnyCodeSkeleton prog (MethodAnalysisPrinter [comp,m] FalseLiteral) false

   Logger.Info     (idt + "    - searching for an instance      ...")

   let models = RunDafnyProgram code (dafnyScratchSuffix + "_" + (GetMethodFullName comp m))  

   if models.Count = 0 then

@@ -625,49 +360,54 @@ let rec AnalyzeConstructor indent prog comp m =
     else

       sol

 and TryInferConditionals indent prog comp m unifs heapInst = 

+  // use the orginal method, not the one with an extra precondition

+  let __FixSolution sol =

+    sol |> Map.fold (fun acc (cc,mm) v -> 

+                       if GetMethodName mm = GetMethodName m then

+                         acc |> Map.add (cc,m) v

+                       else 

+                         acc |> Map.add (cc,mm) v) Map.empty

   let idt = Indent indent

   let wrongSol = Utils.MapSingleton (comp,m) [TrueLiteral, heapInst]

   let heapInst2 = ApplyUnifications indent prog comp m unifs heapInst false

   let expr = GetHeapExpr prog m heapInst2

   // now evaluate and see what's left

   let newCond = Eval heapInst2 (function VarLiteral(_) -> false | _ -> true) expr

-  try

-    if newCond = TrueLiteral then

-      Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

-      wrongSol

-    else

-      let candCond = 

-        if newCond = FalseLiteral then

-          // it must be because there is some aliasing going on between method arguments, 

-          // so we should try that as a candidate pre-condition

-          let tmp = DiscoverAliasing (GetMethodArgs m |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2

-          if tmp = TrueLiteral then failwith ("post-condition evaluated to false and no aliasing was discovered")

-          tmp

-        else 

-          newCond

-      Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 candCond))

-      let p2,c2,m2 = AddPrecondition prog comp m candCond

-      let sol = MakeModular indent p2 c2 m2 candCond heapInst2

-      Logger.Info (idt + "    - verifying partial solution ... ")

-      let verified = 

-        if Options.CONFIG.verifyPartialSolutions then

-          VerifySolution p2 sol Options.CONFIG.genRepr

-        else 

-          true

-      if verified then

-        if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

-        let p3,c3,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

-        let fixedSol = sol |> Map.fold (fun acc (cc,mm) v -> 

-                                          if GetMethodName mm = GetMethodName m then

-                                            acc |> Map.add (cc,m) v

-                                          else 

-                                            acc |> Map.add (cc,mm) v) Map.empty

-        MergeSolutions fixedSol (AnalyzeConstructor (indent + 2) p3 c3 m3)

+  if newCond = TrueLiteral then

+    Logger.InfoLine (sprintf "%s    - no more interesting pre-conditions" idt)

+    wrongSol

+  else

+    let candCond = 

+      if newCond = FalseLiteral then

+        // it must be because there is some aliasing going on between method arguments, 

+        // so we should try that as a candidate pre-condition

+        let tmp = DiscoverAliasing (GetMethodArgs m |> List.map (function Var(name,_) -> VarLiteral(name))) heapInst2

+        if tmp = TrueLiteral then failwith ("post-condition evaluated to false and no aliasing was discovered")

+        tmp

       else 

-        Logger.InfoLine "NOT VERIFIED"

-        wrongSol                     

-  with

-    ex -> raise ex

+        newCond

+    Logger.InfoLine (sprintf "%s    - candidate pre-condition: %s" idt (PrintExpr 0 candCond))

+    let _,_,m2 = AddPrecondition prog comp m candCond

+    let sol = MakeModular indent prog comp m2 candCond heapInst2

+    Logger.Info (idt + "    - verifying partial solution ... ")

+    let verified = 

+      if Options.CONFIG.verifyPartialSolutions then

+        VerifySolution prog sol Options.CONFIG.genRepr

+      else 

+        true

+    if verified then

+      if Options.CONFIG.verifyPartialSolutions then Logger.InfoLine "VERIFIED" else Logger.InfoLine "SKIPPED"

+      let solThis = match FindExisting indent comp m2 candCond with

+                    | Some(sol2) -> sol2

+                    | None -> sol   

+      let _,_,m3 = AddPrecondition prog comp m (UnaryNot(candCond))

+      let solRest = match FindExisting indent comp m3 (UnaryNot(candCond)) with

+                    | Some(sol3) -> sol3

+                    | None -> AnalyzeConstructor (indent + 2) prog comp m3

+      MergeSolutions (__FixSolution solThis) (__FixSolution solRest)

+    else 

+      Logger.InfoLine "NOT VERIFIED"

+      wrongSol  

       

 let GetMethodsToAnalyze prog =

   let mOpt = Options.CONFIG.methodToSynth;

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 641a7143..dc6534e1 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -61,6 +61,31 @@ let Substitute e1 e2 expr =
              else

                None) expr

 

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

+/// Distributes the negation operator over 

+/// arithmetic relations

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

+let rec DistributeNegation expr = 

+  let __Neg op = 

+    match op with

+    | "="  -> Some("!=")

+    | "!=" -> Some("=")

+    | "<"  -> Some(">")

+    | ">"  -> Some("<")

+    | ">=" -> Some("<=")

+    | "<=" -> Some(">=")

+    | _ -> None

+  Rewrite (fun e -> 

+    match e with

+    | UnaryExpr("!", sub) ->

+        match sub with 

+        | BinaryExpr(p,op,lhs,rhs) -> 

+            match __Neg op with

+            | Some(op') -> Some(BinaryExpr(p, op', DistributeNegation lhs, DistributeNegation rhs))

+            | None -> None

+        | _ -> None

+    | _ -> None) expr

+

 let rec DescendExpr visitorFunc composeFunc leafVal expr = 

   let __Compose elist =

     match elist with

@@ -814,7 +839,7 @@ let MyDesugar expr removeOriginal =
   __Desugar expr

 

 let Desugar expr = MyDesugar expr false

-let DesugarRemove expr = MyDesugar expr true

+let DesugarAndRemove expr = MyDesugar expr true

 

 let rec DesugarLst exprLst = 

   match exprLst with

diff --git a/Jennisys/Jennisys/CodeGen.fs b/Jennisys/Jennisys/CodeGen.fs
index 754f75aa..a8a4cda6 100644
--- a/Jennisys/Jennisys/CodeGen.fs
+++ b/Jennisys/Jennisys/CodeGen.fs
@@ -198,8 +198,11 @@ let PrintReprAssignments prog heapInst indent =
                                           fullReprExpr :: acc

                                        ) []

   

-  idt + "// repr stuff" + newline + 

-  (PrintStmtList reprGetsList indent)

+  if not (reprGetsList = []) then

+    idt + "// repr stuff" + newline + 

+    (PrintStmtList reprGetsList indent)

+  else

+    ""

                                                           

 let rec PrintHeapCreationCode prog sol indent genRepr =    

   let idt = Indent indent

diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index 69a597cc..668263b9 100644
--- a/Jennisys/Jennisys/Jennisys.fsproj
+++ b/Jennisys/Jennisys/Jennisys.fsproj
@@ -23,7 +23,7 @@
     <WarningLevel>3</WarningLevel>

     <PlatformTarget>x86</PlatformTarget>

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

-    <StartArguments>examples/Set.jen /method:Set.Singleton /genRepr  /genMod</StartArguments>

+    <StartArguments>examples/Set.jen /method:SetNode.Triple /genRepr  /genMod</StartArguments>

     <StartWorkingDirectory>C:\boogie\Jennisys\Jennisys\</StartWorkingDirectory>

   </PropertyGroup>

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

@@ -69,6 +69,8 @@
     <Compile Include="DafnyPrinter.fs" />

     <Compile Include="TypeChecker.fs" />

     <Compile Include="Resolver.fs" />

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

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

     <Compile Include="CodeGen.fs" />

     <Compile Include="Analyzer.fs" />

     <Compile Include="Jennisys.fs" />

diff --git a/Jennisys/Jennisys/MethodUnifier.fs b/Jennisys/Jennisys/MethodUnifier.fs
new file mode 100644
index 00000000..54a76139
--- /dev/null
+++ b/Jennisys/Jennisys/MethodUnifier.fs
@@ -0,0 +1,135 @@
+module MethodUnifier

+

+open Ast

+open AstUtils

+open Printer 

+open Resolver

+open Utils

+

+exception CannotUnify

+

+type UnifDirection = LTR | RTL

+

+let rec UnifyImplies lhs rhs dir unifs = 

+  let ___AddOrNone unifs name e = Some(unifs |> Utils.MapAddNew name e)

+

+  if lhs = FalseLiteral || rhs = TrueLiteral then

+    Some(unifs)

+  else 

+    try 

+      let l,r = match dir with

+                | LTR -> lhs,rhs

+                | RTL -> rhs,lhs

+      match l, r with

+      | VarLiteral(vname), rhs -> ___AddOrNone unifs vname rhs

+      | IntLiteral(nL), IntLiteral(nR) when nL = nR -> 

+          Some(unifs)

+      | BoolLiteral(bL), BoolLiteral(bR) when bL = bR -> 

+          Some(unifs)

+      | SetExpr(elistL),  SetExpr(elistR) 

+      | SequenceExpr(elistL), SequenceExpr(elistR) when List.length elistL = List.length elistR ->

+          let unifs2 = List.fold2 (fun acc elL elR -> match UnifyImplies elL elR dir acc with

+                                                      | Some(u) -> u

+                                                      | None -> raise CannotUnify) unifs elistL elistR

+          Some(unifs2)

+      | _ when l = r ->

+          Some(unifs)

+      | _ ->

+          let __InvOps op1 op2 = match op1, op2 with "<" , ">" | ">" , "<" | "<=", ">=" | ">=", "<=" -> true | _ -> false

+          let __ImpliesOp op1 op2 = 

+            match op1, op2 with 

+            | "<" , "!=" | ">" , "!=" -> true 

+            | "=" , ">=" | "=" , "<=" -> true 

+            | _ -> false

+          let __CommOp op = match op with "=" | "!=" -> true | _ -> false

+

+          let __TryUnifyPair x1 a1 x2 a2 unifs = 

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

+            builder {

+              let! unifsLhs = UnifyImplies x1 a1 dir unifs

+              let! unifsRhs = UnifyImplies x2 a2 dir unifsLhs

+              return Some(unifsRhs)

+            }

+

+          // target implies candidate!

+          let rec ___f2 consequence premise unifs = 

+            match consequence, premise with

+            // same operators + commutative -> try both

+            | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opT = opC && __CommOp opT ->

+                match __TryUnifyPair lhsC lhsT rhsC rhsT unifs with

+                | Some(x) -> Some(x)

+                | None -> __TryUnifyPair lhsC rhsT rhsC lhsT unifs

+            // operators are the same

+            | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when opC = opT ->

+                __TryUnifyPair lhsC lhsT rhsC rhsT unifs

+            // operators are exactly the invers of one another

+            | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when __InvOps opC opT ->

+                __TryUnifyPair lhsC rhsT rhsC lhsT unifs

+            // 

+            | BinaryExpr(_, opT, lhsT, rhsT), BinaryExpr(_, opC, lhsC, rhsC) when __ImpliesOp opC opT ->

+                __TryUnifyPair lhsC lhsT rhsC rhsT unifs

+            | UnaryExpr(opC, subC), UnaryExpr(opP, subP) when opC = opP ->

+                UnifyImplies subP subC dir unifs 

+            | _ -> None                     

+

+          let rec ___f1 targetLst candidateLst unifs = 

+            match targetLst, candidateLst with

+            | targetExpr :: targetRest, candExpr :: candRest -> 

+                // trying to find a unification for "targetExpr"

+                let uOpt = match ___f2 targetExpr candExpr unifs with

+                            // found -> just return

+                            | Some(unifs2) -> Some(unifs2)

+                            // not found -> keep looking in the rest of the candidate expressions

+                            | None -> ___f1 [targetExpr] candRest unifs

+                match uOpt with

+                // found -> try find for the rest of the target expressions

+                | Some(unifs2) -> ___f1 targetRest candidateLst unifs2

+                // not found -> fail

+                | None -> None

+            | targetExpr :: _, [] ->

+                // no more candidates for unification for this targetExpr -> fail

+                None

+            | [], _ ->

+                // we've found unifications for all target expressions -> return the current unifications map

+                Some(unifs)

+                  

+          let lhsConjs = lhs |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts

+          let rhsConjs = rhs |> DesugarAndRemove |> DistributeNegation |> SplitIntoConjunts

+          ___f1 rhsConjs lhsConjs unifs

+    with

+    | KeyAlreadyExists

+    | CannotUnify -> None

+

+let TryUnify targetMthd candMethod = 

+  let targetPre,targetPost = GetMethodPrePost targetMthd

+  let candPre,candPost = GetMethodPrePost candMethod

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

+  builder {

+    let! unifs1 = UnifyImplies targetPre candPre RTL Map.empty

+    let! unifs2 = UnifyImplies candPost targetPost LTR unifs1

+    return Some(unifs2)

+  }

+

+let rec TryFindAMatch targetMthd candidateMethods = 

+  let targetMthdName = GetMethodName targetMthd

+  match candidateMethods with

+  | candMthd :: rest ->

+      if GetMethodName candMthd = targetMthdName then

+        // skip if it is the same method

+        TryFindAMatch targetMthd rest

+      else

+        match TryUnify targetMthd candMthd with

+        | Some(unifs) -> Some(candMthd,unifs)

+        | None -> TryFindAMatch targetMthd rest

+  | [] -> None

+  

+let TryFindExisting comp targetMthd = 

+  match TryFindAMatch targetMthd (GetMembers comp |> FilterMethodMembers) with

+  | Some(m,unifs) -> m,unifs

+  | None -> targetMthd, Map.empty

+

+let ApplyMethodUnifs m unifs =

+  GetMethodArgs m |> List.map (fun (Var(name,_)) -> 

+                                 match Map.tryFind name unifs with

+                                 | Some(e) -> e

+                                 | None -> VarLiteral(name))
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Modularizer.fs b/Jennisys/Jennisys/Modularizer.fs
new file mode 100644
index 00000000..72181c2f
--- /dev/null
+++ b/Jennisys/Jennisys/Modularizer.fs
@@ -0,0 +1,179 @@
+module Modularizer

+

+open Ast

+open AstUtils

+open MethodUnifier

+open Printer 

+open Resolver

+open Utils

+

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

+/// Merges two solution maps so that if there are multiple entries for a

+/// single (comp,method) pair it concatenates them (corresponds to multiple 

+/// branches).

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

+let MergeSolutions sol1 sol2 = 

+  let rec __Merge sol1map sol2lst res =

+    match sol2lst with

+    | ((c2,m2), lst2) :: rest -> 

+        match sol1map |> Map.tryFindKey (fun (c1,m1) lst1 -> CheckSameMethods (c1,m1) (c2,m2)) with

+        | Some(c1,m1) -> 

+            let lst1 = sol1map |> Map.find(c1,m1)

+            let newRes = res |> Map.add (c1,m1) (lst1@lst2)

+            __Merge sol1map rest newRes

+        | None -> 

+            let newRes = res |> Map.add (c2,m2) lst2

+            __Merge sol1map rest newRes

+    | [] -> res

+  (* --- function body starts here --- *)

+  __Merge sol1 (sol2 |> Map.toList) sol1 

+                   

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

+/// Tries to make a given solution for a given method into more modular, 

+/// by delegating some statements (initialization of inner objects) to 

+/// method calls. 

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

+let GetModularBranch prog comp meth hInst = 

+  let rec __AddDirectChildren e acc = 

+    match e with

+    | ObjLiteral(_) when not (e = ThisLiteral || e = NullLiteral) -> acc |> Set.add e

+    | SequenceExpr(elist)

+    | SetExpr(elist) -> elist |> List.fold (fun acc2 e2 -> __AddDirectChildren e2 acc2) acc

+    | _ -> acc

+

+  let __GetDirectChildren = 

+    let thisRhsExprs = hInst.assignments |> List.choose (function ((obj,_),e) when obj.name = "this" -> Some(e) | _ -> None)

+    thisRhsExprs |> List.fold (fun acc e -> __AddDirectChildren e acc) Set.empty 

+                 |> Set.toList

+

+  let directChildren = lazy (__GetDirectChildren)

+

+  let __IsAbstractField ty var = 

+    let builder = CascadingBuilder<_>(false)

+    let varName = GetVarName var

+    builder {

+      let! comp = FindComponent prog (GetTypeShortName ty)

+      let! fld = GetAbstractFields comp |> List.fold (fun acc v -> if GetVarName v = varName then Some(varName) else acc) None

+      return true

+    }

+

+  let __FindObj objName = 

+    try 

+      hInst.assignments |> List.find (fun ((obj,_),_) -> obj.name = objName) |> fst |> fst

+    with

+      | ex -> failwithf "obj %s not found for method %s" objName (GetMethodFullName comp meth)

+

+  let __GetObjLitType objLitName = 

+    (__FindObj objLitName).objType

+

+  let __GetAbsFldAssignments objLitName = 

+    hInst.assignments |> List.choose (fun ((obj,var),e) ->

+                                        if obj.name = objLitName && __IsAbstractField obj.objType var then

+                                          Some(var,e)

+                                        else

+                                          None)

+  let rec __ExamineAndFix x e = 

+    match e with

+    | ObjLiteral(id) when not (Utils.ListContains e (directChildren.Force())) -> 

+        let absFlds = __GetAbsFldAssignments id

+        absFlds |> List.fold (fun acc (Var(vname,_),vval) -> BinaryAnd acc (BinaryEq (Dot(x, vname)) vval)) TrueLiteral

+    | SequenceExpr(elist) ->

+        let rec __fff lst acc cnt = 

+          match lst with

+          | fsExpr :: rest -> 

+              let acc = BinaryAnd acc (__ExamineAndFix (SelectExpr(x, IntLiteral(cnt))) fsExpr)

+              __fff rest acc (cnt+1)

+          | [] -> 

+              let lenExpr = BinaryEq (SeqLength(x)) (IntLiteral(cnt)) 

+              BinaryAnd lenExpr acc

+        __fff elist TrueLiteral 0

+    | _ -> BinaryEq x e

+

+  let __GetSpecFor objLitName =

+    let absFieldAssignments = __GetAbsFldAssignments objLitName

+    absFieldAssignments |> List.fold (fun acc (Var(name,_),e) -> BinaryAnd acc (__ExamineAndFix (IdLiteral(name)) e)) TrueLiteral

+  

+  let __GetArgsUsed expr = 

+    let args = GetMethodArgs meth

+    let argSet = DescendExpr2 (fun e acc ->

+                                 match e with

+                                 | VarLiteral(vname) ->

+                                     match args |> List.tryFind (function Var(name,_) when vname = name -> true | _ -> false) with

+                                     | Some(var) -> acc |> Set.add var

+                                     | None -> acc

+                                 | _ -> acc

+                               ) expr Set.empty

+    argSet |> Set.toList

+

+  let rec __GetDelegateMethods objs acc = 

+    match objs with

+    | ObjLiteral(name) as obj :: rest ->

+        let mName = sprintf "_synth_%s_%s" (GetMethodFullName comp meth |> String.map (fun c -> if c = '.' then '_' else c)) name

+        let pre,_ = GetMethodPrePost meth //TrueLiteral

+        let post = __GetSpecFor name

+        let ins = __GetArgsUsed (BinaryAnd pre post)

+        let sgn = Sig(ins, [])

+        let m = Method(mName, sgn, pre, post, true)

+        let c = FindComponent prog (name |> __GetObjLitType |> GetTypeShortName) |> Utils.ExtractOption

+        let m',unifs = TryFindExisting c m

+        let args = ApplyMethodUnifs m' unifs

+        __GetDelegateMethods rest (acc |> Map.add obj (c,m',args))

+    | _ :: rest -> failwith "internal error: expected to see only ObjLiterals"

+    | [] -> acc

+

+  (* --- function body starts here --- *)

+  let delegateMethods = __GetDelegateMethods (directChildren.Force()) Map.empty

+  let initChildrenExprList = delegateMethods |> Map.toList

+                                             |> List.map (fun (receiver, (cmp,mthd,args)) -> 

+                                                            let key = __FindObj (PrintExpr 0 receiver), Var("", None)

+                                                            let e = MethodCall(receiver, GetMethodName mthd, args)

+                                                            (key, e))

+  let newAssgns = hInst.assignments |> List.filter (fun ((obj,_),_) -> if obj.name = "this" then true else false)

+  let newProg, newComp, newMethodsLst = delegateMethods |> Map.fold (fun acc receiver (c,newMthd,_) ->

+                                                                       let obj = __FindObj (PrintExpr 0 receiver)

+                                                                       match acc with

+                                                                       | accProg, accComp, accmList ->

+                                                                           let oldComp = FindComponent accProg (GetTypeShortName obj.objType) |> Utils.ExtractOption

+                                                                           let prog', mcomp' = AddReplaceMethod accProg oldComp newMthd None

+                                                                           let mList' = (mcomp', newMthd) :: accmList

+                                                                           let comp' = if accComp = oldComp then mcomp' else accComp

+                                                                           prog', comp', mList'

+                                                                    ) (prog, comp, [])

+  newProg, newComp, newMethodsLst, { hInst with assignments = initChildrenExprList @ newAssgns }

+

+let rec MakeModular indent prog comp m cond heapInst = 

+  let idt = Indent indent

+  if Options.CONFIG.genMod then   

+    Logger.InfoLine (idt + "    - delegating to method calls     ...")

+    let newProg, newComp, newMthdLst, newHeapInst = GetModularBranch prog comp m heapInst

+    let msol = Utils.MapSingleton (newComp,m) [cond, newHeapInst]

+    newMthdLst |> List.fold (fun acc (c,m) -> 

+                               acc |> MergeSolutions (Utils.MapSingleton (c,m) []) 

+                             ) msol     

+  else 

+    Utils.MapSingleton (comp,m) [cond, heapInst]

+

+//let GetModularSol prog sol = 

+//  let comp = fst (fst sol)

+//  let meth = snd (fst sol)

+//  let rec __xxx prog lst = 

+//    match lst with

+//    | (cond, hInst) :: rest -> 

+//        let newProg, newComp, newMthdLst, newhInst = GetModularBranch prog comp meth hInst

+//        let newProg, newRest = __xxx newProg rest

+//        newProg, ((cond, newhInst) :: newRest)

+//    | [] -> prog, []

+//  let newProg, newSolutions = __xxx prog (snd sol)

+//  let newComp = FindComponent newProg (GetComponentName comp) |> Utils.ExtractOption

+//  newProg, ((newComp, meth), newSolutions)

+//

+//let Modularize prog solutions = 

+//  let rec __Modularize prog sols acc = 

+//    match sols with

+//    | sol :: rest -> 

+//        let (newProg, newSol) = GetModularSol prog sol

+//        let newAcc = acc |> Map.add (fst newSol) (snd newSol)

+//        __Modularize newProg rest newAcc 

+//    | [] -> (prog, acc)

+//  (* --- function body starts here --- *) 

+//  __Modularize prog (Map.toList solutions) Map.empty 

diff --git a/Jennisys/Jennisys/examples/Set.jen b/Jennisys/Jennisys/examples/Set.jen
index 60a294c1..b867a007 100644
--- a/Jennisys/Jennisys/examples/Set.jen
+++ b/Jennisys/Jennisys/examples/Set.jen
@@ -40,13 +40,17 @@ class SetNode {
     requires x != y
     ensures elems = {x y}
 
-  constructor Double2(x: int, y: int)
+  constructor DoubleBase(x: int, y: int)
     requires x > y
     ensures elems = {x y}
 
   constructor Triple(x: int, y: int, z: int)
     requires x != y && y != z && z != x
     ensures elems = {x y z}
+
+  constructor TripleBase(x: int, y: int, z: int)
+    requires x < y && y < z
+    ensures elems = {x y z}
 }
 
 model SetNode {
diff --git a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
index f754d540..c9584a5f 100644
--- a/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
+++ b/Jennisys/Jennisys/examples/mod2/jennisys-synth_Set.dfy
@@ -30,14 +30,15 @@ class Set {
 

   method Double(p: int, q: int)

     modifies this;

+    requires p != q;

     ensures fresh(Repr - {this});

     ensures Valid();

     ensures elems == {p, q};

   {

-    var gensym67 := new SetNode;

-    gensym67.Double(p, q);

+    var gensym72 := new SetNode;

+    gensym72.Double(p, q);

     this.elems := {p, q};

-    this.root := gensym67;

+    this.root := gensym72;

     // repr stuff

     this.Repr := {this} + this.root.Repr;

   }

@@ -126,21 +127,6 @@ class SetNode {
   }

 

 

-  method Init(x: int)

-    modifies this;

-    ensures fresh(Repr - {this});

-    ensures Valid();

-    ensures elems == {x};

-  {

-    this.data := x;

-    this.elems := {x};

-    this.left := null;

-    this.right := null;

-    // repr stuff

-    this.Repr := {this};

-  }

-

-

   method Triple(x: int, y: int, z: int)

     modifies this;

     requires x != y;

@@ -151,64 +137,19 @@ class SetNode {
     ensures elems == {x, y, z};

   {

     if (x < y && z > y) {

-      var gensym80 := new SetNode;

-      var gensym81 := new SetNode;

-      gensym80.Init(z);

-      gensym81.Init(x);

-      this.data := y;

-      this.elems := {x, y, z};

-      this.left := gensym81;

-      this.right := gensym80;

-      // repr stuff

-      this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+      this.TripleBase(x, y, z);

     } else {

       if (z < x && y > x) {

-        var gensym80 := new SetNode;

-        var gensym81 := new SetNode;

-        gensym80.Init(y);

-        gensym81.Init(z);

-        this.data := x;

-        this.elems := {x, y, z};

-        this.left := gensym81;

-        this.right := gensym80;

-        // repr stuff

-        this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+        this.TripleBase(z, x, y);

       } else {

         if (x < z && y > z) {

-          var gensym80 := new SetNode;

-          var gensym81 := new SetNode;

-          gensym80.Init(y);

-          gensym81.Init(x);

-          this.data := z;

-          this.elems := {x, y, z};

-          this.left := gensym81;

-          this.right := gensym80;

-          // repr stuff

-          this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+          this.TripleBase(x, z, y);

         } else {

           if (z < y && x > y) {

-            var gensym80 := new SetNode;

-            var gensym81 := new SetNode;

-            gensym80.Init(x);

-            gensym81.Init(z);

-            this.data := y;

-            this.elems := {x, y, z};

-            this.left := gensym81;

-            this.right := gensym80;

-            // repr stuff

-            this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+            this.TripleBase(z, y, x);

           } else {

             if (y < z && x > z) {

-              var gensym80 := new SetNode;

-              var gensym81 := new SetNode;

-              gensym80.Init(x);

-              gensym81.Init(y);

-              this.data := z;

-              this.elems := {x, y, z};

-              this.left := gensym81;

-              this.right := gensym80;

-              // repr stuff

-              this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+              this.TripleBase(y, z, x);

             } else {

               var gensym80 := new SetNode;

               var gensym81 := new SetNode;

@@ -230,40 +171,72 @@ class SetNode {
 

   method Double(x: int, y: int)

     modifies this;

+    requires x != y;

     ensures fresh(Repr - {this});

     ensures Valid();

     ensures elems == {x, y};

   {

     if (y > x) {

-      var gensym77 := new SetNode;

-      gensym77.Init(y);

-      this.data := x;

-      this.elems := {x, y};

-      this.left := null;

-      this.right := gensym77;

-      // repr stuff

-      this.Repr := {this} + this.right.Repr;

+      this.DoubleBase(y, x);

     } else {

-      if (x > y) {

-        var gensym77 := new SetNode;

-        gensym77.Init(x);

-        this.data := y;

-        this.elems := {x, y};

-        this.left := null;

-        this.right := gensym77;

-        // repr stuff

-        this.Repr := {this} + this.right.Repr;

-      } else {

-        this.data := y;

-        this.elems := {x, y};

-        this.left := null;

-        this.right := null;

-        // repr stuff

-        this.Repr := {this};

-      }

+      this.DoubleBase(x, y);

     }

   }

 

+

+  method DoubleBase(x: int, y: int)

+    modifies this;

+    requires x > y;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y};

+  {

+    var gensym77 := new SetNode;

+    gensym77.Init(x);

+    this.data := y;

+    this.elems := {x, y};

+    this.left := null;

+    this.right := gensym77;

+    // repr stuff

+    this.Repr := {this} + this.right.Repr;

+  }

+

+

+  method Init(x: int)

+    modifies this;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x};

+  {

+    this.data := x;

+    this.elems := {x};

+    this.left := null;

+    this.right := null;

+    // repr stuff

+    this.Repr := {this};

+  }

+

+

+  method TripleBase(x: int, y: int, z: int)

+    modifies this;

+    requires x < y;

+    requires y < z;

+    ensures fresh(Repr - {this});

+    ensures Valid();

+    ensures elems == {x, y, z};

+  {

+    var gensym80 := new SetNode;

+    var gensym81 := new SetNode;

+    gensym80.Init(z);

+    gensym81.Init(x);

+    this.data := y;

+    this.elems := {x, y, z};

+    this.left := gensym81;

+    this.right := gensym80;

+    // repr stuff

+    this.Repr := ({this} + this.left.Repr) + this.right.Repr;

+  }

+

 }