[sledge] Rename Sh.is_false to is_unsat

Summary:
Sh.is_false checks if the pure constraints are inconsistent with the
first-order consequences of the spatial constraints. This involves
some, though not very expensive, logical reasoning. But is it not
checking only testing for the representation of Sh.false_, which one
might expect from its name. This renaming also makes room for the
operation that does test for the representation of Sh.false_.

Reviewed By: jvillard

Differential Revision: D25756580

fbshipit-source-id: 30510f45a

sledge/src/domain_sh.ml

@@ -41,7 +41,7 @@ let join p q =
   |>
   [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" pp)]
 
-let is_false = Sh.is_false
+let is_false = Sh.is_unsat
 let dnf = Sh.dnf
 let exec_assume q b = Exec.assume q (X.formula b) |> Option.map ~f:simplify
 let exec_kill r q = Exec.kill q (X.reg r) |> simplify

sledge/src/exec.ml

@@ -719,7 +719,7 @@ let exec_specs pre specs =
 
 let assume pre cnd =
   let post = Sh.and_ cnd pre in
-  if Sh.is_false post then None else Some post
+  if Sh.is_unsat post then None else Some post
 
 let kill pre reg =
   let ms = Var.Set.of_ reg in

sledge/src/sh.ml

@@ -592,7 +592,9 @@ let pure_approx q =
   |>
   [%Trace.retn fun {pf} -> pf "%a" Formula.pp]
 
-let is_false q = Context.refutes q.ctx (pure_approx q)
+(** test if pure constraints are inconsistent with first-order consequences
+    of spatial constraints *)
+let is_unsat q = Context.refutes q.ctx (pure_approx q)
 
 let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
   let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts =
@@ -696,7 +698,7 @@ let rec propagate_context_ ancestor_vs ancestor_ctx q =
          let djn_xs = Var.Set.diff (Context.fv djn_ctx) q'.us in
          let djn = List.map ~f:(elim_exists djn_xs) djn in
          let ctx_djn = and_ctx_ djn_ctx (orN djn) in
-         assert (is_false ctx_djn || Var.Set.subset new_xs ~of_:djn_xs) ;
+         assert (is_unsat ctx_djn || Var.Set.subset new_xs ~of_:djn_xs) ;
          star (exists djn_xs ctx_djn) q' ))
   |>
   [%Trace.retn fun {pf} q' ->
@@ -754,7 +756,7 @@ let rec simplify_ us rev_xss q =
   let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in
   let removed, q =
     (* simplification can reveal inconsistency *)
-    if is_false q then (Var.Set.empty, false_ q.us)
+    if is_unsat q then (Var.Set.empty, false_ q.us)
     else if Context.Subst.is_empty subst then (Var.Set.empty, q)
     else
       (* normalize wrt solutions *)

sledge/src/sh.mli

@@ -113,7 +113,7 @@ val extend_us : Var.Set.t -> t -> t
 
 (** Query *)
 
-val is_false : t -> bool
+val is_unsat : t -> bool
 (** Holds only of inconsistent formulas, does not hold of all inconsistent
     formulas. *)
 

sledge/src/solver.ml

@@ -639,10 +639,10 @@ let pure_entails x q = Sh.is_empty q && Context.implies x (Sh.pure_approx q)
 
 let rec excise ({min; xs; sub; zs; pgs} as goal) =
   [%Trace.info "@[<2>excise@ %a@]" pp goal] ;
-  if Sh.is_false min then Some (Sh.false_ (Var.Set.diff sub.us zs))
+  if Sh.is_unsat min then Some (Sh.false_ (Var.Set.diff sub.us zs))
   else if pure_entails min.ctx sub then
     Some (Sh.exists zs (Sh.extend_us xs min))
-  else if Sh.is_false sub then None
+  else if Sh.is_unsat sub then None
   else if pgs then
     goal |> with_ ~pgs:false |> excise_exists |> excise_heap >>= excise
   else None $> fun _ -> [%Trace.info "@[<2>excise fail@ %a@]" pp goal]