From edb60837b35f5b1815a9ddfeb6a3f6782111a3c1 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:24:52 -0800
Subject: [PATCH] [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 | 2 +-
sledge/src/exec.ml | 2 +-
sledge/src/sh.ml | 8 +++++---
sledge/src/sh.mli | 2 +-
sledge/src/solver.ml | 4 ++--
5 files changed, 10 insertions(+), 8 deletions(-)
diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 48acfd8f2..396ec1501 100644
--- a/sledge/src/domain_sh.ml
+++ b/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
diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 9be20df12..da67e0f9a 100644
--- a/sledge/src/exec.ml
+++ b/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
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index d6bb98f19..764a6001c 100644
--- a/sledge/src/sh.ml
+++ b/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 *)
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 212b6c393..e672fd4cc 100644
--- a/sledge/src/sh.mli
+++ b/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. *)
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 309a5e41c..678ceb72c 100644
--- a/sledge/src/solver.ml
+++ b/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]