[sledge] Fix Arith.trms to include proper subterms of uninterpreted terms

Summary:
For arithmetic terms that are a single monomial, Arith.trms is
currently the singleton iterator containing the term itself. In
particular, Arith.trms is not the *sub*terms in this case. In this
case the principal constructor is multiplication. This diff fixes
these cases and defines Arith.trms to contain the factors of a
singleton monomial.

Reviewed By: jvillard

Differential Revision: D25883719

fbshipit-source-id: a88611bba

sledge/src/fol/arithmetic.ml

@@ -298,7 +298,10 @@ struct
           Sum.iter poly ~f:(fun mono _ ->
               if not (Mono.equal_one mono) then f mono ) )
 
-    let trms poly = Iter.flat_map ~f:Mono.trms (monos poly)
+    let trms poly =
+      match get_mono poly with
+      | Some mono -> Mono.trms mono
+      | None -> Iter.map ~f:trm_of_mono (monos poly)
 
     let map poly ~f =
       [%trace]

sledge/src/fol/arithmetic_intf.ml

@@ -59,7 +59,13 @@ module type S = sig
   (** Traverse *)
 
   val trms : t -> trm iter
-  (** [trms a] enumerates the indeterminate terms appearing in [a] *)
+  (** [trms a] is the maximal foreign or noninterpreted proper subterms of
+      [a]. Considering an arithmetic term as a polynomial,
+      [trms (c × (Σᵢ₌₁ⁿ cᵢ × Πⱼ₌₁ᵐᵢ
+      Xᵢⱼ^pᵢⱼ))] is the sequence of monomials
+      [Πⱼ₌₁ᵐᵢ Xᵢⱼ^pᵢⱼ] for each [i]. If the arithmetic
+      term is a monomial, [trms (Πⱼ₌₁ᵐ Xⱼ^pⱼ)] is the sequence
+      of factors [Xⱼ] for each [j]. *)
 
   val map : t -> f:(trm -> trm) -> t
   (** [map ~f a] is [a] with each maximal non-interpreted subterm