[sledge] Delay unsat check in exec_assume until after simplify

Summary:
Sh.simplify propagates first-order constraints over the formula's
propositional structure, and can reveal inconsistency. It is therefore
sometimes beneficial to check consistency after simplifying rather
than before.

Reviewed By: jvillard

Differential Revision: D25756585

fbshipit-source-id: 2a205c965

sledge/src/domain_sh.ml

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

sledge/src/exec.ml

@@ -722,10 +722,8 @@ let exec_specs pre specs =
 let assume pre cnd =
   [%trace]
     ~call:(fun {pf} -> pf "%a" Formula.pp cnd)
-    ~retn:(fun {pf} -> pf "%a" pp)
-  @@ fun () ->
-  let post = Sh.and_ cnd pre in
-  if Sh.is_unsat post then None else Some post
+    ~retn:(fun {pf} -> pf "%a" Sh.pp)
+  @@ fun () -> Sh.and_ cnd pre
 
 let kill pre reg =
   let ms = Var.Set.of_ reg in

sledge/src/exec.mli

@@ -9,7 +9,7 @@
 
 open Fol
 
-val assume : Sh.t -> Formula.t -> Sh.t option
+val assume : Sh.t -> Formula.t -> Sh.t
 val kill : Sh.t -> Var.t -> Sh.t
 val move : Sh.t -> (Var.t * Term.t) iarray -> Sh.t
 val load : Sh.t -> reg:Var.t -> ptr:Term.t -> len:Term.t -> Sh.t option