Web z3

songyahui · May 14, 2023 · 71ba312 · 71ba312
1 parent 89e4fae
commit 71ba312
Show file tree

Hide file tree

Showing 5 changed files with 59 additions and 61 deletions.
diff --git a/parsing/Pretty.ml b/parsing/Pretty.ml
@@ -393,7 +393,7 @@ let mergeState (pi1, h1) (pi2, h2) =
   (*print_endline (string_of_kappa (SepConj (h1, h2)) ^ " =====> ");
   print_endline (string_of_kappa heap ^ "   and    " ^ string_of_pi unification);
 *)
-  (Provers.normalPure (And (pi1, pi2)), heap)
+  (ProversEx.normalize_pure (And (pi1, pi2)), heap)
 
 
 let rec string_of_normalisedStagedSpec (spec:normalisedStagedSpec) : string = 
@@ -515,7 +515,7 @@ let normalise_stagedSpec (acc:normalisedStagedSpec) (stagedSpec:stagedSpec) : no
     let (h2',   unification')    = normaliseMagicWand h3 h2 existential false in 
 
 
-    let normalStage' = (existential, mergeState req (And(p3, unification), magicWandHeap), (Provers.normalPure (And(p2, unification')), h2'), ret) in 
+    let normalStage' = (existential, mergeState req (And(p3, unification), magicWandHeap), (ProversEx.normalize_pure (And(p2, unification')), h2'), ret) in 
     (effectStages, normalStage')
 
   | NormalReturn (pi, heap, ret') -> (effectStages, (existential, req, mergeState ens (pi, heap), ret'))
