Check for satisfiability in other sorts in term abduction validation …

…procedure. Two ways to pass `validate` in `Joint` abduction.

examples/liquid_bsearch2_harder3.ml.target

@@ -30,9 +30,9 @@ let bsearch
   (fun key vec ->
     let Ex3 xcase =
     let rec look :
-    type (*i*) (*j*) (*k*) b (*0 ≤ k + 1 ∧ 0 ≤ i ∧
-    k + 1 ≤ j*). (b -> (b (* j *)) array -> (* i *) num -> (* k *) num ->
-                     (* k *) ex3)
+    type (*i*) (*k*) (*n*) a (*0 ≤ n + 1 ∧ 0 ≤ k ∧
+    n + 1 ≤ i*). (a -> (a (* i *)) array -> (* k *) num -> (* n *) num ->
+                     (* n *) ex3)
     =
     (fun key vec lo hi ->
       (if lo <= hi then
@@ -44,6 +44,6 @@ let bsearch
         | EQ ->
             (if equal key x then let xcase = m in Ex3 xcase else
             let xcase = -1 in Ex3 xcase))) :
-      (* k *) ex3) else let xcase = -1 in Ex3 xcase)) in
+      (* n *) ex3) else let xcase = -1 in Ex3 xcase)) in
     look key vec 0 (array_length vec + -1) in Ex4 xcase)
 

examples/liquid_gauss_asserted.gadti.target

