Jennisys: SetNode.Find example

7 files changed, 36 insertions, 23 deletions

diff --git a/Jennisys/Jennisys/AstUtils.fs b/Jennisys/Jennisys/AstUtils.fs
index 83a6269c..c1e87dc3 100644
--- a/Jennisys/Jennisys/AstUtils.fs
+++ b/Jennisys/Jennisys/AstUtils.fs
@@ -375,11 +375,13 @@ let BinarySub lhs rhs = BinaryExpr(55, "-", lhs, rhs)
 //  =======================================================

 let BinaryIn lhs rhs = 

   match lhs, rhs with

+  | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 0 -> FalseLiteral

   | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 1 -> BinaryEq lhs (elist.[0])

   | _ -> BinaryExpr(40, "in", lhs, rhs)

 

 let BinaryNotIn lhs rhs = 

   match lhs, rhs with

+  | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 0 -> TrueLiteral

   | _, SequenceExpr(elist) | _, SetExpr(elist) when elist |> List.length = 1 -> BinaryNeq lhs (elist.[0])

   | _ -> BinaryExpr(40, "!in", lhs, rhs)

   

@@ -983,7 +985,7 @@ let EvalSym2 fullResolverFunc otherResolverFunc returnFunc ctx expr =
             match vars with

             | v :: restV -> 

                 try 

-                  let vDom = GetVarDomain fullResolverFunc returnFunc ctx v e

+                  let vDom = GetVarDomain resolverFunc returnFunc ctx v e

                   __ExhaustVar v restV vDom

                 with

                   | ex -> ForallExpr([v], __TraverseVars restV) 

@@ -1148,10 +1150,10 @@ let rec ExtractTopLevelExpressions stmt =
 let rec PullUpMethodCalls stmt = 

   let stmtList = new System.Collections.Generic.LinkedList<_>()

   let rec __PullUpMethodCalls expr = 

-    stmtList.Clear()

