[sledge] Change: Implement Fol using a solver-independent intermediate type

Summary:
In order to allow implementations of the single Fol interface using
multiple backend first-order logic solvers, add explicit definitions
of terms and formulas in the Fol module, and implement Context in
terms of them.

The Fol interface supports freely mixing Terms and Formulas, in
particular there is `Term.ite : cnd:Formula.t -> thn:Term.t ->
els:Term.t -> Term.t` which allows Formulas to appear in Terms. The
Fol implementation performs enough normalization to enable using an
internal representation of terms that is strictly partitioned into
"theory terms" and "formulas", which are stratified below "conditional
terms" and then below "general terms". This partitioning and
stratification enables using backend solvers that do not support
mixing formulas in terms.

Reviewed By: jvillard

Differential Revision: D22170506

fbshipit-source-id: a014ee7d7

infer/src/pulse/Pudge_intf.ml

@@ -16,39 +16,43 @@ module type S = sig
 
   val true_ : t
 
-  module Term : sig
+  module Var : sig
     type t
 
-    val zero : t
+    val of_absval : AbstractValue.t -> t
 
-    val le : t -> t -> t
+    val to_absval : t -> AbstractValue.t
+    (** use with caution: will crash the program if the given variable wasn't generated from an
+        [AbstractValue.t] using [Var.of_absval] *)
+  end
 
-    val lt : t -> t -> t
+  module Term : sig
+    type t
 
-    val not_ : t -> t
+    val zero : t
 
     val of_intlit : IntLit.t -> t
 
     val of_absval : AbstractValue.t -> t
 
-    val of_unop : Unop.t -> t -> t
+    val of_unop : Unop.t -> t -> t option
 
-    val of_binop : Binop.t -> t -> t -> t
+    val of_binop : Binop.t -> t -> t -> t option
   end
 
-  module Var : sig
+  module Formula : sig
     type t
 
-    val of_absval : AbstractValue.t -> t
+    val eq : Term.t -> Term.t -> t
 
-    val to_absval : t -> AbstractValue.t
-    (** use with caution: will crash the program if the given variable wasn't generated from an
-        [AbstractValue.t] using [Var.of_absval] *)
-  end
+    val lt : Term.t -> Term.t -> t
 
-  val and_eq : Term.t -> Term.t -> t -> t
+    val not_ : t -> t
+
+    val term_binop : Binop.t -> Term.t -> Term.t -> t option
+  end
 
-  val and_term : Term.t -> t -> t
+  val and_formula : Formula.t -> t -> t
 
   val and_ : t -> t -> t
 

infer/src/pulse/PulseDummySledge.ml

@@ -21,19 +21,25 @@ module Term = struct
 
   let zero = ()
 
-  let le () () = ()
+  let of_intlit _ = ()
 
-  let lt () () = ()
+  let of_absval _ = ()
 
-  let not_ () = ()
+  let of_unop _ () = None
 
-  let of_intlit _ = ()
+  let of_binop _ () () = None
+end
 
-  let of_absval _ = ()
+module Formula = struct
+  type t = unit
+
+  let eq () () = ()
+
+  let lt () () = ()
 
-  let of_unop _ () = ()
+  let not_ () = ()
 
-  let of_binop _ () () = ()
+  let term_binop _ () () = None
 end
 
 (* same type as {!PulsePathCondition.t} to be nice to summary serialization *)
@@ -46,9 +52,7 @@ let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
 
 let true_ = {eqs= Lazy.from_val Ses.Equality.true_; non_eqs= Lazy.from_val Ses.Term.true_}
 
-let and_eq () () phi = phi
-
-let and_term () phi = phi
+let and_formula () phi = phi
 
 let and_ phi1 _ = phi1
 

infer/src/pulse/PulsePathCondition.ml

@@ -51,7 +51,7 @@ let and_nonnegative v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.nat bo_itvs
     ; citvs= CItvs.add v CItv.zero_inf citvs
