From af58e744a250a12e21b3299e3554d104e8a43d9c Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:34:23 -0800 Subject: [PATCH] [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 | 5 ++++- sledge/src/fol/arithmetic_intf.ml | 8 +++++++- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml index 9edf08f68..5110eab19 100644 --- a/sledge/src/fol/arithmetic.ml +++ b/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] diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml index 0c768d13a..9bd81cc6a 100644 --- a/sledge/src/fol/arithmetic_intf.ml +++ b/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