-    let newExpr = RewriteBU (function  

-                               | MethodOutSelect(_) as expr ->

-                                   let vname = SymGen.NewSym

+    let newExpr = RewriteBU (fun expr ->  

+                               match expr with

+                               | MethodOutSelect(_) ->

+                                   let vname = SymGen.NewSymFake expr

                                    let e' = VarLiteral(vname)

                                    let var = VarDeclExpr([Var(vname,None)], true)

                                    let asgn = BinaryGets var expr

@@ -1160,6 +1162,7 @@ let rec PullUpMethodCalls stmt =
                                | _ -> None

                             ) expr

     newExpr, (stmtList |> List.ofSeq)

+  stmtList.Clear()

   match stmt with

   | ExprStmt(e)    -> 

       let e', slist = __PullUpMethodCalls e

diff --git a/Jennisys/Jennisys/FixpointSolver.fs b/Jennisys/Jennisys/FixpointSolver.fs
index 40b43386..ef6e8e43 100644
--- a/Jennisys/Jennisys/FixpointSolver.fs
+++ b/Jennisys/Jennisys/FixpointSolver.fs
@@ -165,7 +165,7 @@ let rec ComputeClosure heapInst expandExprFunc premises =
   

   let MySetAdd expr set =

     let x = Printer.PrintExpr 0 expr

-    if x.Contains("$") then

+    if x.Contains("$") || not (expandExprFunc expr) then

       set

     else 

       match expr with

@@ -324,12 +324,15 @@ let rec ComputeClosure heapInst expandExprFunc premises =
     | [] -> premises

 

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

-  let premises' = __Iter (premises |> Set.toList) premises

-  if premises' = premises then

-    premises'

-  else 

-    //Logger.TraceLine "-----------------------"

-    //premises' |> Set.iter (fun e -> Logger.TraceLine (Printer.PrintExpr 0 e))

-    ComputeClosure heapInst expandExprFunc premises' 

+  let iterOnceFunc p = __Iter (p |> Set.toList) p

+  // TODO: iterate only 3 times, instead of to full closure

+  iterOnceFunc premises |> iterOnceFunc |> iterOnceFunc

+//  let premises' = iterOnceFunc premises 

+//  if premises' = premises then

+//    premises'

+//  else 

+//    Logger.TraceLine "-------closure----------------"

+//    //premises' |> Set.iter (fun e -> Logger.TraceLine (Printer.PrintExpr 0 e))

+//    ComputeClosure heapInst expandExprFunc premises' 

 

 

diff --git a/Jennisys/Jennisys/Jennisys.fs b/Jennisys/Jennisys/Jennisys.fs
index 6dd2d26a..f65aff17 100644
--- a/Jennisys/Jennisys/Jennisys.fs
+++ b/Jennisys/Jennisys/Jennisys.fs
@@ -60,4 +60,12 @@ with
       printfn "%s" PrintHelpMsg
   | EvalFailed(msg) as ex -> 
       printfn "  [EVALUATION ERROR]  %s" msg
-      printfn "%O" ex.StackTrace 
\ No newline at end of file
+      printfn "%O" ex.StackTrace 
+
+//let mc = MethodOutSelect (MethodCall(IdLiteral("left"),"SetNode","Find",[VarLiteral("n")]), "ret")
+//let expr = BinaryOr (BinaryOr (BinaryEq (VarLiteral("a")) (VarLiteral("b"))) mc) (mc) 
+//printfn "%s" (PrintExpr 0 expr)
+//printfn ""
+//
+//let stmt = ExprStmt(expr)
+//printfn "%s" (DafnyPrinter.PrintStmt stmt 0 false)
\ No newline at end of file
diff --git a/Jennisys/Jennisys/Jennisys.fsproj b/Jennisys/Jennisys/Jennisys.fsproj
index f84066fc..e7e129f8 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 /genMod /genRepr /method:SetNode.Find</StartArguments>

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

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

   </PropertyGroup>

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

diff --git a/Jennisys/Jennisys/MethodUnifier.fs b/Jennisys/Jennisys/MethodUnifier.fs
index 62800dcd..0a6ec6a6 100644
--- a/Jennisys/Jennisys/MethodUnifier.fs
+++ b/Jennisys/Jennisys/MethodUnifier.fs
@@ -49,7 +49,7 @@ let ApplyMethodUnifs receiver (c,m) unifs =
   let outs = GetMethodOutArgs m |> __Apply

   

   let retVars, asgs = outs |> List.fold (fun (acc1,acc2) e -> 

-                                          let vname = SymGen.NewSym

+                                          let vname = SymGen.NewSymFake e

                                           let v = Var(vname, None)

                                           let acc1' = acc1 @ [v]

                                           let acc2' = acc2 @ [ArbitraryStatement(Assign(VarLiteral(vname), e))]

diff --git a/Jennisys/Jennisys/SymGen.fs b/Jennisys/Jennisys/SymGen.fs
index a2e783ad..b736ef31 100644
--- a/Jennisys/Jennisys/SymGen.fs
+++ b/Jennisys/Jennisys/SymGen.fs
@@ -1,9 +1,9 @@
 module SymGen

 

-let cnt = ref 0

+let incr =

+  let counter = ref 0

+  fun () ->

+    counter := !counter + 1

+    !counter

 

-let NewSym = 

-  let sym = sprintf "x_%d" !cnt

-  cnt := !cnt + 1

-  sym

-   
\ No newline at end of file
+let NewSymFake expr = sprintf "x_%d" (incr())
\ No newline at end of file
diff --git a/Jennisys/Jennisys/examples/List.jen b/Jennisys/Jennisys/examples/List.jen
index 376d2e29..29e6faf7 100644
--- a/Jennisys/Jennisys/examples/List.jen
+++ b/Jennisys/Jennisys/examples/List.jen
@@ -35,7 +35,6 @@ class Node[T] {
     ensures list = [p q]
 
   method List() returns (lst: seq[T])
-    requires |list| = 1
     ensures lst = list
 
   method Tail() returns (tail: Node[T])