[sledge] Represent arithmetic terms using polynomials

Summary:
Change the representation of Fol terms to use polynomials for
arithmetic. This is a generalization and simplification of those used
in Ses. In particular, the treatment of division is stronger as it
captures associativity, commutativity, and unit laws, plus being the
inverse of multiplication.

Also, the interface is staged and factored so that the implementation
of polynomials and arithmetic is separate from the rest of terms.

Reviewed By: jvillard

Differential Revision: D24306108

fbshipit-source-id: 78589a8ec

sledge/nonstdlib/NS.ml

@@ -183,6 +183,14 @@ module Q = struct
 
   let of_z = Q.of_bigint
 
+  let pow q = function
+    | 1 -> q
+    | 0 -> Q.one
+    | -1 -> Q.inv q
+    | n ->
+        let q, n = if n < 0 then (Q.inv q, -n) else (q, n) in
+        Q.make (Z.pow (Q.num q) n) (Z.pow (Q.den q) n)
+
   include Q
 end
 

sledge/nonstdlib/NS.mli

@@ -147,6 +147,7 @@ module Q : sig
   val t_of_sexp : Sexp.t -> t
   val sexp_of_t : t -> Sexp.t
   val pp : t pp
+  val pow : t -> int -> t
 end
 
 module Z : sig

sledge/nonstdlib/map.ml

@@ -62,6 +62,7 @@ end) : S with type key = Key.t = struct
     M.union (fun key v1 v2 -> Some (combine ~key v1 v2)) x y
 
   let union x y ~f = M.union f x y
+  let partition m ~f = M.partition f m
   let is_empty = M.is_empty
 
   let root_key m =
@@ -110,6 +111,22 @@ end) : S with type key = Key.t = struct
   let find_exn m k = M.find k m
   let find m k = M.find_opt k m
 