-    ; pudge= Pudge.and_term Pudge.Term.(le zero (of_absval v)) pudge }
+    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
 
 
 let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -60,7 +60,7 @@ let and_positive v ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v Itv.ItvPure.pos bo_itvs
     ; citvs= CItvs.add v (CItv.ge_to IntLit.one) citvs
-    ; pudge= Pudge.and_term Pudge.Term.(lt zero (of_absval v)) pudge }
+    ; pudge= Pudge.(and_formula (Formula.lt Term.zero (Term.of_absval v)) pudge) }
 
 
 let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -69,7 +69,7 @@ let and_eq_int v i ({satisfiable; bo_itvs; citvs; pudge} as phi) =
     { satisfiable
     ; bo_itvs= BoItvs.add v (Itv.ItvPure.of_int_lit i) bo_itvs
     ; citvs= CItvs.add v (CItv.equal_to i) citvs
-    ; pudge= Pudge.and_eq (Pudge.Term.of_absval v) (Pudge.Term.of_intlit i) pudge }
+    ; pudge= Pudge.(and_formula (Formula.eq (Term.of_absval v) (Term.of_intlit i)) pudge) }
 
 
 let simplify ~keep {satisfiable; bo_itvs; citvs; pudge} =
@@ -182,8 +182,9 @@ let and_pudge_callee subst pudge_caller pudge_callee =
         let subst', v_caller = subst_find_or_new subst v_callee in
         (subst', Pudge.Var.of_absval v_caller) )
   in
-  (* Don't trigger the computation of [path_condition] by asking for satisfiability here. Instead,
-     pudge (un-)satisfiability is computed lazily when we discover issues. *)
+  (* Don't trigger the computation of the underlying Sledge data structure by asking for
+     satisfiability here. Instead, pudge (un-)satisfiability is computed lazily when we discover
+     issues. *)
   (subst, Pudge.and_ pudge_caller pudge_callee_translated)
 
 
@@ -240,16 +241,19 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs bo_itvs =
   BoItvs.add binop_addr bo_itv bo_itvs
 
 
-let eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge =
+let eval_pudge_binop binop_addr binop op_lhs op_rhs pudge =
+  let open Pudge in
   let term_of_op = function
     | LiteralOperand i ->
-        Pudge.Term.of_intlit i
+        Term.of_intlit i
     | AbstractValueOperand v ->
-        Pudge.Term.of_absval v
+        Term.of_absval v
   in
-  Pudge.and_eq (Pudge.Term.of_absval binop_addr)
-    (Pudge.Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs))
-    pudge
+  match Term.of_binop binop (term_of_op op_lhs) (term_of_op op_rhs) with
+  | None ->
+      pudge
+  | Some t_binop ->
+      and_formula (Formula.eq (Term.of_absval binop_addr) t_binop) pudge
 
 
 let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -258,7 +262,7 @@ let eval_binop binop_addr binop op_lhs op_rhs ({satisfiable; bo_itvs; citvs; pud
     { satisfiable
     ; bo_itvs= eval_bo_itv_binop binop_addr binop op_lhs op_rhs bo_itvs
     ; citvs= eval_citv_binop binop_addr binop op_lhs op_rhs citvs
-    ; pudge= eval_path_condition_binop binop_addr binop op_lhs op_rhs pudge }
+    ; pudge= eval_pudge_binop binop_addr binop op_lhs op_rhs pudge }
 
 
 let eval_citv_unop unop_addr unop operand_addr citvs =
@@ -278,8 +282,13 @@ let eval_bo_itv_unop unop_addr unop operand_addr bo_itvs =
       BoItvs.add unop_addr itv bo_itvs
 
 
-let eval_path_condition_unop unop_addr unop addr pudge =
-  Pudge.and_eq (Pudge.Term.of_absval unop_addr) Pudge.Term.(of_unop unop (of_absval addr)) pudge
+let eval_pudge_unop unop_addr (unop : Unop.t) addr pudge =
+  let open Pudge in
+  match Term.of_unop unop (Term.of_absval addr) with
+  | None ->
+      pudge
+  | Some t_unop ->
+      and_formula (Formula.eq (Term.of_absval unop_addr) t_unop) pudge
 
 
 let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi) =