@@ -71,4 +71,4 @@ val rowElim :
    ∀i, j, k, n[0 ≤ n ∧ k ≤ i ∧ n + 1 ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()
+val gauss : ∀n[0 ≤ n]. Matrix (n, n + 1) → ()

examples/liquid_gauss_simpler_asserted.gadti.target

@@ -71,4 +71,4 @@ external rowElim :
    ∀i, j, k, n[0 ≤ n ∧ n + 1 ≤ i ∧ k ≤ i ∧ k ≤ j].
    Array (Float, j) → Array (Float, i) → Num k → Num n → ()
 
-val gauss : ∀n[1 ≤ n]. Matrix (n, n + 1) → ()
+val gauss : ∀n[0 ≤ n]. Matrix (n, n + 1) → ()

examples/liquid_simplex_step_3a.gadti.target

@@ -44,4 +44,4 @@ external is_neg_aux :
 external is_neg :
    ∀i, k, n[1 ≤ k ∧ n ≤ i + 1]. Matrix (k, i) → Num n → Bool
 
-val main_step3_test : ∀k, n[1 ≤ n ∧ 3 ≤ k]. Matrix (n, k) → Float
+val main_step3_test : ∀k, n[1 ≤ n ∧ 2 ≤ k]. Matrix (n, k) → Float

src/Abduction.ml

@@ -33,7 +33,7 @@ let residuum q prem concl =
   let concl = to_formula concl in
   solve ~use_quants:false q (subst_formula prem concl)
 
-type t_validation = (VarSet.t * subst) list
+type t_validation = (VarSet.t * (subst * NumS.state)) list
 (* Result remembers the invariant parameters [bvs]. *)
 exception Result of VarSet.t * var_name list * subst * t_validation
 
@@ -243,16 +243,19 @@ let connecteds_vs tvs sb =
 (* FIXME: do we need to check the state of numerical constraints? *)
 let validate q validation added_vs x t lc =
   List.map
-    (fun (br_vs, state as br) ->
+    (fun (br_vs, (state_typ, state_num) as br) ->
        if not (VarSet.is_empty (VarSet.inter added_vs br_vs))
        then
          try
-           let t', _ = VarMap.find x state in
+           let t', _ = VarMap.find x state_typ in
            let upd =
-             unify ~use_quants:false ~sb:state q [Eqty (t, t', lc)] in
-           VarSet.union added_vs br_vs, upd.cnj_typ
+             unify ~use_quants:false ~sb:state_typ q [Eqty (t, t', lc)] in
+           let state_num =
+             NumS.satisfiable_exn ~state:state_num upd.cnj_num in
+           VarSet.union added_vs br_vs, (upd.cnj_typ, state_num)
          with Not_found ->
-           VarSet.union added_vs br_vs, VarMap.add x (t, lc) state
+           VarSet.union added_vs br_vs,
+           (VarMap.add x (t, lc) state_typ, state_num)
        else br)
     validation
 
@@ -748,13 +751,14 @@ module TermAbd = struct
   type discarded = answer
   (* premise including alien premise, conclusion *)
   type branch = sep_formula * subst
-  type br_state = subst
+  type br_state = subst * NumS.state
   type validation = t_validation
 
   let abd_fail_timeout = fail_timeout_count
   let abd_fail_flag = abd_fail_flag
 
-  let abd_simple (obvs, q, dissociate) ~discard ~validation ~neg_validate
+  let abd_simple (obvs, q, dissociate) ~discard ~validation
+      ~validate ~neg_validate
       (bvs, acc) br =
     abd_simple q ~obvs ~bvs ~dissociate ~validation ~neg_validate
         ~discard 0 acc br
@@ -804,8 +808,9 @@ let abd_typ q ~bvs ?(dissociate=false) ~validation ~neg_validate ~discard
     else brs in
   (*[* Format.printf "abd_typ: alien_eqs=%a@\n%!"
     pr_subst !alien_eqs; *]*)
+  let validate _ _ = () in
   let cand_bvs, (vs, ans) =
-    JCA.abd (bvs, q, dissociate) ~discard validation ~neg_validate
+    JCA.abd (bvs, q, dissociate) ~discard validation ~validate ~neg_validate
       (bvs, ([], VarMap.empty)) brs in
   (*[* Format.printf "abd_typ: result vs=%s@\nans=%a@\n%!"
     (String.concat ","(List.map var_str vs))
@@ -843,28 +848,28 @@ let abd_typ q ~bvs ?(dissociate=false) ~validation ~neg_validate ~discard
 let abd_mockup_num q ~bvs brs =
   (* Do not change the order and no. of branches afterwards. *)
   let brs_typ, brs_num = List.split
-    (map_some (fun (prem, concl) ->
-      let prems_opt =
-        try Some (unify ~use_quants:false q prem)
-        with Contradiction _ -> None in
-      match prems_opt with
-      | Some prem ->
-        if List.exists
-          (function CFalse _ -> true | _ -> false) prem.cnj_so
-        then None
-        else                          (* can raise Contradiction *)
-          let {cnj_typ=concl_typ; cnj_num=concl_num; cnj_so=concl_so} =
-            solve ~use_quants:false q concl in
-          List.iter (function
-          | CFalse loc ->
-            raise (Contradiction (Type_sort,
-                                  "assert false is possible", None, loc))
-          | _ -> ()) concl_so;
-          if not (is_right (NumS.satisfiable concl_num)) then None
-          else Some ((prem, concl_typ),
-                     (prem.cnj_num, concl_num))
-      | None -> None)
-       brs) in
+      (map_some (fun (prem, concl) ->
+           let prems_opt =
+             try Some (unify ~use_quants:false q prem)
+             with Contradiction _ -> None in
+           match prems_opt with
+           | Some prem ->
+             if List.exists
+                 (function CFalse _ -> true | _ -> false) prem.cnj_so
+             then None
+             else                          (* can raise Contradiction *)
+               let {cnj_typ=concl_typ; cnj_num=concl_num; cnj_so=concl_so} =
+                 solve ~use_quants:false q concl in
+               List.iter (function
+                   | CFalse loc ->
+                     raise (Contradiction (Type_sort,
+                                           "assert false is possible", None, loc))
+                   | _ -> ()) concl_so;
+               if not (is_right (NumS.satisfiable concl_num)) then None
+               else Some ((prem, concl_typ),
+                          (prem.cnj_num, concl_num))
+           | None -> None)
+          brs) in
   let verif_brs = List.map2
       (fun (prem, concl_ty) (_, concl_num) ->
          VarSet.union (fvs_sb prem.cnj_typ)
@@ -874,17 +879,18 @@ let abd_mockup_num q ~bvs brs =
          prem, concl_ty, concl_num)
       brs_typ brs_num in
   let validation =
-    List.map
-    (fun (br_vs, prem, concl_ty, concl_num) ->
-        (* Do not use quantifiers, because premise is in the conjunction. *)
-        (* TODO: after cleanup optimized in abd_simple, pass clean_ans
-           and remove cleanup here *)
-        let {cnj_typ=sb_ty; cnj_num=_(* ans_num *); cnj_so=_} =
-          combine_sbs q [prem.cnj_typ; concl_ty] in
-        (* let cnj_num = ans_num @ prem.cnj_num @ concl_num in *)
-        (* FIXME: need num state? *)
-        br_vs, (sb_ty (*, NumS.satisfiable cnj_num*)))
-    verif_brs in
+    map_some
+      (fun (br_vs, prem, concl_ty, concl_num) ->
+         (* Do not use quantifiers, because premise is in the conjunction. *)
+         (* TODO: after cleanup optimized in abd_simple, pass clean_ans
+            and remove cleanup here *)
+         try
+           let {cnj_typ=sb_ty; cnj_num=ans_num; cnj_so=_} =
+             combine_sbs q [prem.cnj_typ; concl_ty] in
+           let cnj_num = ans_num @ prem.cnj_num @ concl_num in
+           Some (br_vs, (sb_ty, NumS.satisfiable_exn cnj_num))
+         with Contradiction _ -> None)
+      verif_brs in
   let neg_validate _ = 0 in
   try
     let cand_bvs, alien_eqs, tvs, ans_typ, more_in_brs =
@@ -951,17 +957,19 @@ let abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars
          prem, concl_ty, concl_num)
       brs_typ brs_num in
   let validation =
-    List.map
-    (fun (br_vs, prem, concl_ty, concl_num) ->
-        (* Do not use quantifiers, because premise is in the conjunction. *)
-        (* TODO: after cleanup optimized in abd_simple, pass clean_ans
-           and remove cleanup here *)
-        let {cnj_typ=sb_ty; cnj_num=_(* ans_num *); cnj_so=_} =
-          combine_sbs q [prem.cnj_typ; concl_ty] in
-        (* let cnj_num = ans_num @ prem.cnj_num @ concl_num in *)
-        (* FIXME: need num state? *)
-        br_vs, (sb_ty (*, NumS.satisfiable cnj_num*)))
-    verif_brs in
+    map_some
+      (fun (br_vs, prem, concl_ty, concl_num) ->
+         try
+           (* Do not use quantifiers, because premise is in the conjunction. *)
+           (* TODO: after cleanup optimized in abd_simple, pass clean_ans
+              and remove cleanup here *)
+           let {cnj_typ=sb_ty; cnj_num=ans_num; cnj_so=_} =
+             combine_sbs q [prem.cnj_typ; concl_ty] in
+           let cnj_num = ans_num @ prem.cnj_num @ concl_num in
+           (* FIXME: need num state? *)
+           Some (br_vs, (sb_ty, NumS.satisfiable_exn cnj_num))
+         with Contradiction _ -> None)
+      verif_brs in
   (* TODO: could be optimized too. *)
   let neg_validate (vs, ans) =
     (* Returns the number of negative constraints not contradicted by

src/Abduction.mli

@@ -44,7 +44,7 @@ val num_neg_since : int ref
 val abd_fail_flag : bool ref
 val abd_timeout_flag : bool ref
 
-type t_validation = (Defs.VarSet.t * Terms.subst) list
+type t_validation = (Defs.VarSet.t * (Terms.subst * NumS.state)) list
 
 val abd_simple :
   Defs.quant_ops ->

src/InvarGenTTest.ml

@@ -202,7 +202,6 @@ let tests = "InvarGenT" >::: [
            test_case "flatten_pairs" ());
       "flatten_quadrs" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "flatten_quadrs" ());
       "flatten_septs" >::
@@ -440,12 +439,10 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_bcopy" ());
       "liquid_bsearch-simpler" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch_simpler" ());
       "liquid_bsearch" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch" ());
       "liquid_bsearch-harder" >::
@@ -463,22 +460,18 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_bsearch2_simpler2" ());
       "liquid_bsearch2" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch2" ());
       "liquid_bsearch2-harder1" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch2_harder1" ());
       "liquid_bsearch2-harder2" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_bsearch2_harder2" ());
       "liquid_bsearch2-harder3" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case ~test_annot:true "liquid_bsearch2_harder3" ());
       "liquid_bsearch2-harder4" >::
@@ -519,11 +512,11 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_isort" ());
       "liquid_isort-harder" >::
         (fun () ->
+           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_isort_harder" ());
       "liquid_vecswap_simpler" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_vecswap_simpler" ());
       "liquid_vecswap" >::
@@ -532,6 +525,7 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_vecswap" ());
       "liquid_isort-full" >::
         (fun () ->
+           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_isort_full" ());
       "liquid_tower_showposts" >::
@@ -544,7 +538,6 @@ let tests = "InvarGenT" >::: [
            test_case "liquid_tower_simpler" ());
       "liquid_tower_asserted" >::
         (fun () ->
-           todo "FIXME";
            skip_if !debug "debug";
            test_case "liquid_tower_asserted" ());
       "liquid_tower" >::

src/InvariantsTest.ml

@@ -815,6 +815,7 @@ let rec plus =
 
   "binary plus asserted" >::
     (fun () ->
+       todo "FIXE";
        skip_if !debug "debug";
        test_case "binary plus"
 "datatype Binary : num

src/Joint.ml

@@ -23,6 +23,7 @@ module type ABD_PARAMS = sig
   val abd_simple :
     args -> discard:discarded list ->
     validation:validation ->
+    validate:(VarSet.t -> answer -> unit) ->    
     neg_validate:(answer -> int) ->
     accu -> branch -> (accu * validation) option
   val extract_ans : accu -> answer
@@ -37,7 +38,8 @@ let debug_dep = ref 0
 
 module JointAbduction (P : ABD_PARAMS) = struct
 
-  let abd args ~discard (init_validation : P.validation) ~neg_validate
+  let abd args ~discard (init_validation : P.validation)
+      ~validate ~neg_validate
       init_acc brs =
     P.abd_fail_flag := false;
     let culprit = ref None
@@ -58,7 +60,7 @@ module JointAbduction (P : ABD_PARAMS) = struct
           (List.length aside_brs)
           (List.length more_brs) P.pr_branch br; *]*)
         match P.abd_simple args ~discard ~validation
-                ~neg_validate acc br with
+                ~validate ~neg_validate acc br with
         | Some (acc, validation) ->
           loop fails discard acc validation (br::done_brs)
             aside_brs more_brs
@@ -90,7 +92,7 @@ module JointAbduction (P : ABD_PARAMS) = struct
           ddepth (List.length discard) (List.length done_brs)
           (List.length aside_brs) P.pr_branch br; *]*)
         match P.abd_simple args ~discard ~validation
-                ~neg_validate acc br with
+                ~validate ~neg_validate acc br with
         | Some (acc, validation) ->
           check_aside fails best discard acc validation (br::done_brs)
             aside_brs

src/Joint.mli

@@ -21,10 +21,12 @@ module type ABD_PARAMS = sig
   val abd_fail_timeout : int ref
   val abd_fail_flag : bool ref
   (** The variables passed to [validate] should be the variables of
-      the atom whose addition to the partial answer is being validated. *)
+      the atom whose addition to the partial answer is being
+      validated. Usually only one of [validation], [validate] is used. *)
   val abd_simple :
     args -> discard:discarded list ->
     validation:validation ->
+    validate:(VarSet.t -> answer -> unit) ->    
     neg_validate:(answer -> int) ->
     accu -> branch -> (accu * validation) option
   val extract_ans : accu -> answer
@@ -41,6 +43,7 @@ module JointAbduction (P : ABD_PARAMS) : sig
   val abd :
     P.args -> discard:P.discarded list ->
     P.validation ->
+    validate:(VarSet.t -> P.answer -> unit) ->
     neg_validate:(P.answer -> int) ->
     P.accu -> P.branch list -> P.accu
 end