From bffcaf4fe7ddf6cbe8eed7c22120fe2b890f5c53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Thu, 6 Jun 2024 17:25:48 +0200 Subject: [PATCH] Do not assert in user code Instead of triggering an [assert false], the [poly] function now raises [Invalid_argument] when provided with a polynomial that has only one variable. Fixes #33 --- src/assertBounds.ml | 10 ++++++++++ src/assertBounds.mli | 16 ++++++++++++---- 2 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/assertBounds.ml b/src/assertBounds.ml index 6e1d9ae..c985cab 100644 --- a/src/assertBounds.ml +++ b/src/assertBounds.ml @@ -219,6 +219,16 @@ module Make(Core : CoreSig.S) : S with module Core = Core = struct let poly env p ?min ?max slk = debug "[entry of assert_poly]" env (Result.get None); check_invariants env (Result.get None); + (* Note: we should not convert the call to [poly] into a call to [var] + here because we introduce the equality [poly = slk] and then we set + the bounds for [slk] to [min] and [max]. + + If there is a single variable (i.e. [poly = k * x] for some + coefficient [k] and variable [x]), we do not want to add the useless + slack variable [slk = k * x]. *) + if not (P.is_polynomial p) then + invalid_arg + "poly: must have two variables or more, use var instead"; assert (P.is_polynomial p); let mini = update_min_bound env min in let maxi = update_max_bound env max in diff --git a/src/assertBounds.mli b/src/assertBounds.mli index 5e7d428..177fea3 100644 --- a/src/assertBounds.mli +++ b/src/assertBounds.mli @@ -22,13 +22,21 @@ module type S = sig Core.Var.t -> Core.t * bool - (* The returned bool is [true] if the asserted bounds are not trivial - (i.e. not implied by known bounds) *) (** [poly env poly min max x] returns a new environment obtained by changing the bounds of [poly] in [env] to [min] and [max]. The polynomial is represented by the slack variable [x]. - If the bounds were implied by other known bounds (in other words, if the - environment did not change) the associated boolean will be [false]. + + [poly] must be a polynomial (as tested by [Core.P.is_polynomial]), that + is, it must contain at least two distinct variables. Use [var] instead + for constraints that apply to a single variable. + + The returned bool is [true] if the asserted bounds are not trivial (i.e. + not implied by known bounds). If the bounds were implied by other known + bounds (in other words, if the environment did not change) the associated + boolean will be [false]. + + @raise Invalid_argument if [poly] contains zero or one variables (use [var] + to add constraints to a single variable). *) val poly : Core.t ->