@@ -288,7 +297,7 @@ let eval_unop unop_addr unop addr ({satisfiable; bo_itvs; citvs; pudge} as phi)
     { satisfiable
     ; bo_itvs= eval_bo_itv_unop unop_addr unop addr bo_itvs
     ; citvs= eval_citv_unop unop_addr unop addr citvs
-    ; pudge= eval_path_condition_unop unop_addr unop addr pudge }
+    ; pudge= eval_pudge_unop unop_addr unop addr pudge }
 
 
 let prune_bo_with_bop ~negated v_opt arith bop arith' phi =
@@ -328,15 +337,18 @@ let bind_satisfiable phi ~f = if phi.satisfiable then f phi else phi
 let prune_binop ~negated bop lhs_op rhs_op ({satisfiable; bo_itvs= _; citvs; pudge} as phi) =
   if not satisfiable then phi
   else
-    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, path_cond_lhs = eval_operand phi lhs_op in
-    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, path_cond_rhs = eval_operand phi rhs_op in
+    let value_lhs_opt, arith_lhs_opt, bo_itv_lhs, pudge_lhs = eval_operand phi lhs_op in
+    let value_rhs_opt, arith_rhs_opt, bo_itv_rhs, pudge_rhs = eval_operand phi rhs_op in
     let phi =
-      let pudge =
-        let t_positive = Pudge.Term.of_binop bop path_cond_lhs path_cond_rhs in
-        let t = if negated then Pudge.Term.not_ t_positive else t_positive in
-        Pudge.and_term t pudge
-      in
-      {phi with pudge}
+      match Pudge.Formula.term_binop bop pudge_lhs pudge_rhs with
+      | None ->
+          phi
+      | Some f_positive ->
+          let pudge =
+            let f = if negated then Pudge.Formula.not_ f_positive else f_positive in
+            Pudge.and_formula f pudge
+          in
+          {phi with pudge}
     in
     match CItv.abduce_binop_is_true ~negated bop arith_lhs_opt arith_rhs_opt with
     | Unsatisfiable ->

infer/src/pulse/PulseSledge.ml

@@ -6,14 +6,13 @@
  *)
 
 open! IStd
-module F = Format
 module L = Logging
 module AbstractValue = PulseAbstractValue
 
 [@@@warning "+9"]
 
 module Var = struct
-  module Var = Ses.Var
+  module Var = Sledge.Fol.Var
 
   let of_absval (v : AbstractValue.t) = Var.identified ~name:"v" ~id:(v :> int)
 
@@ -26,153 +25,133 @@ module Var = struct
 end
 
 module Term = struct
-  module Term = Ses.Term
+  module Term = Sledge.Fol.Term
 
   let of_intlit i = Term.integer (IntLit.to_big_int i)
 
   let of_absval v = Term.var (Var.of_absval v)
 
-  let of_unop (unop : Unop.t) t = match unop with Neg -> Term.neg t | BNot | LNot -> Term.not_ t
+  let of_unop (unop : Unop.t) t = match unop with Neg -> Some (Term.neg t) | BNot | LNot -> None
 
   let of_binop (binop : Binop.t) t1 t2 =
     let open Term in
     match binop with
     | PlusA _ | PlusPI ->
-        add t1 t2
+        Some (add t1 t2)
     | MinusA _ | MinusPI | MinusPP ->
-        sub t1 t2
+        Some (sub t1 t2)
     | Mult _ ->
-        mul t1 t2
-    | Div ->
-        div t1 t2
-    | Mod ->
-        rem t1 t2
-    | Shiftlt ->
-        shl t1 t2
+        Some (mul t1 t2)
+    | Div | Mod | Shiftlt | Shiftrt | Lt | Gt | Le | Ge | Eq | Ne | BAnd | LAnd | BOr | LOr | BXor
+      ->
+        None
+
+
+  include Term
+end
+
+module Formula = struct
+  module Formula = Sledge.Fol.Formula
+
+  let term_binop (binop : Binop.t) t1 t2 =
+    match binop with
+    | BAnd
+    | BOr
+    | BXor
+    | PlusA _
+    | PlusPI
+    | MinusA _
+    | MinusPI
+    | MinusPP
+    | Mult _
+    | Div
+    | Mod
+    | Shiftlt
     | Shiftrt ->
