From 1a4363627c80b66a2d1e0d78a281cc32bf437c17 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:36:19 -0800
Subject: [PATCH] [sledge] Revise Arith.map to use maximal non-interpreted
 subterms
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
Change Arith.map to not descend through non-interpreted arithmetic
operators. For example, in `2×(x × y) + 3×z + 4`, `map ~f` will apply
`f` to the subterms `x × y` and `z`, but not `x` or `y`.

The logical notion of "subterm" that is needed by the solver does not
coincide with the representation. This is essentially due to not
"flattening" or "purifying" terms.  That is, traditionally `x × y`
would not be permitted as an indeterminate of a polynomial. Instead, a
new variable would need to be introduced: `v = x × y` and then the
polynomial would be expressed as `2×v + 3×z + 4`. Taking maximal
non-interpreted subterms as the definition of "subterm" results in
subterms in the non-flattened representation that are equivalent to
those that would result from flattening the representation.

Reviewed By: jvillard

Differential Revision: D24746235

fbshipit-source-id: d8fcf46a1
---
 sledge/src/fol/arithmetic.ml      | 42 +++++++++++++++++++------------
 sledge/src/fol/arithmetic_intf.ml |  6 ++---
 2 files changed, 28 insertions(+), 20 deletions(-)

diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index 734ba63de..3cbce44d8 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -178,6 +178,15 @@ struct
         | _ -> Uninterpreted )
       | `Many -> Interpreted
 
+    let is_noninterpreted poly =
+      match Sum.only_elt poly with
+      | Some (mono, _) -> (
+        match Prod.classify mono with
+        | `Zero -> false
+        | `One (_, n) -> n <> 1
+        | `Many -> true )
+      | None -> false
+
     let get_const poly =
       match Sum.classify poly with
       | `Zero -> Some Q.zero
@@ -193,7 +202,6 @@ struct
     module CM = struct
       type t = Q.t * Prod.t
 
-      let one = (Q.one, Mono.one)
       let mul (c1, m1) (c2, m2) = (Q.mul c1 c2, Mono.mul m1 m2)
 
       (** Monomials [Mono.t] have [trm] indeterminates, which include, via
@@ -232,6 +240,12 @@ struct
         |> check invariant
     end
 
+    (** Embed a monomial into a term, flattening if possible *)
+    let trm_of_mono mono =
+      match Mono.get_trm mono with
+      | Some trm -> trm
+      | None -> Embed.to_trm (Sum.of_ mono Q.one)
+
     (** Embed a term into a polynomial, by projecting a polynomial out of
         the term if possible *)
     let trm trm =
@@ -272,21 +286,17 @@ struct
         ~call:(fun {pf} -> pf "%a" pp poly)
         ~retn:(fun {pf} -> pf "%a" pp)
       @@ fun () ->
-      let p, p' = (poly, Sum.empty) in
-      let p, p' =
-        Sum.fold poly (p, p') ~f:(fun mono coeff (p, p') ->
-            let m, cm' = (mono, CM.one) in
-            let m, cm' =
-              Prod.fold mono (m, cm') ~f:(fun trm power (m, cm') ->
-                  let trm' = f trm in
-                  if trm == trm' then (m, cm')
-                  else
-                    (Prod.remove trm m, CM.mul cm' (CM.of_trm trm' ~power)) )
-            in
-            ( Sum.remove mono p
-            , Sum.union p' (CM.to_poly (CM.mul (coeff, m) cm')) ) )
-      in
-      Sum.union p p' |> check invariant
+      ( if is_noninterpreted poly then poly
+      else
+        let p, p' =
+          Sum.fold poly (poly, Sum.empty) ~f:(fun mono coeff (p, p') ->
+              let e = trm_of_mono mono in
+              let e' = f e in
+              if e == e' then (p, p')
+              else (Sum.remove mono p, Sum.union p' (mulc coeff (trm e'))) )
+        in
+        Sum.union p p' )
+      |> check invariant
 
     (* traverse *)
 
diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
index f829b541f..50187ac9e 100644
--- a/sledge/src/fol/arithmetic_intf.ml
+++ b/sledge/src/fol/arithmetic_intf.ml
@@ -57,10 +57,8 @@ module type S = sig
       coefficients in [p] and [n] are non-negative. *)
 
   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ᵢⱼ]. *)
+  (** [map ~f a] is [a] with each maximal non-interpreted subterm
+      transformed by [f]. *)
 
   (** Traverse *)