+  let only_binding m =
+    match root_key m with
+    | Some k -> (
+      match M.split k m with
+      | l, Some v, r when is_empty l && is_empty r -> Some (k, v)
+      | _ -> None )
+    | None -> None
+
+  let classify m =
+    match root_key m with
+    | None -> `Zero
+    | Some k -> (
+      match M.split k m with
+      | l, Some v, r when is_empty l && is_empty r -> `One (k, v)
+      | _ -> `Many )
+
   let find_multi m k =
     match M.find_opt k m with None -> [] | Some vs -> vs
 

sledge/nonstdlib/map_intf.ml

@@ -53,12 +53,15 @@ module type S = sig
     'a t -> 'a t -> combine:(key:key -> 'a -> 'a -> 'a) -> 'a t
 
   val union : 'a t -> 'a t -> f:(key -> 'a -> 'a -> 'a option) -> 'a t
+  val partition : 'a t -> f:(key -> 'a -> bool) -> 'a t * 'a t
 
   (** {1 Query} *)
 
   val is_empty : 'a t -> bool
   val is_singleton : 'a t -> bool
   val length : 'a t -> int
+  val only_binding : 'a t -> (key * 'a) option
+  val classify : 'a t -> [`Zero | `One of key * 'a | `Many]
 
   val choose_key : 'a t -> key option
   (** Find an unspecified key. Different keys may be chosen for equivalent

sledge/nonstdlib/multiset.ml

@@ -46,8 +46,8 @@ struct
 
   let pp sep pp_elt fs s = List.pp sep pp_elt fs (M.to_alist s)
   let empty = M.empty
-  let of_ = M.singleton
-  let if_nz q = if Mul.equal Mul.zero q then None else Some q
+  let of_ x i = if Mul.equal Mul.zero i then empty else M.singleton x i
+  let if_nz i = if Mul.equal Mul.zero i then None else Some i
 
   let add m x i =
     M.change m x ~f:(function
@@ -58,6 +58,14 @@ struct
   let find_and_remove = M.find_and_remove
   let union m n = M.union m n ~f:(fun _ i j -> if_nz (Mul.add i j))
 
+  let diff m n =
+    M.merge m n ~f:(fun ~key:_ -> function
+      | `Both (i, j) -> if_nz (Mul.sub i j)
+      | `Left i -> Some i
+      | `Right j -> Some (Mul.neg j) )
+
+  let partition = M.partition
+
   let map m ~f =
     let m' = empty in
     let m, m' =
@@ -67,28 +75,40 @@ struct
             if Mul.equal i' i then (m, m') else (M.set m ~key:x ~data:i', m')
           else (M.remove m x, add m' x' i') )
     in
-    M.fold m' ~init:m ~f:(fun ~key:x ~data:i m -> add m x i)
+    union m m'
+
+  let map_counts m ~f = M.map ~f m
+  let mapi_counts m ~f = M.mapi ~f:(fun ~key ~data -> f key data) m
+
+  let flat_map m ~f =
+    let m' = empty in
+    let m, m' =
+      M.fold m ~init:(m, m') ~f:(fun ~key:x ~data:i (m, m') ->
+          let d = f x i in
+          match M.only_binding d with
+          | Some (x', i') ->
+              if x' == x then
+                if Mul.equal i' i then (m, m')
+                else (M.set m ~key:x ~data:i', m')
+              else (M.remove m x, union m' d)
+          | None -> (M.remove m x, union m' d) )
+    in
+    union m m'
 
-  let map_counts m ~f = M.mapi ~f:(fun ~key ~data -> f key data) m
   let is_empty = M.is_empty
   let is_singleton = M.is_singleton
   let length m = M.length m
   let count m x = match M.find m x with Some q -> q | None -> Mul.zero
+  let only_elt = M.only_binding
+  let classify = M.classify
   let choose = M.choose
   let choose_exn = M.choose_exn
   let pop = M.pop
   let min_elt = M.min_binding
   let pop_min_elt = M.pop_min_binding
-
-  let classify s =
-    match pop s with
-    | None -> `Zero
-    | Some (elt, q, s') when is_empty s' -> `One (elt, q)
-    | _ -> `Many
-
   let to_list m = M.to_alist m
   let iter m ~f = M.iteri ~f:(fun ~key ~data -> f key data) m
   let exists m ~f = M.existsi ~f:(fun ~key ~data -> f key data) m
   let for_all m ~f = M.for_alli ~f:(fun ~key ~data -> f key data) m
-  let fold m ~f ~init = M.fold ~f:(fun ~key ~data -> f key data) m ~init
+  let fold m ~init ~f = M.fold ~f:(fun ~key ~data -> f key data) m ~init
 end

sledge/nonstdlib/multiset_intf.ml

@@ -44,15 +44,28 @@ module type S = sig
   (** Set the multiplicity of an element to zero. [O(log n)] *)
 
   val union : t -> t -> t
-  (** Sum multiplicities pointwise. [O(n + m)] *)
+  (** Add multiplicities pointwise. [O(n + m)] *)
+
+  val diff : t -> t -> t
+  (** Subtract multiplicities pointwise. [O(n + m)] *)
 
   val map : t -> f:(elt -> mul -> elt * mul) -> t
   (** Map over the elements in ascending order. Preserves physical equality
       if [f] does. *)
 
-  val map_counts : t -> f:(elt -> mul -> mul) -> t
+  val map_counts : t -> f:(mul -> mul) -> t
+  (** Map over the multiplicities of the elements in ascending order. *)
+
+  val mapi_counts : t -> f:(elt -> mul -> mul) -> t
   (** Map over the multiplicities of the elements in ascending order. *)
 
+  val flat_map : t -> f:(elt -> mul -> t) -> t
+  (** Flat map over the elements in ascending order. Preserves physical
+      equality if [f e m] is a singleton [(e', m')] with [e == e'] and
+      [Mul.equal m m'] for all elements. *)
+
+  val partition : t -> f:(elt -> mul -> bool) -> t * t
+
   (* queries *)
 
   val is_empty : t -> bool
@@ -64,6 +77,9 @@ module type S = sig
   val count : t -> elt -> mul
   (** Multiplicity of an element. [O(log n)]. *)
 
+  val only_elt : t -> (elt * mul) option
+  (** The only element of a singleton multiset. [O(1)]. *)
+
   val choose_exn : t -> elt * mul
   (** Find an unspecified element. [O(1)]. *)
 
@@ -99,6 +115,6 @@ module type S = sig
   val for_all : t -> f:(elt -> mul -> bool) -> bool
   (** Test whether all elements satisfy a predicate. *)
 
-  val fold : t -> f:(elt -> mul -> 's -> 's) -> init:'s -> 's
+  val fold : t -> init:'s -> f:(elt -> mul -> 's -> 's) -> 's
   (** Fold over the elements in ascending order. *)
 end

sledge/src/arithmetic.ml

@@ -0,0 +1,268 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Arithmetic terms *)
+
+include Arithmetic_intf
+
+module Representation (Trm : INDETERMINATE) = struct
+  module Prod = struct
+    include Multiset.Make
+              (Int)
+              (struct
+                type t = Trm.trm [@@deriving compare, equal, sexp]
+              end)
+
+    let t_of_sexp = t_of_sexp Trm.trm_of_sexp
+  end
+
+  module Mono = struct
+    type t = Prod.t [@@deriving compare, equal, sexp]
+
+    let num_den m = Prod.partition m ~f:(fun _ i -> i >= 0)
+
+    let ppx strength ppf power_product =
+      let pp_factor ppf (indet, exponent) =
+        if exponent = 1 then (Trm.ppx strength) ppf indet
+        else Format.fprintf ppf "%a^%i" (Trm.ppx strength) indet exponent
+      in
+      let pp_num ppf num =
+        if Prod.is_empty num then Trace.pp_styled `Magenta "1" ppf
+        else Prod.pp "@ @<2>× " pp_factor ppf num
+      in
+      let pp_den ppf den =
+        if not (Prod.is_empty den) then
+          Format.fprintf ppf "@ / %a"
+            (Prod.pp "@ / " pp_factor)
+            (Prod.map_counts ~f:Int.neg den)
+      in
+      let num, den = num_den power_product in
+      Format.fprintf ppf "@[<2>(%a%a)@]" pp_num num pp_den den
+
+    (** [one] is the empty product Πᵢ₌₁⁰ xᵢ^pᵢ *)
+    let one = Prod.empty
+
+    let equal_one = Prod.is_empty
+
+    (** [of_ x₁ p₁] is the singleton product Πᵢ₌₁¹ x₁^p₁ *)
+    let of_ x p = Prod.of_ x p
+
+    (** [pow (Πᵢ₌₁ⁿ xᵢ^pᵢ) p] is Πᵢ₌₁ⁿ xᵢ^(pᵢ×p) *)
+    let pow mono = function
+      | 0 -> Prod.empty
+      | 1 -> mono
+      | power -> Prod.map_counts ~f:(Int.mul power) mono
+
+    let mul x y = Prod.union x y
+
+    (** [get_trm m] is [Some x] iff [equal m (of_ x 1)] *)
+    let get_trm mono =
+      match Prod.only_elt mono with Some (trm, 1) -> Some trm | _ -> None
+  end
+
+  module Sum = struct
+    include Multiset.Make (Q) (Mono)
+
+    let t_of_sexp = t_of_sexp Mono.t_of_sexp
+  end
+
+  module Poly = struct
+    type t = Sum.t [@@deriving compare, equal, sexp]
+    type trm = Trm.trm
+  end
+
+  include Poly
+
+  module Make (Embed : EMBEDDING with type trm := Trm.trm and type t := t) =
+  struct
+    include Poly
+
+    let ppx strength ppf poly =
+      if Sum.is_empty poly then Trace.pp_styled `Magenta "0" ppf
+      else
+        let pp_coeff_mono ppf (m, c) =
+          if Mono.equal_one m then Trace.pp_styled `Magenta "%a" ppf Q.pp c
+          else
+            Format.fprintf ppf "%a @<2>× %a" Q.pp c (Mono.ppx strength) m
+        in
+        Format.fprintf ppf "@[<2>(%a)@]" (Sum.pp "@ + " pp_coeff_mono) poly
+
+    let mono_invariant mono =
+      let@ () = Invariant.invariant [%here] mono [%sexp_of: Mono.t] in
+      Prod.iter mono ~f:(fun base power ->
+          (* powers are non-zero *)
+          assert (not (Int.equal Int.zero power)) ;
+          match Embed.get_arith base with
+          | None -> ()
+          | Some poly -> (
+            match Sum.classify poly with
+            | `Many -> ()
+            | `Zero | `One _ ->
+                (* polynomial factors are not constant or singleton, which
+                   should have been flattened into the parent monomial *)
+                assert false ) ) ;
+      match Mono.get_trm mono with
+      | None -> ()
+      | Some trm -> (
+        match Embed.get_arith trm with
+        | None -> ()
+        | Some _ ->
+            (* singleton monomials are not polynomials, which should have
+               been flattened into the parent polynomial *)
+            assert false )
+
+    let invariant poly =
+      let@ () = Invariant.invariant [%here] poly [%sexp_of: t] in
+      Sum.iter poly ~f:(fun mono coeff ->
+          (* coefficients are non-zero *)
+          assert (not (Q.equal Q.zero coeff)) ;
+          mono_invariant mono )
+
+    (* constants *)
+
+    let const q = Sum.of_ Mono.one q |> check invariant
+    let zero = const Q.zero |> check (fun p -> assert (Sum.is_empty p))
+
+    (* core constructors *)
+
+    let neg poly = Sum.map_counts ~f:Q.neg poly |> check invariant
+    let add p q = Sum.union p q |> check invariant
+    let sub p q = add p (neg q)
+
+    let mulc coeff poly =
+      ( if Q.equal Q.one coeff then poly
+      else if Q.equal Q.zero coeff then zero
+      else Sum.map_counts ~f:(Q.mul coeff) poly )
+      |> check invariant
+
+    (* projections and embeddings *)
+
+    type view = Trm of trm | Const of Q.t | Compound
+
+    let classify poly =
+      match Sum.classify poly with
+      | `Zero -> Const Q.zero
+      | `One (mono, coeff) -> (
+        match Prod.classify mono with
+        | `Zero -> Const coeff
+        | `One (trm, 1) when Q.equal Q.one coeff -> Trm trm
+        | _ -> Compound )
+      | `Many -> Compound
+
+    let get_const poly =
+      match Sum.classify poly with
+      | `Zero -> Some Q.zero
+      | `One (mono, coeff) when Mono.equal_one mono -> Some coeff
+      | _ -> None
+
+    let get_mono poly =
+      match Sum.only_elt poly with
+      | Some (mono, coeff) when Q.equal Q.one coeff -> Some mono
+      | _ -> None
+
+    (** Terms of a polynomial: product of a coefficient and a monomial *)
+    module CM = struct
+      type t = Q.t * Prod.t
+
+      let one = (Q.one, Mono.one)
+      let equal_one (c, m) = Mono.equal_one m && Q.equal Q.one c
+      let mul (c1, m1) (c2, m2) = (Q.mul c1 c2, Mono.mul m1 m2)
+
+      (** Monomials [Mono.t] have [trm] indeterminates, which include, via
+          [get_arith], polynomials [t] over monomials themselves. To avoid
+          redundant representations, singleton polynomials are flattened. *)
+      let of_trm : ?power:int -> trm -> t =
+       fun ?(power = 1) base ->
+        match Embed.get_arith base with
+        | Some poly -> (
+          match Sum.classify poly with
+          (* 0 ^ p₁ ==> 0 × 1 *)
+          | `Zero -> (Q.zero, Mono.one)
+          (* (Σᵢ₌₁¹ cᵢ × Xᵢ) ^ p₁ ==> cᵢ^p₁ × Πⱼ₌₁¹ Xⱼ^pⱼ *)
+          | `One (mono, coeff) -> (Q.pow coeff power, Mono.pow mono power)
+          (* (Σᵢ₌₁ⁿ cᵢ × Xᵢ) ^ p₁ ==> 1 × Πⱼ₌₁¹ (Σᵢ₌₁ⁿ cᵢ × Xᵢ)^pⱼ *)
+          | `Many -> (Q.one, Mono.of_ base power) )
+        (* X₁ ^ p₁ ==> 1 × Πⱼ₌₁¹ Xⱼ^pⱼ *)
+        | None -> (Q.one, Mono.of_ base power)
+
+      (** Polynomials [t] have [trm] indeterminates, which, via [get_arith],
+          include polynomials themselves. To avoid redundant
+          representations, singleton monomials are flattened. Also, constant
+          multiplication is not interpreted in [Prod], so constant
+          polynomials are multiplied by their coefficients directly. *)
+      let to_poly : t -> Poly.t =
+       fun (coeff, mono) ->
+        ( match Mono.get_trm mono with
+        | Some trm -> (
+          match Embed.get_arith trm with
+          (* c × (Σᵢ₌₁ⁿ cᵢ × Xᵢ) ==> Σᵢ₌₁ⁿ c×cᵢ × Xᵢ *)
+          | Some poly -> mulc coeff poly
+          (* c₁ × X₁ ==> Σᵢ₌₁¹ cᵢ × Xᵢ *)
+          | None -> Sum.of_ mono coeff )
+        (* c₁ × (Πⱼ₌₁ᵐ X₁ⱼ^p₁ⱼ) ==> Σᵢ₌₁¹ cᵢ × (Πⱼ₌₁ᵐ Xᵢⱼ^pᵢⱼ) *)
+        | None -> Sum.of_ mono coeff )
+        |> check invariant
+    end
+
+    (** Embed a term into a polynomial, by projecting a polynomial out of
+        the term if possible *)
+    let trm trm =
+      ( match Embed.get_arith trm with
+      | Some poly -> poly
+      | None -> Sum.of_ (Mono.of_ trm 1) Q.one )
+      |> check (fun poly ->
+             assert (equal poly (CM.to_poly (CM.of_trm trm))) )
+
+    (** Project out the term embedded into a polynomial, if possible *)
+    let get_trm poly =
+      match get_mono poly with
+      | Some mono -> Mono.get_trm mono
+      | None -> None
+
+    (* constructors over indeterminates *)
+
+    let mul e1 e2 = CM.to_poly (CM.mul (CM.of_trm e1) (CM.of_trm e2))
+
+    let div n d =
+      CM.to_poly (CM.mul (CM.of_trm n) (CM.of_trm d ~power:(-1)))
+
+    let pow base power = CM.to_poly (CM.of_trm base ~power)
+
+    (* transform *)
+
+    let map poly ~f =
+      let p, p' = (poly, Sum.empty) in
+      let p, p' =
+        Sum.fold poly ~init:(p, p') ~f:(fun mono coeff (p, p') ->
+            let m, cm' = (mono, CM.one) in
+            let m, cm' =
+              Prod.fold mono ~init:(m, cm') ~f:(fun trm power (m, cm') ->
+                  let trm' = f trm in
+                  if trm == trm' then (m, cm')
+                  else
+                    (Prod.remove m trm, CM.mul cm' (CM.of_trm trm' ~power)) )
+            in
+            if CM.equal_one cm' then (p, p')
+            else
+              ( Sum.remove p mono
+              , Sum.union p' (CM.to_poly (CM.mul (coeff, m) cm')) ) )
+      in
+      if Sum.is_empty p' then poly else Sum.union p p' |> check invariant
+
+    (* traverse *)
+
+    let iter poly =
+      Iter.from_iter (fun f ->
+          Sum.iter poly ~f:(fun mono _ ->
+              Prod.iter mono ~f:(fun trm _ -> f trm) ) )
+
+    type product = Prod.t
+
+    let fold_factors = Prod.fold
+    let fold_monomials = Sum.fold
+  end
+end