-        lshr t1 t2
+        Term.of_binop binop t1 t2 |> Option.map ~f:(fun t -> Formula.dq t Term.zero)
     | Lt ->
-        lt t1 t2
+        Some (Formula.lt t1 t2)
     | Gt ->
-        lt t2 t1
+        Some (Formula.lt t2 t1)
     | Le ->
-        le t1 t2
+        Some (Formula.le t1 t2)
     | Ge ->
-        le t2 t1
+        Some (Formula.le t2 t1)
     | Eq ->
-        eq t1 t2
+        Some (Formula.eq t1 t2)
     | Ne ->
-        dq t1 t2
-    | BAnd | LAnd ->
-        and_ t1 t2
-    | BOr | LOr ->
-        or_ t1 t2
-    | BXor ->
-        xor t1 t2
+        Some (Formula.dq t1 t2)
+    | LAnd ->
+        Option.both (Formula.project t1) (Formula.project t2)
+        |> Option.map ~f:(fun (f1, f2) -> Formula.and_ f1 f2)
+    | LOr ->
+        Option.both (Formula.project t1) (Formula.project t2)
+        |> Option.map ~f:(fun (f1, f2) -> Formula.or_ f1 f2)
 
 
-  include Term
+  include Formula
 end
 
-module Equality = struct
-  include Ses.Equality
+module Context = struct
+  include Sledge.Fol.Context
 
   let assert_no_new_vars api new_vars =
     if not (Var.Set.is_empty new_vars) then
       L.die InternalError "Huho, %s generated fresh new variables %a" api Var.Set.pp new_vars
 
 
-  let and_eq t1 t2 r =
-    let new_vars, r' = Ses.Equality.and_eq Var.Set.empty t1 t2 r in
-    assert_no_new_vars "Equality.and_eq" new_vars ;
-    r'
-
-
-  let and_term t r =
-    let new_vars, r' = Ses.Equality.and_term Var.Set.empty t r in
-    assert_no_new_vars "Equality.and_term" new_vars ;
+  let and_formula phi r =
+    let new_vars, r' = Sledge.Fol.Context.and_formula Var.Set.empty phi r in
+    assert_no_new_vars "Context.and_formula" new_vars ;
     r'
 
 
   let and_ r1 r2 =
-    let new_vars, r' = Ses.Equality.and_ Var.Set.empty r1 r2 in
-    assert_no_new_vars "Equality.and_" new_vars ;
+    let new_vars, r' = Sledge.Fol.Context.and_ Var.Set.empty r1 r2 in
+    assert_no_new_vars "Context.and_" new_vars ;
     r'
 
 
   let apply_subst subst r =
-    let new_vars, r' = Ses.Equality.apply_subst Var.Set.empty subst r in
-    assert_no_new_vars "Equality.apply_subst" new_vars ;
+    let new_vars, r' = Sledge.Fol.Context.apply_subst Var.Set.empty subst r in
+    assert_no_new_vars "Context.apply_subst" new_vars ;
     r'
 end
 
-(** We distinguish between what the equality relation of sledge can express and the "non-equalities"
-    terms that this relation ignores. We keep the latter around for completeness: we can still
-    substitute known equalities into these and sometimes get contradictions back. *)
-type t = {eqs: Equality.t lazy_t; non_eqs: Term.t lazy_t}
-
-let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs
-
-
-let true_ = {eqs= Lazy.from_val Equality.true_; non_eqs= Lazy.from_val Term.true_}
+type t = Context.t lazy_t
 
-let and_eq t1 t2 phi = {phi with eqs= lazy (Equality.and_eq t1 t2 (Lazy.force phi.eqs))}
+let pp fmt (lazy phi) = Context.pp fmt phi
 