@@ -642,7 +642,7 @@ let rec detectfailedAssertions (spec:spec) : spec =
   | [] -> []
   | Require (pi, heap) :: xs  -> 
     (
-      let pi' = Provers.normalPure pi in 
+      let pi' = ProversEx.normalize_pure pi in 
       match ProversEx.entailConstrains pi' (False) with 
       | true  -> [Require (False , heap)]
       | _ -> Require (pi' , heap) ::  detectfailedAssertions xs 

diff --git a/provers/js/provers.ml b/provers/js/provers.ml
@@ -1,22 +1,36 @@
 open Hiptypes
 
+(*
+https://github.com/Z3Prover/z3/blob/master/src/api/js/examples/high-level/miracle-sudoku.ts
+https://microsoft.github.io/z3guide/programming/Z3%20JavaScript%20Examples/
+*)
+
+(*
+x = ctx.Int.const('x')
+s = new ctx.Solver()
+s.add(ctx.Int.const('x').eq(1))
+r = await s.check()
++s.model().eval(x)
+
+s = new ctx.Solver()
+a = ctx.Int.const('a')
+s.add(ctx.Exists([a], a.eq(1)))
+r = await s.check()
+*)
+
 let rec build_term : Jv.t -> term -> Jv.t =
  fun ctx t ->
   match t with
   | Plus (a, b) ->
-    (* Brr.Console.(log [str "zz1"; ctx; build_term ctx a]); *)
     Jv.call (build_term ctx a) "add" [| build_term ctx b |]
     (* Jv.call ctx "Add" [| build_term ctx a; build_term ctx b |] *)
   | Minus (a, b) -> Jv.call (build_term ctx a) "sub" [| build_term ctx b |]
   | Num n ->
     (* Jv.of_int n *)
-    Jv.call (Jv.get ctx "Int") "const" [| Jv.of_int n |]
-  | Var s ->
-    (* TODO may have to keep track of bindings... *)
-    (* Brr.Console.(
-       log [str "zz"; Jv.get ctx "Int"; Jv.get (Jv.get ctx "Int") "const"]); *)
-    Jv.call (Jv.get ctx "Int") "const" [| Jv.of_string s |]
-  | UNIT | TList _ | TTupple _ -> failwith ""
+    Jv.call (Jv.get ctx "Int") "val" [| Jv.of_int n |]
+  | Var s -> Jv.call (Jv.get ctx "Int") "const" [| Jv.of_string s |]
+  | UNIT -> failwith "TODO"
+  | TList _ | TTupple _ -> failwith "not yet implemented"
 
 let build_op : Jv.t -> bin_op -> term -> term -> Jv.t =
  fun ctx op a b ->
@@ -37,50 +51,57 @@ let rec build_fml : pi -> Jv.t -> Jv.t =
   | Not a -> Jv.apply (Jv.get ctx "Not") [| build_fml a ctx |]
   | Imply (a, b) ->
     Jv.apply (Jv.get ctx "Implies") [| build_fml a ctx; build_fml b ctx |]
-  | True -> Jv.of_bool true
-  | False -> Jv.of_bool false
+  | True ->
+    Jv.call (Jv.get ctx "Bool") "val" [| Jv.of_bool true |]
+    (* Jv.of_bool true *)
+  | False ->
+    (* Jv.of_bool false *)
+    Jv.call (Jv.get ctx "Bool") "val" [| Jv.of_bool true |]
   | Atomic (op, a, b) -> build_op ctx op a b
   | Predicate (_, _) -> failwith "not implemented"
-(* | Or (a, b) -> Jv.apply (Jv.get ctx "Or") [| (build_fml a ctx ); (build_fml b ctx ) |] *)
-(* ctx *)
-
-(* let solve () =
-   Console.(log [str "calling solve from ocaml1"]);
-   (* Console.(log [Jv.get Jv.global "z3"]) *)
-   (* ; *)
-   let f = build_fml (And (True, True)) in
-   let k sat = Console.(log [str ("ocaml: sat? " ^ string_of_bool sat)]) in
-   Jv.apply
-     (Jv.get (Jv.get Jv.global "z3") "solve")
-     [| Jv.callback ~arity:1 f; Jv.callback ~arity:1 k |]
-   |> ignore *)
 
 open Effect
 open Effect.Deep
 
-type _ Effect.t += Ask : pi -> bool t
+(* function is from ctx to z3 expression *)
+type _ Effect.t += Ask : (Jv.t -> Jv.t) -> bool t
 
-let askZ3 v = perform (Ask v)
+let askZ3 p = perform (Ask (build_fml p))
 let valid p = not (askZ3 (Not p))
-let entails_exists _ _ _ = true
-let normalPure p = p
+
+(* check if p1 => ex vs. p2 is valid *)
+let entails_exists p1 vs p2 =
+  let f ctx =
+    Jv.apply (Jv.get ctx "Not")
+      [|
+        Jv.apply (Jv.get ctx "Implies")
+          [|
+            build_fml p1 ctx;
+            Jv.apply (Jv.get ctx "Exists")
+              [|
+                Jv.of_list
+                  (fun v ->
+                    Jv.call (Jv.get ctx "Int") "const" [| Jv.of_string v |])
+                  vs;
+                build_fml p2 ctx;
+              |];
+          |];
+      |]
+  in
+  not (perform (Ask f))
 
 let handle f =
   try_with f ()
     {
       effc =
         (fun (type a) (eff : a t) ->
           match eff with
-          | Ask pi ->
+          | Ask make_pi ->
             Some
               (fun (k : (a, _) continuation) ->
-                let f ctx = build_fml pi ctx in
-                let k1 sat =
-                  (* print_endline "got result!!"; *)
-                  continue k sat
-                in
+                let k1 sat = continue k sat in
                 (Jv.call (Jv.get Jv.global "z3") "solve")
-                  [| Jv.callback ~arity:1 f; Jv.callback ~arity:1 k1 |]
+                  [| Jv.callback ~arity:1 make_pi; Jv.callback ~arity:1 k1 |]
                 |> ignore)
           | _ -> None);
     }
diff --git a/provers/native/provers.ml b/provers/native/provers.ml
@@ -138,27 +138,4 @@ let askZ3 pi =
     let () = historyTable := (hash_pi pi, re) :: !historyTable in
     re
 
-let rec normalPure (pi : pi) : pi =
-  match pi with
-  | And (p1, p2) ->
-    let p1 = normalPure p1 in
-    let p2 = normalPure p2 in
-    (match (p1, p2) with
-    | True, _ -> p2
-    | _, True -> p1
-    | False, _ -> False
-    | _, False -> False
-    | _, _ -> And (p1, p2))
-  | Or (p1, p2) ->
-    let p1 = normalPure p1 in
-    let p2 = normalPure p2 in
-    (match (p1, p2) with
-    | True, _ -> True
-    | _, True -> True
-    | False, _ -> p2
-    | _, False -> p1
-    | _, _ -> Or (p1, p2))
-  | Not p1 -> Not (normalPure p1)
-  | _ -> pi
-
 let handle f = f ()
diff --git a/provers/provers.mli b/provers/provers.mli
@@ -4,4 +4,3 @@ val askZ3 : pi -> bool
 val valid : pi -> bool
 val entails_exists : pi -> string list -> pi -> bool
 val handle : (unit -> unit) -> unit
-val normalPure : pi -> pi
diff --git a/web/main.js b/web/main.js
@@ -28,6 +28,7 @@ function solve(f, k) {
 
   // const { Context } = init();
   const ctx = new Context("main");
+  window.ctx = ctx;
   // const { Solver, Int, And } = ctx;
   // const x = Int.const('x');
   const solver = new ctx.Solver();