From df26c0f2318b3f866643c590cdb2203cf1be1079 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 9 Apr 2021 08:13:53 -0700 Subject: [PATCH] [sledge] Work harder to detect infeasible paths when executing assume Summary: Switch to a stronger but more expensive operation to check if a symbolic heap is unsatisfiable. Reviewed By: ngorogiannis Differential Revision: D27564872 fbshipit-source-id: c8e306408 --- sledge/src/domain_sh.ml | 2 +- sledge/src/sh.mli | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 3173ce687..7fb38ed91 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -46,7 +46,7 @@ let dnf = Sh.dnf let exec_assume q b = Exec.assume q (X.formula b) |> simplify - |> fun q -> if Sh.is_unsat q then None else Some q + |> fun q -> if Sh.is_unsat_dnf q then None else Some q let exec_kill r q = Exec.kill q (X.reg r) |> simplify diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli index 405850ec8..c22d10a91 100644 --- a/sledge/src/sh.mli +++ b/sledge/src/sh.mli @@ -117,6 +117,10 @@ val is_unsat : t -> bool (** Holds only of inconsistent formulas, does not hold of all inconsistent formulas. *) +val is_unsat_dnf : t -> bool +(** Holds only of inconsistent formulas, does not hold of all inconsistent + formulas. Like [is_unsat] but more complete and expensive. *) + val is_empty : t -> bool (** Holds only if all satisfying states have empty heap. *)