-let and_term (t : Term.t) phi =
-  (* add the term to the relation *)
-  let eqs = lazy (Equality.and_term t (Lazy.force phi.eqs)) in
-  (* [t] normalizes to [true_] so [non_eqs] never changes, do this regardless for now *)
-  let non_eqs = lazy (Term.and_ (Lazy.force phi.non_eqs) (Equality.normalize (Lazy.force eqs) t)) in
-  {eqs; non_eqs}
+let true_ = Lazy.from_val Context.true_
 
+let and_formula f phi = lazy (Context.and_formula f (Lazy.force phi))
 
-let and_ phi1 phi2 =
-  { eqs= lazy (Equality.and_ (Lazy.force phi1.eqs) (Lazy.force phi2.eqs))
-  ; non_eqs= lazy (Term.and_ (Lazy.force phi1.non_eqs) (Lazy.force phi2.non_eqs)) }
+let and_ phi1 phi2 = lazy (Context.and_ (Lazy.force phi1) (Lazy.force phi2))
 
+let is_known_zero t phi = Context.entails_eq (Lazy.force phi) t Term.zero
 
-let is_known_zero t phi = Equality.entails_eq (Lazy.force phi.eqs) t Term.zero
-
-(* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *)
-let is_unsat {eqs; non_eqs} =
-  (* [Term.is_false] is cheap, forcing [eqs] is expensive, then calling [Equality.normalize] is
-     expensive on top of that *)
-  Term.is_false (Lazy.force non_eqs)
-  || Equality.is_false (Lazy.force eqs)
-  || Term.is_false (Equality.normalize (Lazy.force eqs) (Lazy.force non_eqs))
-
-
-let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} =
-  Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs)
+let is_unsat phi = Context.is_false (Lazy.force phi)
 
+let fv (lazy phi) = Context.fv phi
 
 let fold_map_variables phi ~init ~f =