sledge/src/arithmetic.mli

@@ -0,0 +1,15 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Arithmetic terms *)
+
+include module type of Arithmetic_intf
+
+module Representation (Indeterminate : INDETERMINATE) :
+  REPRESENTATION
+    with type var := Indeterminate.var
+    with type trm := Indeterminate.trm

sledge/src/arithmetic_intf.ml

@@ -0,0 +1,104 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(** Arithmetic terms *)
+
+open Ses
+
+module type S = sig
+  type var
+  type trm
+  type t [@@deriving compare, equal, sexp]
+
+  val ppx : var Var.strength -> t pp
+
+  (** Construct and Destruct atomic terms *)
+
+  val const : Q.t -> t
+  (** [const q] represents the constant [q] *)
+
+  val get_const : t -> Q.t option
+  (** [get_const a] is [Some q] iff [equal a (const q)] *)
+
+  val trm : trm -> t
+  (** [trm x] represents the indeterminate term [x] *)
+
+  val get_trm : t -> trm option
+  (** [get_trm a] is [Some x] iff [equal a (trm x)] *)
+
+  type view = Trm of trm | Const of Q.t | Compound
+
+  val classify : t -> view
+  (** [classify a] is [Trm x] iff [get_trm a] is [Some x], [Const q] iff
+      [get_const a] is [Some q], and [Compound] otherwise *)
+
+  (** Construct compound terms *)
+
+  val neg : t -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mulc : Q.t -> t -> t
+  val mul : trm -> trm -> t
+  val div : trm -> trm -> t
+  val pow : trm -> int -> t
+
+  (** Transform *)
+
+  val map : t -> f:(trm -> trm) -> t
+  (** [map ~f a] is [a] with each indeterminate transformed by [f]. Viewing
+      [a] as a polynomial,
+      [map ~f (Σᵢ₌₁ⁿ cᵢ × Πⱼ₌₁ᵐᵢ xᵢⱼ^pᵢⱼ)] is
+      [Σᵢ₌₁ⁿ cᵢ × Πⱼ₌₁ᵐᵢ (f xᵢⱼ)^pᵢⱼ]. *)
+
+  (** Traverse *)
+
+  val iter : t -> trm iter
+  (** [iter a] enumerates the indeterminate terms appearing in [a] *)
+
+  (**/**)
+
+  type product
+
+  val fold_factors : product -> init:'s -> f:(trm -> int -> 's -> 's) -> 's
+  val fold_monomials : t -> init:'s -> f:(product -> Q.t -> 's -> 's) -> 's
+end
+
+(** Indeterminate terms, treated as atomic / variables except when they can
+    be flattened using [EMBEDDING.get_arith]. *)
+module type INDETERMINATE = sig
+  type trm [@@deriving compare, equal, sexp]
+  type var
+
+  val ppx : var Var.strength -> trm pp
+end
+
+(** An embedding of arithmetic terms [t] into indeterminates [trm],
+    expressed as a partial projection from [trm] to [t]. The inverse
+    embedding function is generally internal to the client. *)
+module type EMBEDDING = sig
+  type trm
+  type t
+
+  val get_arith : trm -> t option
+  (** [get_arith x] should be [Some a] if indeterminate [x] is equivalent to
+      [a] embedded into an indeterminate term. This is used to flatten
+      indeterminates that are actually arithmetic for the client, thereby
+      enabling arithmetic operations to be interpreted more often. *)
+end
+
+(** A type [t] representing arithmetic terms over indeterminates [trm]
+    together with a functor [Make] that takes an [EMBEDDING] of arithmetic
+    terms [t] into indeterminates [trm] and produces an implementation of
+    the primary interface [S]. *)
+module type REPRESENTATION = sig
+  type t [@@deriving compare, equal, sexp]
+  type var
+  type trm
+
+  module Make (_ : EMBEDDING with type trm := trm and type t := t) :
+    S with type var := var with type trm := trm with type t := t
+end

sledge/src/fol.ml

@@ -5,110 +5,239 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Ses
+
 let pp_boxed fs fmt =
   Format.pp_open_box fs 2 ;
   Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
 
-module Funsym = Ses.Funsym
-module Predsym = Ses.Predsym
-
 (*
  * Terms
  *)
 
-(** Terms, denoting functions from structures to values, built from
-    variables and applications of function symbols from various theories. *)
-type trm =
-  (* variables *)
-  | Var of {id: int; name: string}
-  (* arithmetic *)
-  | Z of Z.t
-  | Q of Q.t
-  | Neg of trm
-  | Add of trm * trm
-  | Sub of trm * trm
-  | Mulq of Q.t * trm
-  (* sequences (of non-fixed size) *)
-  | Splat of trm
-  | Sized of {seq: trm; siz: trm}
-  | Extract of {seq: trm; off: trm; len: trm}
-  | Concat of trm array
-  (* records (with fixed indices) *)
-  | Select of {idx: int; rcd: trm}
-  | Update of {idx: int; rcd: trm; elt: trm}
-  | Record of trm array
-  | Ancestor of int
-  (* uninterpreted *)
-  | Apply of Funsym.t * trm array
-[@@deriving compare, equal, sexp]
-
-let compare_trm x y =
-  if x == y then 0
-  else
-    match (x, y) with
-    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-        Int.compare i j
-    | _ -> compare_trm x y
+(** Variable terms, represented as a subtype of general terms *)
+module rec Var : sig
+  include Var_intf.VAR with type t = private Trm.trm
 
-let equal_trm x y =
-  x == y
-  ||
-  match (x, y) with
-  | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
-      Int.equal i j
-  | _ -> equal_trm x y
+  val of_ : Trm.trm -> t
+end = struct
+  module T = struct
+    type t = Trm.trm [@@deriving compare, equal, sexp]
 
-(* destructors *)
+    let invariant x =
+      let@ () = Invariant.invariant [%here] x [%sexp_of: t] in
+      match x with
+      | Var _ -> ()
+      | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_t x) ()
 
-let get_z = function Z z -> Some z | _ -> None
-let get_q = function Q q -> Some q | Z z -> Some (Q.of_z z) | _ -> None
+    let make ~id ~name = Trm._Var id name |> check invariant
+    let id = function Trm.Var v -> v.id | x -> violates invariant x
+    let name = function Trm.Var v -> v.name | x -> violates invariant x
+  end
 
-(* constructors *)
+  include Var0.Make (T)
 
-(* statically allocated since they are tested with == *)
-let zero = Z Z.zero
-let one = Z Z.one
+  let of_ v = v |> check T.invariant
+end
 
-let _Z z =
-  if Z.equal Z.zero z then zero else if Z.equal Z.one z then one else Z z
+and Arith0 :
+  (Arithmetic.REPRESENTATION
+    with type var := Var.t
+    with type trm := Trm.trm) =
+  Arithmetic.Representation (Trm)
+
+and Arith :
+  (Arithmetic.S
+    with type var := Var.t
+    with type trm := Trm.trm
+    with type t = Arith0.t) = struct
+  include Arith0
+
+  include Make (struct
+    let get_arith (e : Trm.trm) =
+      match e with
+      | Z z -> Some (Arith.const (Q.of_z z))
+      | Q q -> Some (Arith.const q)
+      | Arith a -> Some a
+      | _ -> None
+  end)
+end
 
-let _Q q = if Z.equal Z.one (Q.den q) then _Z (Q.num q) else Q q
-let _Neg x = Neg x
+(** Terms, built from variables and applications of function symbols from
+    various theories. Denote functions from structures to values. *)
+and Trm : sig
+  type var = Var.t
 
-let _Add x y =
-  match (x, y) with
-  | _, Q q when Q.sign q = 0 -> x
-  | Q q, _ when Q.sign q = 0 -> y
-  | _ -> Add (x, y)
+  type trm = private
+    (* variables *)
+    | Var of {id: int; name: string}
+    (* arithmetic *)
+    | Z of Z.t
+    | Q of Q.t
+    | Arith of Arith.t
+    (* sequences (of flexible size) *)
+    | Splat of trm
+    | Sized of {seq: trm; siz: trm}
+    | Extract of {seq: trm; off: trm; len: trm}
+    | Concat of trm array
+    (* records (with fixed indices) *)
+    | Select of {idx: int; rcd: trm}
+    | Update of {idx: int; rcd: trm; elt: trm}
+    | Record of trm array
+    | Ancestor of int
+    (* uninterpreted *)
+    | Apply of Funsym.t * trm array
+  [@@deriving compare, equal, sexp]
 
-let _Sub x y = Sub (x, y)
+  val ppx : Var.t Var.strength -> trm pp
+  val _Var : int -> string -> trm
+  val _Z : Z.t -> trm
+  val _Q : Q.t -> trm
+  val _Arith : Arith.t -> trm
+  val _Splat : trm -> trm
+  val _Sized : trm -> trm -> trm
+  val _Extract : trm -> trm -> trm -> trm
+  val _Concat : trm array -> trm
+  val _Select : int -> trm -> trm
+  val _Update : int -> trm -> trm -> trm
+  val _Record : trm array -> trm
+  val _Ancestor : int -> trm
+  val _Apply : Funsym.t -> trm array -> trm
+end = struct
+  type var = Var.t
+
+  type trm =
+    | Var of {id: int; name: string}
+    | Z of Z.t
+    | Q of Q.t
+    | Arith of Arith.t
+    | Splat of trm
+    | Sized of {seq: trm; siz: trm}
+    | Extract of {seq: trm; off: trm; len: trm}
+    | Concat of trm array
+    | Select of {idx: int; rcd: trm}
+    | Update of {idx: int; rcd: trm; elt: trm}
+    | Record of trm array
+    | Ancestor of int
+    | Apply of Funsym.t * trm array
+  [@@deriving compare, equal, sexp]
 
-let _Mulq q x =
-  if Q.equal Q.one q then x else if Q.sign q = 0 then zero else Mulq (q, x)
+  let compare_trm x y =
+    if x == y then 0
+    else
+      match (x, y) with
+      | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+          Int.compare i j
+      | _ -> compare_trm x y
+
+  let equal_trm x y =
+    x == y
+    ||
+    match (x, y) with
+    | Var {id= i; name= _}, Var {id= j; name= _} when i > 0 && j > 0 ->
+        Int.equal i j
+    | _ -> equal_trm x y
+
+  let rec ppx strength fs trm =
+    let rec pp fs trm =
+      let pf fmt = pp_boxed fs fmt in
+      match trm with
+      | Var _ as v -> Var.ppx strength fs (Var.of_ v)
+      | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z
+      | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q
+      | Arith a -> Arith.ppx strength fs a
+      | Splat x -> pf "%a^" pp x
+      | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
+      | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
+      | Concat [||] -> pf "@<2>⟨⟩"
+      | Concat xs -> pf "(%a)" (Array.pp "@,^" pp) xs
+      | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx
+      | Update {idx; rcd; elt} ->
+          pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
+      | Record xs -> pf "{%a}" (ppx_record strength) xs
+      | Ancestor i -> pf "(ancestor %i)" i
+      | Apply (f, [||]) -> pf "%a" Funsym.pp f
+      | Apply
+          ( ( (Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr)
+            as f )
+          , [|x; y|] ) ->
+          pf "(%a@ %a@ %a)" pp x Funsym.pp f pp y
+      | Apply (f, es) ->
+          pf "%a(%a)" Funsym.pp f (Array.pp ",@ " (ppx strength)) es
+    in
+    pp fs trm
+
+  and ppx_record strength fs elts =
+    [%Trace.fprintf
+      fs "%a"
+        (fun fs elts ->
+          let exception Not_a_string in
+          match
+            String.init (Array.length elts) ~f:(fun i ->
+                match elts.(i) with
+                | Z c -> Char.of_int_exn (Z.to_int c)
+                | _ -> raise Not_a_string )
+          with
+          | s -> Format.fprintf fs "%S" s
+          | exception (Not_a_string | Z.Overflow | Failure _) ->
+              Format.fprintf fs "@[<h>%a@]"
+                (Array.pp ",@ " (ppx strength))
+                elts )
+        elts]
+
+  (* destructors *)
+
+  let get_z = function Z z -> Some z | _ -> None
+  let get_q = function Q q -> Some q | Z z -> Some (Q.of_z z) | _ -> None
+
+  (* constructors *)
+
+  let _Var id name = Var {id; name}
+
+  (* statically allocated since they are tested with == *)
+  let zero = Z Z.zero
+  let one = Z Z.one
+
+  let _Z z =
+    if Z.equal Z.zero z then zero else if Z.equal Z.one z then one else Z z
+
+  let _Q q = if Z.equal Z.one (Q.den q) then _Z (Q.num q) else Q q
+
+  let _Arith a =
+    match Arith.classify a with
+    | Trm e -> e
+    | Const q -> _Q q
+    | Compound -> Arith a
+
+  let _Splat x = Splat x
+  let _Sized seq siz = Sized {seq; siz}
+  let _Extract seq off len = Extract {seq; off; len}
+  let _Concat es = Concat es
+  let _Select idx rcd = Select {idx; rcd}
+  let _Update idx rcd elt = Update {idx; rcd; elt}
+  let _Record es = Record es
+  let _Ancestor i = Ancestor i
+
+  let _Apply f es =
+    match
+      Funsym.eval ~equal:equal_trm ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es
+    with
+    | Some c -> c
+    | None -> Apply (f, es)
+end
 
-let _Splat x = Splat x
-let _Sized seq siz = Sized {seq; siz}
-let _Extract seq off len = Extract {seq; off; len}
-let _Concat es = Concat es
-let _Select idx rcd = Select {idx; rcd}
-let _Update idx rcd elt = Update {idx; rcd; elt}
-let _Record es = Record es
-let _Ancestor i = Ancestor i
+open Trm
 
-let _Apply f es =
-  match
-    Funsym.eval ~equal:equal_trm ~get_z ~ret_z:_Z ~get_q ~ret_q:_Q f es
-  with
-  | Some c -> c
-  | None -> Apply (f, es)
+let zero = _Z Z.zero
+let one = _Z Z.one
 
 (*
  * Formulas
  *)
 
-(** Formulas, denoting sets of structures, built from propositional
-    variables, applications of predicate symbols from various theories, and
-    first-order logic connectives. *)
+(** Formulas, built from literals with predicate symbols from various
+    theories, and propositional constants and connectives. Denote sets of
+    structures. *)
 module Fml : sig
   type fml = private
     (* propositional constants *)
@@ -421,96 +550,14 @@ type cnd = [`Ite of fml * cnd * cnd | `Trm of trm]
     formulas. *)
 type exp = [cnd | `Fml of fml] [@@deriving compare, equal, sexp]
 
-(*
- * Variables
- *)
-
-(** Variable terms *)
-module Var : sig
-  include Ses.Var_intf.VAR with type t = private trm
-
-  val of_ : trm -> t
-end = struct
-  module T = struct
-    type t = trm [@@deriving compare, equal, sexp]
-  end
-
-  let invariant (x : trm) =
-    let@ () = Invariant.invariant [%here] x [%sexp_of: trm] in
-    match x with
-    | Var _ -> ()
-    | _ -> fail "non-var: %a" Sexp.pp_hum (sexp_of_trm x) ()
-
-  include Ses.Var0.Make (struct
-    include T
-
-    let make ~id ~name = Var {id; name} |> check invariant
-    let id = function Var v -> v.id | x -> violates invariant x
-    let name = function Var v -> v.name | x -> violates invariant x
-  end)
-
-  let of_ v = v |> check invariant
-end
-
-type var = Var.t
-
 (*
  * Representation operations
  *)
 
 (** pp *)
 
-let rec ppx_t strength fs trm =
-  let rec pp fs trm =
-    let pf fmt = pp_boxed fs fmt in
-    match trm with
-    | Var _ as v -> Var.ppx strength fs (Var.of_ v)
-    | Z z -> Trace.pp_styled `Magenta "%a" fs Z.pp z
-    | Q q -> Trace.pp_styled `Magenta "%a" fs Q.pp q
-    | Neg x -> pf "(- %a)" pp x
-    | Add (x, y) -> pf "(%a@ + %a)" pp x pp y
-    | Sub (x, y) -> pf "(%a@ - %a)" pp x pp y
-    | Mulq (q, x) -> pf "(%a@ @<2>× %a)" Q.pp q pp x
-    | Splat x -> pf "%a^" pp x
-    | Sized {seq; siz} -> pf "@<1>⟨%a,%a@<1>⟩" pp siz pp seq
-    | Extract {seq; off; len} -> pf "%a[%a,%a)" pp seq pp off pp len
-    | Concat [||] -> pf "@<2>⟨⟩"
-    | Concat xs -> pf "(%a)" (Array.pp "@,^" pp) xs
-    | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx
-    | Update {idx; rcd; elt} -> pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
-    | Record xs -> pf "{%a}" (ppx_record strength) xs
-    | Ancestor i -> pf "(ancestor %i)" i
-    | Apply (f, [||]) -> pf "%a" Funsym.pp f
-    | Apply
-        ( ( ( Mul | Div | Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr
-            | BitAshr ) as f )
-        , [|x; y|] ) ->
-        pf "(%a@ %a@ %a)" pp x Funsym.pp f pp y
-    | Apply (f, es) ->
-        pf "%a(%a)" Funsym.pp f (Array.pp ",@ " (ppx_t strength)) es
-  in
-  pp fs trm
-
-and ppx_record strength fs elts =
-  [%Trace.fprintf
-    fs "%a"
-      (fun fs elts ->
-        let exception Not_a_string in
-        match
-          String.init (Array.length elts) ~f:(fun i ->
-              match elts.(i) with
-              | Z c -> Char.of_int_exn (Z.to_int c)
-              | _ -> raise Not_a_string )
-        with
-        | s -> Format.fprintf fs "%S" s
-        | exception (Not_a_string | Z.Overflow | Failure _) ->
-            Format.fprintf fs "@[<h>%a@]"
-              (Array.pp ",@ " (ppx_t strength))
-              elts )
-      elts]
-
 let ppx_f strength fs fml =
-  let pp_t = ppx_t strength in
+  let pp_t = Trm.ppx strength in
   let rec pp fs fml =
     let pf fmt = pp_boxed fs fmt in
     match (fml : fml) with
@@ -539,7 +586,7 @@ let ppx_f strength fs fml =
 let pp_f = ppx_f (fun _ -> None)
 
 let ppx_c strength fs ct =
-  let pp_t = ppx_t strength in
+  let pp_t = Trm.ppx strength in
   let pp_f = ppx_f strength in
   let rec pp fs ct =
     let pf fmt = pp_boxed fs fmt in
@@ -559,20 +606,20 @@ let pp = ppx (fun _ -> None)
 
 let rec fold_vars_t e ~init ~f =
   match e with
-  | Var _ as v -> f init (Var.of_ v)
   | Z _ | Q _ | Ancestor _ -> init
-  | Neg x | Mulq (_, x) | Splat x | Select {rcd= x} ->
-      fold_vars_t ~f x ~init
-  | Add (x, y)
-   |Sub (x, y)
-   |Sized {seq= x; siz= y}
-   |Update {rcd= x; elt= y} ->
+  | Var _ as v -> f init (Var.of_ v)
+  | Splat x | Select {rcd= x} -> fold_vars_t ~f x ~init
+  | Sized {seq= x; siz= y} | Update {rcd= x; elt= y} ->
       fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
   | Extract {seq= x; off= y; len= z} ->
       fold_vars_t ~f x
         ~init:(fold_vars_t ~f y ~init:(fold_vars_t ~f z ~init))
   | Concat xs | Record xs | Apply (_, xs) ->
       Array.fold ~f:(fun init -> fold_vars_t ~f ~init) xs ~init
+  | Arith a ->
+      Iter.fold
+        ~f:(fun s x -> fold_vars_t ~f x ~init:s)
+        ~init (Arith.iter a)
 
 let rec fold_vars_f ~init p ~f =
   match (p : fml) with
@@ -645,11 +692,10 @@ let rec map_trms_f ~f b =
 let rec map_vars_t ~f e =
   match e with
   | Var _ as v -> (f (Var.of_ v) : var :> trm)
-  | Z _ | Q _ | Ancestor _ -> e
-  | Neg x -> map1 (map_vars_t ~f) e _Neg x
-  | Add (x, y) -> map2 (map_vars_t ~f) e _Add x y
-  | Sub (x, y) -> map2 (map_vars_t ~f) e _Sub x y
-  | Mulq (q, x) -> map1 (map_vars_t ~f) e (_Mulq q) x
+  | Z _ | Q _ -> e
+  | Arith a ->
+      let a' = Arith.map ~f:(map_vars_t ~f) a in
+      if a == a' then e else _Arith a'
   | Splat x -> map1 (map_vars_t ~f) e _Splat x
   | Sized {seq; siz} -> map2 (map_vars_t ~f) e _Sized seq siz
   | Extract {seq; off; len} -> map3 (map_vars_t ~f) e _Extract seq off len
@@ -657,6 +703,7 @@ let rec map_vars_t ~f e =
   | Select {idx; rcd} -> map1 (map_vars_t ~f) e (_Select idx) rcd
   | Update {idx; rcd; elt} -> map2 (map_vars_t ~f) e (_Update idx) rcd elt
   | Record xs -> mapN (map_vars_t ~f) e _Record xs
+  | Ancestor _ -> e
   | Apply (g, xs) -> mapN (map_vars_t ~f) e (_Apply g) xs
 
 let map_vars_f ~f = map_trms_f ~f:(map_vars_t ~f)
@@ -844,35 +891,19 @@ module Term = struct
 
   let var v = `Trm (v : var :> trm)
 
-  (* constants *)
+  (* arithmetic *)
 
   let zero = `Trm zero
   let one = `Trm one
-
-  let integer z =
-    if Z.equal Z.zero z then zero
-    else if Z.equal Z.one z then one
-    else `Trm (Z z)
-
-  let rational q = `Trm (Q q)
-
-  (* arithmetic *)
-
-  let neg = ap1t _Neg
-  let add = ap2t _Add
-  let sub = ap2t _Sub
-  let mulq q = ap1t (_Mulq q)
-
-  let mul =
-    ap2 (fun x y ->
-        match x with
-        | Z z -> mulq (Q.of_z z) (`Trm y)
-        | Q q -> mulq q (`Trm y)
-        | _ -> (
-          match y with
-          | Z z -> mulq (Q.of_z z) (`Trm x)
-          | Q q -> mulq q (`Trm x)
-          | _ -> ap2t (fun x y -> Apply (Mul, [|x; y|])) (`Trm x) (`Trm y) ) )
+  let integer z = `Trm (_Z z)
+  let rational q = `Trm (_Q q)
+  let neg = ap1t @@ fun x -> _Arith Arith.(neg (trm x))
+  let add = ap2t @@ fun x y -> _Arith Arith.(add (trm x) (trm y))
+  let sub = ap2t @@ fun x y -> _Arith Arith.(sub (trm x) (trm y))
+  let mulq q = ap1t @@ fun x -> _Arith Arith.(mulc q (trm x))
+  let mul = ap2t @@ fun x y -> _Arith (Arith.mul x y)
+  let div = ap2t @@ fun x y -> _Arith (Arith.div x y)
+  let pow x i = (ap1t @@ fun x -> _Arith (Arith.pow x i)) x
 
   (* sequences *)
 
@@ -888,33 +919,25 @@ module Term = struct
   let record elts = apNt _Record elts
   let ancestor i = `Trm (_Ancestor i)
 
-  (* if-then-else *)
-
-  let ite ~cnd ~thn ~els = ite cnd thn els
-
   (* uninterpreted *)
 
   let apply sym args = apNt (_Apply sym) args
 
+  (* if-then-else *)
+
+  let ite ~cnd ~thn ~els = ite cnd thn els
+
   (** Destruct *)
 
   let d_int = function `Trm (Z z) -> Some z | _ -> None
 
   (** Access *)
 
-  let const_of x =
-    let rec const_of t =
-      let neg = Option.map ~f:Q.neg in
-      let add = Option.map2 ~f:Q.add in
-      match t with
-      | Z z -> Some (Q.of_z z)
-      | Q q -> Some q
-      | Neg x -> neg (const_of x)
-      | Add (x, y) -> add (const_of x) (const_of y)
-      | Sub (x, y) -> add (const_of x) (neg (const_of y))
-      | _ -> None
-    in
-    match x with `Trm t -> const_of t | _ -> None
+  let const_of = function
+    | `Trm (Z z) -> Some (Q.of_z z)
+    | `Trm (Q q) -> Some q
+    | `Trm (Arith a) -> Arith.get_const a
+    | _ -> None
 
   (** Traverse *)
 
@@ -1093,14 +1116,22 @@ let vs_to_ses : Var.Set.t -> Ses.Var.Set.t =
   Var.Set.fold vs ~init:Ses.Var.Set.empty ~f:(fun vs v ->
       Ses.Var.Set.add vs (v_to_ses v) )
 
-let rec t_to_ses : trm -> Ses.Term.t = function
+let rec arith_to_ses poly =
+  Arith.fold_monomials poly ~init:Ses.Term.zero ~f:(fun mono coeff e ->
+      Ses.Term.add e
+        (Ses.Term.mulq coeff
+           (Arith.fold_factors mono ~init:Ses.Term.one ~f:(fun trm pow f ->
+                let rec exp b i =
+                  assert (i > 0) ;
+                  if i = 1 then b else Ses.Term.mul b (exp f (i - 1))
+                in
+                Ses.Term.mul f (exp (t_to_ses trm) pow) ))) )
+
+and t_to_ses : trm -> Ses.Term.t = function
   | Var {name; id} -> Ses.Term.var (Ses.Var.identified ~name ~id)
   | Z z -> Ses.Term.integer z
   | Q q -> Ses.Term.rational q
-  | Neg x -> Ses.Term.neg (t_to_ses x)
-  | Add (x, y) -> Ses.Term.add (t_to_ses x) (t_to_ses y)
-  | Sub (x, y) -> Ses.Term.sub (t_to_ses x) (t_to_ses y)
-  | Mulq (q, x) -> Ses.Term.mulq q (t_to_ses x)
+  | Arith a -> arith_to_ses a
   | Splat x -> Ses.Term.splat (t_to_ses x)
   | Sized {seq; siz} ->
       Ses.Term.sized ~seq:(t_to_ses seq) ~siz:(t_to_ses siz)
@@ -1114,8 +1145,6 @@ let rec t_to_ses : trm -> Ses.Term.t = function
   | Record es ->
       Ses.Term.record (IArray.of_array (Array.map ~f:t_to_ses es))
   | Ancestor i -> Ses.Term.rec_record i
-  | Apply (Mul, [|x; y|]) -> Ses.Term.mul (t_to_ses x) (t_to_ses y)
-  | Apply (Div, [|x; y|]) -> Ses.Term.div (t_to_ses x) (t_to_ses y)
   | Apply (Rem, [|x; y|]) -> Ses.Term.rem (t_to_ses x) (t_to_ses y)
   | Apply (BitAnd, [|x; y|]) -> Ses.Term.and_ (t_to_ses x) (t_to_ses y)
   | Apply (BitOr, [|x; y|]) -> Ses.Term.or_ (t_to_ses x) (t_to_ses y)
@@ -1171,8 +1200,8 @@ let vs_of_ses : Ses.Var.Set.t -> Var.Set.t =
   Ses.Var.Set.fold vs ~init:Var.Set.empty ~f:(fun vs v ->
       Var.Set.add vs (v_of_ses v) )
 
-let uap1 f = ap1t (fun x -> Apply (f, [|x|]))
-let uap2 f = ap2t (fun x y -> Apply (f, [|x; y|]))
+let uap1 f = ap1t (fun x -> _Apply f [|x|])
+let uap2 f = ap2t (fun x y -> _Apply f [|x; y|])
 let uposN p = apNf (_UPosLit p)
 let unegN p = apNf (_UNegLit p)
 
@@ -1237,18 +1266,18 @@ and of_ses : Ses.Term.t -> exp =
     | Some (e, q, prod) ->
         let rec expn e n =
           let p = Z.pred n in
-          if Z.sign p = 0 then e else uap2 Mul e (expn e p)
+          if Z.sign p = 0 then e else mul e (expn e p)
         in
         let exp e q =
           let n = Q.num q in
           let sn = Z.sign n in
           if sn = 0 then of_ses e
           else if sn > 0 then expn (of_ses e) n
-          else uap2 Div one (expn (of_ses e) (Z.neg n))
+          else div one (expn (of_ses e) (Z.neg n))
         in
         Ses.Term.Qset.fold prod ~init:(exp e q) ~f:(fun e q s ->
-            uap2 Mul (exp e q) s ) )
-  | Ap2 (Div, d, e) -> uap_ttt Div d e
+            mul (exp e q) s ) )
+  | Ap2 (Div, d, e) -> div (of_ses d) (of_ses e)
   | Ap2 (Rem, d, e) -> uap_ttt Rem d e
   | And es -> apN and_ (uap2 BitAnd) tt es
   | Or es -> apN or_ (uap2 BitOr) ff es

sledge/src/fol.mli

@@ -5,26 +5,10 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
-(** Variables *)
-module Var : sig
-  include Ses.Var_intf.VAR
-
-  module Subst : sig
-    type var := t
-    type t [@@deriving compare, equal, sexp]
-    type x = {sub: t; dom: Set.t; rng: Set.t}
+open Ses
 
-    val pp : t pp
-    val empty : t
-    val freshen : Set.t -> wrt:Set.t -> x * Set.t
-    val invert : t -> t
-    val restrict : t -> Set.t -> x
-    val is_empty : t -> bool
-    val domain : t -> Set.t
-    val range : t -> Set.t
-    val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a
-  end
-end
+(** Variables *)
+module Var : Var_intf.VAR
 
 (** Terms *)
 module rec Term : sig
@@ -51,8 +35,10 @@ module rec Term : sig
   val sub : t -> t -> t
   val mulq : Q.t -> t -> t
   val mul : t -> t -> t
+  val div : t -> t -> t
+  val pow : t -> int -> t
 
-  (* sequences (of non-fixed size) *)
+  (* sequences (of flexible size) *)
   val splat : t -> t
   val sized : seq:t -> siz:t -> t
   val extract : seq:t -> off:t -> len:t -> t
@@ -65,7 +51,7 @@ module rec Term : sig
   val ancestor : int -> t
 
   (* uninterpreted *)
-  val apply : Ses.Funsym.t -> t array -> t
+  val apply : Funsym.t -> t array -> t
 
   (* if-then-else *)
   val ite : cnd:Formula.t -> thn:t -> els:t -> t
@@ -130,8 +116,8 @@ and Formula : sig
   val le : Term.t -> Term.t -> t
 
   (* uninterpreted *)
-  val uposlit : Ses.Predsym.t -> Term.t array -> t
-  val uneglit : Ses.Predsym.t -> Term.t array -> t
+  val uposlit : Predsym.t -> Term.t array -> t
+  val uneglit : Predsym.t -> Term.t array -> t
 
   (* connectives *)
   val not_ : t -> t

sledge/src/llair_to_Fol.ml

@@ -111,9 +111,9 @@ and term : Llair.Exp.t -> T.t =
   | Ap2 (Add, _, d, e) -> ap_ttt T.add d e
   | Ap2 (Sub, _, d, e) -> ap_ttt T.sub d e
   | Ap2 (Mul, _, d, e) -> ap_ttt T.mul d e
-  | Ap2 (Div, _, d, e) -> ap_ttt (uap2 Div) d e
+  | Ap2 (Div, _, d, e) -> ap_ttt T.div d e
   | Ap2 (Rem, _, d, e) -> ap_ttt (uap2 Rem) d e
-  | Ap2 (Udiv, typ, d, e) -> ap_uut (uap2 Div) typ d e
+  | Ap2 (Udiv, typ, d, e) -> ap_uut T.div typ d e
   | Ap2 (Urem, typ, d, e) -> ap_uut (uap2 Rem) typ d e
   | Ap2 (And, _, d, e) -> ap_ttt (uap2 BitAnd) d e
   | Ap2 (Or, _, d, e) -> ap_ttt (uap2 BitOr) d e

sledge/src/ses/funsym.ml

@@ -8,8 +8,6 @@
 (** Function Symbols *)
 
 type t =
-  | Mul
-  | Div
   | Rem
   | BitAnd
   | BitOr
@@ -25,8 +23,6 @@ type t =
 let pp ppf f =
   let pf fmt = Format.fprintf ppf fmt in
   match f with
-  | Mul -> pf "@<1>×"
-  | Div -> pf "/"
   | Rem -> pf "%%"
   | BitAnd -> pf "&&"
   | BitOr -> pf "||"

sledge/src/ses/funsym.mli

@@ -12,8 +12,6 @@
     applied to literal values of the expected sorts are reduced to literal
     values. *)
 type t =
-  | Mul  (** Multiplication *)
-  | Div  (** Division, for integers result is truncated toward zero *)
   | Rem
       (** Remainder of division, satisfies [a = b * div a b + rem a b] and
           for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)

sledge/src/ses/term.ml

@@ -380,7 +380,7 @@ module Sum = struct
   let mul_const const sum =
     assert (not (Q.equal Q.zero const)) ;
     if Q.equal Q.one const then sum
-    else Qset.map_counts ~f:(fun _ -> Q.mul const) sum
+    else Qset.map_counts ~f:(Q.mul const) sum
 
   let to_term sum =
     match Qset.classify sum with

sledge/src/test/fol_test.ml

@@ -189,8 +189,8 @@ let%test_module _ =
       pp_raw r3 ;
       [%expect
         {|
-        (%z_7 × (%y_6 × %y_6)) = %t_1
-      ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (%z_7 × %y_6)
+        (1 × (%z_7 × %y_6^2)) = %t_1
+      ∧ %z_7 = %u_2 = %v_3 = %w_4 = %x_5 = (1 × (%z_7 × %y_6))
 
       {sat= true;
        rep= [[0 ↦ ];
@@ -216,7 +216,9 @@ let%test_module _ =
       pp_raw r4 ;
       [%expect
         {|
-        (8 + %z_7) = %x_5 ∧ (3 + %z_7) = %w_4 ∧ (-4 + %z_7) = %y_6
+        (1 × (%z_7) + 8) = %x_5
+      ∧ (1 × (%z_7) + 3) = %w_4
+      ∧ (1 × (%z_7) + -4) = %y_6
 
       {sat= true;
        rep= [[0 ↦ ];
@@ -322,7 +324,7 @@ let%test_module _ =
       pp_raw r8 ;
       [%expect
         {|
-        (13 × %z_7) = %x_5 ∧ 14 = %y_6
+        (13 × (%z_7)) = %x_5 ∧ 14 = %y_6
     
       {sat= true;
        rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%y_6 ↦ 14]; [%x_5 ↦ (13 × %z_7)]]} |}]
@@ -361,11 +363,11 @@ let%test_module _ =
         {sat= true;
          rep= [[0 ↦ ]; [-1 ↦ ]; [%z_7 ↦ ]; [%x_5 ↦ (-16 + %z_7)]]}
 
-        (%z_7 - (%x_5 + 8))
+        (1 × (%z_7) + -1 × (%x_5) + -8)
 
         8
 
-        ((%x_5 + 8) - %z_7)
+        (-1 × (%z_7) + 1 × (%x_5) + 8)
 
         -8 |}]
 
@@ -378,13 +380,13 @@ let%test_module _ =
 
     let%expect_test _ =
       pp r11 ;
-      [%expect {| (-16 + %z_7) = %x_5 |}]
+      [%expect {| (1 × (%z_7) + -16) = %x_5 |}]
 
     let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
 
     let%expect_test _ =
       pp r12 ;
-      [%expect {| (-16 + %z_7) = %x_5 |}]
+      [%expect {| (1 × (%z_7) + -16) = %x_5 |}]
 
     let r13 =
       of_eqs
@@ -486,7 +488,7 @@ let%test_module _ =
                [%y_6 ↦ ];
                [%x_5 ↦ ]]}
 
-          (-1 + %y_6) = %y_6^ ∧ %x_5 = %x_5^ |}]
+          (1 × (%y_6) + -1) = %y_6^ ∧ %x_5 = %x_5^ |}]
 
     let r19 = of_eqs [(x, y + z); (x, !0); (y, !0)]
 

sledge/src/test/sh_test.ml

@@ -145,11 +145,11 @@ let%test_module _ =
       pp q' ;
       [%expect
         {|
-        ∃ %x_6 .   (-1 + %y_7) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
-    
-          ((-1 + %y_7) = %y_7^) ∧ emp
+        ∃ %x_6 .   (1 × (%y_7) + -1) = %y_7^ ∧ %x_6 = %x_6^ ∧ emp
+
+          ((1 × (%y_7) + -1) = %y_7^) ∧ emp
 
-          (-1 + %y_7) = %y_7^ ∧ emp |}]
+          (1 × (%y_7) + -1) = %y_7^ ∧ emp |}]
 
     let%expect_test _ =
       let q =

sledge/src/test/solver_test.ml

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