-  let term_fold_map t ~init ~f =
-    Term.fold_map_rec_pre t ~init ~f:(fun acc t ->
-        Var.of_term t
-        |> Option.map ~f:(fun v ->
-               let acc', v' = f acc v in
-               (acc', Term.var v') ) )
-  in
-  let acc, eqs' =
-    Equality.classes (Lazy.force phi.eqs)
-    |> Term.Map.fold ~init:(init, Equality.true_) ~f:(fun ~key:t ~data:equal_ts (acc, eqs') ->
-           let acc, t' = term_fold_map ~init:acc ~f t in
-           List.fold equal_ts ~init:(acc, eqs') ~f:(fun (acc, eqs') equal_t ->
-               let acc, t_mapped = term_fold_map ~init:acc ~f equal_t in
-               (acc, Equality.and_eq t' t_mapped eqs') ) )
+  let acc, phi' =
+    Context.classes (Lazy.force phi)
+    |> Term.Map.fold ~init:(init, Context.true_) ~f:(fun ~key:t ~data:equal_ts (acc, phi') ->
+           let acc, t' = Term.fold_map_vars ~init:acc ~f t in
+           List.fold equal_ts ~init:(acc, phi') ~f:(fun (acc, phi') equal_t ->
+               let acc, t_mapped = Term.fold_map_vars ~init:acc ~f equal_t in
+               (acc, Context.and_formula (Formula.eq t' t_mapped) phi') ) )
   in
-  let acc, non_eqs' = term_fold_map ~init:acc ~f (Lazy.force phi.non_eqs) in
-  (acc, {eqs= Lazy.from_val eqs'; non_eqs= Lazy.from_val non_eqs'})
+  (acc, Lazy.from_val phi')
 
 
 let simplify ~keep phi =
   let all_vs = fv phi in
   let keep_vs =
     AbstractValue.Set.fold
-      (fun v keep_vs -> Term.Var.Set.add keep_vs (Var.of_absval v))
-      keep Term.Var.Set.empty
+      (fun v keep_vs -> Var.Set.add keep_vs (Var.of_absval v))
+      keep Var.Set.empty
   in
-  let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] (Lazy.force phi.eqs) in
-  {phi with eqs= Lazy.from_val (Equality.apply_subst simpl_subst (Lazy.force phi.eqs))}
+  let simpl_subst = Context.solve_for_vars [keep_vs; all_vs] (Lazy.force phi) in
+  Lazy.from_val (Context.apply_subst simpl_subst (Lazy.force phi))

sledge/src/fol.mli

@@ -10,6 +10,7 @@ module Var : sig
   type t [@@deriving compare, equal, sexp]
   type strength = t -> [`Universal | `Existential | `Anonymous] option
 
+  val ppx : strength -> t pp
   val pp : t pp
 
   module Map : Map.S with type key := t
@@ -98,17 +99,22 @@ module rec Term : sig
 
   val const_of : t -> Q.t option
 
-  (** Transform *)
+  (** Query *)
 
-  val rename : Var.Subst.t -> t -> t
+  val fv : t -> Var.Set.t
 
   (** Traverse *)
 
-  val fold_vars : t -> init:'a -> f:('a -> Var.t -> 'a) -> 'a
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
 
-  (** Query *)
+  (** Transform *)
 
-  val fv : t -> Var.Set.t
+  val map_vars : f:(Var.t -> Var.t) -> t -> t
+
+  val fold_map_vars :
+    t -> init:'a -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
+
+  val rename : Var.Subst.t -> t -> t
 end
 
 (** Formulas *)
@@ -140,16 +146,25 @@ and Formula : sig
   val or_ : t -> t -> t
   val cond : cnd:t -> pos:t -> neg:t -> t
 
-  (** Transform *)
-
-  val rename : Var.Subst.t -> t -> t
-  val disjuncts : t -> t list
-
   (** Query *)
 
+  val fv : t -> Var.Set.t
   val is_true : t -> bool
   val is_false : t -> bool
-  val fv : t -> Var.Set.t
+
+  (** Traverse *)
+
+  val fold_vars : init:'a -> t -> f:('a -> Var.t -> 'a) -> 'a
+
+  (** Transform *)
+
+  val map_vars : f:(Var.t -> Var.t) -> t -> t
+
+  val fold_map_vars :
+    init:'a -> t -> f:('a -> Var.t -> 'a * Var.t) -> 'a * t
+
+  val rename : Var.Subst.t -> t -> t
+  val disjuncts : t -> t list
 end
 
 (** Inference System *)
@@ -214,7 +229,7 @@ module Context : sig
       implies [a = b+k], or [None] if [a] and [b] are not equal up to an
       integer offset. *)
 
-  val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
+  val fold_terms : init:'a -> t -> f:('a -> Term.t -> 'a) -> 'a
 
   (** Solution Substitutions *)
   module Subst : sig

sledge/src/ses/term.ml

@@ -1040,6 +1040,8 @@ module Var = struct
     | Some v -> v
     | _ -> violates Llair.Reg.invariant r
 
+  let program ~name ~global = Var {name; id= (if global then -1 else 0)}
+
   let fresh name ~wrt =
     let max = match Set.max_elt wrt with None -> 0 | Some max -> id max in
     let x' = Var {name; id= max + 1} in

sledge/src/ses/term.mli

@@ -128,6 +128,7 @@ module Var : sig
   val of_ : term -> t
   val of_term : term -> t option
   val of_reg : Llair.Reg.t -> t
+  val program : name:string -> global:bool -> t
   val fresh : string -> wrt:Set.t -> t * Set.t
 
   val identified : name:string -> id:int -> t

sledge/src/sh_test.ml

@@ -83,9 +83,9 @@ let%test_module _ =
           ( (  0 = %x_6 ∧ emp)
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
-
+    
         ( (∃ %x_6, %x_7 .   2 = %x_7 ∧ (%x_7 = 2) ∧ emp)
-        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) && (%y_7 = 1)) ∧ emp)
+        ∨ (∃ %x_6 .   1 = %x_6 = %y_7 ∧ ((%x_6 = 1) ∧ (%y_7 = 1)) ∧ emp)
         ∨ (  0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
 
@@ -108,11 +108,11 @@ let%test_module _ =
           ( (  0 = _ ∧ emp)
           ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
           )
-
+    
         ( (∃ %x_6, %x_8, %x_9 .   2 = %x_9 ∧ (%x_9 = 2) ∧ emp)
         ∨ (∃ %x_6, %x_8 .
              1 = %y_7 = %x_8
-           ∧ ((%y_7 = 1) && (%x_8 = 1))
+           ∧ ((%x_8 = 1) ∧ (%y_7 = 1))
            ∧ emp)
         ∨ (∃ %x_6 .   0 = %x_6 ∧ (%x_6 = 0) ∧ emp)
         ) |}]
@@ -136,7 +136,7 @@ let%test_module _ =
         ( (  0 = _ ∧ emp)
         ∨ (  ( (  1 = _ = %y_7 ∧ emp) ∨ (  2 = _ ∧ emp) ))
         )
-
+    
         ( (  1 = %y_7 ∧ emp) ∨ (  emp) ∨ (  emp) ) |}]
 
     let%expect_test _ =
@@ -148,9 +148,9 @@ let%test_module _ =
       [%expect
         {|
         ∃ %x_6 .   %x_6 = %x_6^ ∧ (%y_7 + -1) = %y_7^ ∧ emp
-
-          (%y_7 + -1) = %y_7^ ∧ (%y_7^ = (%y_7 + -1)) ∧ emp
-
+    
+          (%y_7 + -1) = %y_7^ ∧ (%y_7^ = ((-1 × 1) + (1 × %y_7))) ∧ emp
+    
           (%y_7 + -1) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
@@ -173,7 +173,7 @@ let%test_module _ =
         {|
         ∃ %a_1, %c_3, %d_4, %e_5 .
           (⟨8,%a_1⟩^⟨8,%d_4⟩) = %e_5
-        ∧ (⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩))
+        ∧ ((⟨16,%e_5⟩ = (⟨8,%a_1⟩^⟨8,%d_4⟩)) ∧ tt)
         ∧ emp
         * ( (  (%x_6 ≠ 0) ∧ emp)
           ∨ (∃ %b_2 .
@@ -182,7 +182,7 @@ let%test_module _ =
              ∧ emp)
           )
 
-          -1 ∧ emp * ( (  -1 ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
+          tt ∧ emp * ( (  tt ∧ emp) ∨ (  (%x_6 ≠ 0) ∧ emp) )
 
           ( (  emp) ∨ (  (%x_6 ≠ 0) ∧ emp) ) |}]
   end )

sledge/src/solver_test.ml

@@ -196,7 +196,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let%expect_test _ =
       infer_frame
@@ -218,7 +218,7 @@ let%test_module _ =
             %a_2 = %a0_10
           ∧ (⟨16,%a_2⟩^⟨16,%a1_11⟩) = %a_1
           ∧ 16 = %m_8 = %n_9
-          ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
+          ∧ ((16 × 1) + (1 × %k_5)) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]
 
     let seg_split_symbolically =
       Sh.star
@@ -236,7 +236,7 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩
+            %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
           * ( (  2 = %n_9 ∧ emp)
             ∨ (  0 = %n_9 ∧ emp)
             ∨ (  1 = %n_9 ∧ emp)
@@ -247,7 +247,7 @@ let%test_module _ =
             ( (  %a_1 = %a_2
                ∧ 2 = %n_9
                ∧ 16 = %m_8
-               ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
+               ∧ ((16 × 1) + (1 × %l_6)) -[ %l_6, 16 )-> ⟨0,%a_3⟩)
             ∨ (  %a_3 = _
                ∧ (⟨8,%a_2⟩^⟨8,%a_3⟩) = %a_1
                ∧ 1 = %n_9
@@ -269,8 +269,8 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%n_9 ≤ 2)
-          ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(-8 × %n_9 + 16),%a_3⟩
+            ((%n_9 ≤ 2) ∧ (tt ∧ tt))
+          ∧ %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 - (8 × %n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
         ) infer_frame: |}]