[Pkg-ocaml-maint-commits] [ocplib-simplex] 01/07: New upstream version 0.4

Ralf Treinen treinen at moszumanska.debian.org
Wed Nov 15 07:45:44 UTC 2017


This is an automated email from the git hooks/post-receive script.

treinen pushed a commit to branch master
in repository ocplib-simplex.

commit d5f4309f6552e4ee207f211463f71508f1b48ecd
Author: Ralf Treinen <treinen at free.fr>
Date:   Tue Nov 14 21:32:03 2017 +0100

    New upstream version 0.4
---
 .ocplint             | 91 ++++++++++++++++++++++++++++++++++------------------
 CHANGES.md           |  8 +++++
 LICENSE              | 21 ++++++++++--
 Makefile.in          | 12 ++++---
 README.md            |  4 +--
 extra/TODO.txt       |  7 +++-
 opam                 |  5 +--
 src/assertBounds.ml  | 65 ++++++++++++++++++++-----------------
 src/assertBounds.mli |  8 +++--
 src/core.ml          | 37 +++++++++++++--------
 src/coreSig.mli      |  9 ++++--
 src/solveBounds.ml   |  3 ++
 src/version.ml       |  2 +-
 13 files changed, 181 insertions(+), 91 deletions(-)

diff --git a/.ocplint b/.ocplint
index 9c821ac..f271267 100644
--- a/.ocplint
+++ b/.ocplint
@@ -11,11 +11,18 @@
 
 
 (* Module to ignore during the lint. *)
-ignored_files = [
+ignore = [
+       tests
 ]
+
+(* Time before erasing cached results (in days). *)
+db_persistence = 1
+
+(* Number of parallel jobs *)
+jobs = 4
 plugin_typedtree = {
 
-(* A plugin with linters on typed tree. *)
+(* A plugin with linters on typed tree *)
   enabled = true
   fully_qualified_identifiers = {
 
@@ -23,7 +30,7 @@ plugin_typedtree = {
     enabled = true
 
 (* Module to ignore durint the lint of "Fully-Qualified Identifiers" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Fully-Qualified Identifiers" *)
@@ -41,7 +48,7 @@ plugin_typedtree = {
     enabled = true
 
 (* Module to ignore durint the lint of "Polymorphic function" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Polymorphic function" *)
@@ -50,7 +57,7 @@ plugin_typedtree = {
 }
 plugin_text = {
 
-(* A plugin with linters on the source. *)
+(* A plugin with linters on the source *)
   enabled = true
   code_length = {
 
@@ -58,7 +65,7 @@ plugin_text = {
     enabled = true
 
 (* Module to ignore durint the lint of "Code Length" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Code Length" *)
@@ -73,7 +80,7 @@ plugin_text = {
     enabled = true
 
 (* Module to ignore durint the lint of "Useless space character and empty line at the end of file." *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Useless space character and empty line at the end of file." *)
@@ -85,7 +92,7 @@ plugin_text = {
     enabled = true
 
 (* Module to ignore durint the lint of "Detect use of unwanted chars in files" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Detect use of unwanted chars in files" *)
@@ -96,34 +103,39 @@ plugin_patch = {
 
 (* Detect pattern with semantic patch. *)
   enabled = true
-  sempatch_lint_default = {
+  sempatch_lint = {
 
-(* Enable/Disable linter "Lint from semantic patches (default)". *)
+(* Enable/Disable linter "Lint from semantic patches.". *)
     enabled = true
 
-(* Module to ignore durint the lint of "Lint from semantic patches (default)" *)
-    ignored_files = [
+(* Module to ignore durint the lint of "Lint from semantic patches." *)
+    ignore = [
     ]
 
-(* Enable/Disable warnings from "Lint from semantic patches (default)" *)
+(* Enable/Disable warnings from "Lint from semantic patches." *)
     warnings = "+A"
   }
-  sempatch_lint_user_defined = {
+}
+plugin_parsing = {
 
-(* Enable/Disable linter "Lint from semantic patches (user defined).". *)
+(* Analyses requiring to re-parse the file *)
+  enabled = true
+  raw_syntax = {
+
+(* Enable/Disable linter "Raw Syntax". *)
     enabled = true
 
-(* Module to ignore durint the lint of "Lint from semantic patches (user defined)." *)
-    ignored_files = [
+(* Module to ignore durint the lint of "Raw Syntax" *)
+    ignore = [
     ]
 
-(* Enable/Disable warnings from "Lint from semantic patches (user defined)." *)
+(* Enable/Disable warnings from "Raw Syntax" *)
     warnings = "+A"
   }
 }
 plugin_parsetree = {
 
-(* A plugin with linters on parsetree. *)
+(* A plugin with linters on parsetree *)
   enabled = true
   code_identifier_length = {
 
@@ -131,7 +143,7 @@ plugin_parsetree = {
     enabled = true
 
 (* Module to ignore durint the lint of "Code Identifier Length" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Code Identifier Length" *)
@@ -149,7 +161,7 @@ plugin_parsetree = {
     enabled = true
 
 (* Module to ignore durint the lint of "List function on singleton" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "List function on singleton" *)
@@ -161,7 +173,7 @@ plugin_parsetree = {
     enabled = true
 
 (* Module to ignore durint the lint of "Physical comparison between allocated litterals." *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Physical comparison between allocated litterals." *)
@@ -173,7 +185,7 @@ plugin_parsetree = {
     enabled = true
 
 (* Module to ignore durint the lint of "Good Practices" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Good Practices" *)
@@ -185,16 +197,28 @@ plugin_parsetree = {
     enabled = true
 
 (* Module to ignore durint the lint of "Check Constructor Arguments" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Check Constructor Arguments" *)
     warnings = "+A"
   }
+  code_redefine_stdlib_module = {
+
+(* Enable/Disable linter "Refedine Stdlib Module". *)
+    enabled = true
+
+(* Module to ignore durint the lint of "Refedine Stdlib Module" *)
+    ignore = [
+    ]
+
+(* Enable/Disable warnings from "Refedine Stdlib Module" *)
+    warnings = "+A"
+  }
 }
 plugin_indent = {
 
-(* A plugin with linters on the source. *)
+(* A plugin with linters on the source *)
   enabled = true
   ocp_indent = {
 
@@ -202,7 +226,7 @@ plugin_indent = {
     enabled = true
 
 (* Module to ignore durint the lint of "Indention with ocp-indent" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Indention with ocp-indent" *)
@@ -211,7 +235,7 @@ plugin_indent = {
 }
 plugin_file_system = {
 
-(* A plugin with linters on file system like interface missing, etc. *)
+(* A plugin with linters on file system like interface missing, etc *)
   enabled = true
   interface_missing = {
 
@@ -219,7 +243,7 @@ plugin_file_system = {
     enabled = true
 
 (* Module to ignore durint the lint of "Missing interface" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Missing interface" *)
@@ -231,7 +255,7 @@ plugin_file_system = {
     enabled = true
 
 (* Module to ignore durint the lint of "File Names" *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "File Names" *)
@@ -240,7 +264,7 @@ plugin_file_system = {
 }
 plugin_complex = {
 
-(* A plugin with linters on different inputs. *)
+(* A plugin with linters on different inputs *)
   enabled = true
   interface_module_type_name = {
 
@@ -248,10 +272,15 @@ plugin_complex = {
     enabled = true
 
 (* Module to ignore durint the lint of "Checks on module type name." *)
-    ignored_files = [
+    ignore = [
     ]
 
 (* Enable/Disable warnings from "Checks on module type name." *)
     warnings = "+A"
   }
 }
+
+(*
+ The following options are not used (errors, obsolete, ...) 
+*)
+ignored_files = [ ]
diff --git a/CHANGES.md b/CHANGES.md
index ccde25c..b7564d9 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,13 @@
 (!!! = may break code that uses previous versions)
 
+version 0.4, August 22, 2017
+===============================
+
+* (!!!) Now, asserting bounds returns whether these bounds are
+  trivially implied by those that are already known
+
+* add a field nb_pivots in the environment to count the number of
+  pivots that have been made so far.
 
 verion 0.3, November 09, 2016
 ===============================
diff --git a/LICENSE b/LICENSE
index e809285..d1eb851 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,7 +1,22 @@
+In the following, ocplib-simplex refers to all files marked "Copyright
+OCamlPro" in this distribution.
+
 ocplib-simplex is distributed under the terms of the GNU Lesser
-General Public License (LGPL) version 2.1 (see below), with some
-exceptions as defined for the OCaml Core System (see
-https://github.com/ocaml/ocaml/blob/trunk/LICENSE)
+General Public License (LGPL) version 2.1 (included below).
+
+As a special exception to the GNU Lesser General Public License, you
+may link, statically or dynamically, a "work that uses ocplib-simplex"
+with a publicly distributed version of ocplib-simplex to produce an
+executable file containing portions of ocplib-simplex, and distribute
+that executable file under terms of your choice, without any of the
+additional requirements listed in clause 6 of the GNU Lesser General
+Public License. By "a publicly distributed version of ocplib-simplex",
+we mean either the unmodified ocplib-simplex as distributed by
+OCamlpro, or a modified version of ocplib-simplex that is distributed
+under the conditions defined in clause 2 of the GNU Lesser General
+Public License. This exception does not however invalidate any other
+reasons why the executable file might be covered by the GNU Lesser
+General Public License.
 
 ----------------------------------------------------------------------
 
diff --git a/Makefile.in b/Makefile.in
index 5ff1656..3c5cf07 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -13,11 +13,11 @@
 # (enclosed in the file LGPL).
 
 # where to install the binaries
-# DESTDIR=
+DESTDIR=@prefix@
 # prefix=@prefix@
 # exec_prefix=@exec_prefix@
 # BINDIR=$(DESTDIR)@bindir@
-# LIBDIR=$(DESTDIR)@libdir@/ocplib-simplex
+LIBDIR=$(DESTDIR)/lib/
 # DATADIR=$(DESTDIR)@datadir@/ocplib-simplex
 
 # where to install the man page
@@ -112,7 +112,8 @@ META: config.status
 ##############
 
 install: all META
-	ocamlfind install ocplib-simplex src/$(LIBNAME).* src/*.mli META
+	OCAMLFIND_DESTDIR=$(LIBDIR) \
+	  ocamlfind install ocplib-simplex src/$(LIBNAME).* src/*.mli META
 
 
 uninstall:
@@ -186,7 +187,7 @@ archi: depend
 
 
 lint:
-	ocp-lint --path /home/omig/Bureau/pro/alt-ergo/ocplib-simplex/src --disable-plugin-indent
+	ocp-lint --disable-plugin-indent --pwarning --perror
 
 edit:
 	emacs src/*ml* &
@@ -194,6 +195,9 @@ edit:
 opam-deps:
 	opam install ocamlfind
 
+opam-tests-deps:
+	opam install ocamlfind num
+
 repin:
 	opam remove ocplib-simplex
 	opam pin add . --y
diff --git a/README.md b/README.md
index 7c1d482..e94d40c 100644
--- a/README.md
+++ b/README.md
@@ -64,6 +64,4 @@ tracker.
 
 `ocplib-simplex` is Copyright (C) --- OCamlPro.  it is distributed
 under the terms of the GNU Lesser General Public License (LGPL)
-version 2.1 (see LICENSE file), with some exceptions as defined for
-the OCaml Core System (see
-https://github.com/ocaml/ocaml/blob/trunk/LICENSE).
\ No newline at end of file
+version 2.1 (see LICENSE file for more details).
\ No newline at end of file
diff --git a/extra/TODO.txt b/extra/TODO.txt
index 86877df..ce44fdf 100644
--- a/extra/TODO.txt
+++ b/extra/TODO.txt
@@ -4,7 +4,12 @@ global:
 - try some more heuristics to extract models for simplexes over ints.
 - add the ability to do some encoding (with a flag): (eg. cubes-test
 for LIA)
-- add optimization capabilities
+- add the ability to backtrack by directly relaxing bounds. This would
+allow to not rely on the functional style to backtrack, and to keep
+the pivots and valuation that have been computed so far
+
+- add the ability to apply substitutions resulting from pivots
+lazily. This is very important for scalability
 
 
 assertBounds.ml:
diff --git a/opam b/opam
index 5296d77..7496031 100644
--- a/opam
+++ b/opam
@@ -1,6 +1,6 @@
 opam-version: "1.2"
 name: "ocplib-simplex"
-version: "0.2+"
+version: "0.4"
 
 authors: "Mohamed Iguernlala <mohamed.iguernlala at ocamlpro.com>"
 maintainer: "Mohamed Iguernlala <mohamed.iguernlala at ocamlpro.com>"
@@ -14,7 +14,7 @@ dev-repo: "https://github.com/OCamlPro-Iguernlala/ocplib-simplex.git"
 
 build:[
         ["autoconf"]
-        ["./configure"]
+        ["./configure" "-prefix" "%{prefix}%"]
 	[make]
 ]
 
@@ -30,6 +30,7 @@ remove:[
 depends: [
   "ocamlfind" {build}
   "conf-autoconf" {build}
+  "num"
 ]
 
 available: [ ocaml-version >= "4.01.0" ]
\ No newline at end of file
diff --git a/src/assertBounds.ml b/src/assertBounds.ml
index 0999ad6..7b5b8b6 100644
--- a/src/assertBounds.ml
+++ b/src/assertBounds.ml
@@ -15,7 +15,7 @@ module type SIG = sig
     Core.Ex.t ->
     Core.bound ->
     Core.Ex.t ->
-    Core.t
+    Core.t * bool
 
   val poly :
     Core.t ->
@@ -25,7 +25,7 @@ module type SIG = sig
     Core.Ex.t ->
     Core.bound ->
     Core.Ex.t ->
-    Core.t
+    Core.t * bool
 
 end
 
@@ -50,18 +50,19 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
         if has_bad_value then UNK, SX.add s fixme else stt, fixme
 
     let assert_basic_var env x mini min_ex maxi max_ex =
-      let info, poly =
+      let info, poly, changed =
         try
           let info, poly = MX.find x env.basic in
-          let info = set_min_bound info mini min_ex in
-          let info = set_max_bound info maxi max_ex in
-          info, poly
+          let info, chang1 = set_min_bound info mini min_ex in
+          let info, chang2 = set_max_bound info maxi max_ex in
+          info, poly, chang1 || chang2
         with Not_found -> assert false
       in
       let status, fixme =
         new_status_basic env.status env.fixme x info (consistent_bounds info)
       in
-      {env with basic = MX.add x (info, poly) env.basic; status; fixme}
+      {env with basic = MX.add x (info, poly) env.basic; status; fixme},
+      changed
 
     (* *)
 
@@ -98,8 +99,8 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
         try MX.find x env.non_basic
         with Not_found -> empty_info, SX.empty
       in
-      let info = set_min_bound info mini min_ex in
-      let info = set_max_bound info maxi max_ex in
+      let info, chang1 = set_min_bound info mini min_ex in
+      let info, chang2 = set_max_bound info maxi max_ex in
       let old_val = info.value in
       let info, changed = ajust_value_of_non_basic info in
       let status, fixme = new_status_non_basic x env.status env.fixme info in
@@ -107,15 +108,17 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
         {env with
           non_basic = MX.add x (info, use) env.non_basic; status; fixme}
       in
-      if not changed then env
-      else adapt_values_of_basic_vars env old_val info.value x use
-
+      let env =
+        if not changed then env
+        else adapt_values_of_basic_vars env old_val info.value x use
+      in
+      env, chang1 || chang2
 
     (* exported function: check_invariants called before and after *)
     let var env x mini ex_min maxi ex_max =
       debug "[entry of assert_var]" env (Result.get None);
       check_invariants env (Result.get None);
-      let env =
+      let env, changed =
         if MX.mem x env.basic then
           assert_basic_var env x mini ex_min maxi ex_max
         else
@@ -123,7 +126,7 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
       in
       debug "[exit of assert_var]" env (Result.get None);
       check_invariants env (Result.get None);
-      env
+      env, changed
 
     let register_slake slk p env =
       if MX.mem slk env.slake then env, false
@@ -172,8 +175,9 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
 
             with Not_found ->
               (* var not initied -> new non_basic *)
-              let env =
+              let env, chang =
                 assert_non_basic_var env x None Ex.empty None Ex.empty in
+              assert (not chang);
               let new_q, x_status = P.replace x c q in
               assert (x_status == P.New);
               let info, use =
@@ -193,7 +197,7 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
       check_invariants env (Result.get None);
       assert (P.is_polynomial p);
       let env, is_fresh = register_slake slk p env in
-      let info, is_basic, env =
+      let info, is_basic, env, change =
         try (* non basic existing var ? *)
           let info, use = MX.find slk env.non_basic in
           assert (
@@ -201,17 +205,18 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
             let zp, _ = P.accumulate slk R.m_one np in
             P.is_empty zp
           );
-          let info = set_min_bound info mini min_ex in
-          let info = set_max_bound info maxi max_ex in
+          let info, chang1 = set_min_bound info mini min_ex in
+          let info, chang2 = set_max_bound info maxi max_ex in
           let old_val = info.value in
           let info, changed = ajust_value_of_non_basic info in
           let env =
             {env with non_basic = MX.add slk (info, use) env.non_basic}
           in
-          info, false,
-          if not changed then env
-          else adapt_values_of_basic_vars env old_val info.value slk use
-
+          let env =
+            if not changed then env
+            else adapt_values_of_basic_vars env old_val info.value slk use
+          in
+          info, false, env, chang1 || chang2
         with Not_found ->
           try (* basic existing var ? *)
             let info, poly = MX.find slk env.basic in
@@ -219,17 +224,19 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
               let np, _ = normalize_polynomial is_fresh slk p env in
               P.equal np poly
             );
-            let info = set_min_bound info mini min_ex in
-            let info = set_max_bound info maxi max_ex in
-            info, true, {env with basic = MX.add slk (info, poly) env.basic}
+            let info, chang1 = set_min_bound info mini min_ex in
+            let info, chang2 = set_max_bound info maxi max_ex in
+            info, true, {env with basic = MX.add slk (info, poly) env.basic},
+            chang1 || chang2
 
           with Not_found -> (* fresh basic var *)
             assert (is_fresh);
             let np, env = normalize_polynomial is_fresh slk p env in
             let info = {empty_info with value = evaluate_poly env np} in
-            let info = set_min_bound info mini min_ex in
-            let info = set_max_bound info maxi max_ex in
-            info, true, {env with basic = MX.add slk (info, np) env.basic}
+            let info, chang1 = set_min_bound info mini min_ex in
+            let info, chang2 = set_max_bound info maxi max_ex in
+            info, true, {env with basic = MX.add slk (info, np) env.basic},
+            chang1 || chang2
       in
       let status, fixme =
         if is_basic then
@@ -241,7 +248,7 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
       let env = {env with status; fixme } in
       debug "[exit of assert_poly]" env (Result.get None);
       check_invariants env (Result.get None);
-      env
+      env, change
 
 
   end
diff --git a/src/assertBounds.mli b/src/assertBounds.mli
index 36fa055..6f31f92 100644
--- a/src/assertBounds.mli
+++ b/src/assertBounds.mli
@@ -8,6 +8,8 @@ module type SIG = sig
 
   module Core : CoreSig.SIG
 
+  (* The returned bool is true if the asserted bounds are not trivial
+     (i.e. not implied by known bounds) *)
   val var :
     Core.t ->
     Core.Var.t ->
@@ -15,8 +17,10 @@ module type SIG = sig
     Core.Ex.t ->
     Core.bound ->
     Core.Ex.t ->
-    Core.t
+    Core.t * bool
 
+  (* The returned bool is true if the asserted bounds are not trivial
+     (i.e. not implied by known bounds) *)
   val poly :
     Core.t ->
     Core.P.t ->
@@ -25,7 +29,7 @@ module type SIG = sig
     Core.Ex.t ->
     Core.bound ->
     Core.Ex.t ->
-    Core.t
+    Core.t * bool
 
 end
 
diff --git a/src/core.ml b/src/core.ml
index 7d569a4..1814f7b 100644
--- a/src/core.ml
+++ b/src/core.ml
@@ -70,6 +70,7 @@ module Make
         status    : simplex_status;
         debug     : int;
         check_invs: bool;
+        nb_pivots : int ref;
       }
 
     let empty_info =
@@ -92,7 +93,8 @@ module Make
         status    = UNK;
         is_int;
         check_invs;
-        debug
+        debug;
+        nb_pivots = ref 0
       }
 
     let on_integers env = env.is_int
@@ -121,27 +123,36 @@ module Make
 
     let set_min_bound info bnd ex =
       match bnd with
-      | None -> info
+      | None -> info, false
       | Some _new ->
-        if violates_min_bound _new info.mini then info
+        let mini = info.mini in
+        if violates_min_bound _new mini || equals_optimum _new mini then
+          info, false
         else
           let empty_dom = not (consistent_bounds_aux bnd info.maxi) in
-          if violates_min_bound info.value bnd then
-            {info with mini = bnd; min_ex = ex; vstatus = LowerKO; empty_dom}
-          else
-            {info with mini = bnd; min_ex = ex; empty_dom}
+          let i' =
+            if violates_min_bound info.value bnd then
+              {info with mini = bnd; min_ex = ex; vstatus = LowerKO; empty_dom}
+            else
+              {info with mini = bnd; min_ex = ex; empty_dom}
+          in i', true
 
     let set_max_bound info bnd ex =
       match bnd with
-      | None -> info
+      | None -> info, false
       | Some _new ->
-        if violates_max_bound _new info.maxi then info
+        let maxi = info.maxi in
+        if violates_max_bound _new maxi || equals_optimum _new maxi then
+          info, false
         else
           let empty_dom = not (consistent_bounds_aux info.mini bnd) in
-          if violates_max_bound info.value bnd then
-            {info with maxi = bnd; max_ex = ex; vstatus = UpperKO; empty_dom}
-          else
-            {info with maxi = bnd; max_ex = ex; empty_dom}
+          let i' =
+            if violates_max_bound info.value bnd then
+              {info with maxi = bnd; max_ex = ex; vstatus = UpperKO; empty_dom}
+            else
+              {info with maxi = bnd; max_ex = ex; empty_dom}
+          in
+          i', true
 
     let ajust_value_of_non_basic info =
       if info.empty_dom then begin
diff --git a/src/coreSig.mli b/src/coreSig.mli
index 6d6816b..7f0d0d0 100644
--- a/src/coreSig.mli
+++ b/src/coreSig.mli
@@ -63,6 +63,7 @@ module type SIG = sig
       status    : simplex_status;
       debug     : int;
       check_invs: bool;
+      nb_pivots : int ref;
     }
 
   val empty_info : var_info
@@ -79,9 +80,13 @@ module type SIG = sig
 
   val violates_max_bound : R2.t -> bound -> bool
 
-  val set_min_bound : var_info -> bound -> Ex.t -> var_info
+  (* The returned bool is true if the asserted bounds are not trivial
+     (i.e. not implied by known bounds) *)
+  val set_min_bound : var_info -> bound -> Ex.t -> var_info * bool
 
-  val set_max_bound : var_info -> bound -> Ex.t -> var_info
+  (* The returned bool is true if the asserted bounds are not trivial
+     (i.e. not implied by known bounds) *)
+  val set_max_bound : var_info -> bound -> Ex.t -> var_info * bool
 
   (* vstatus is supposed to be well set *)
   val ajust_value_of_non_basic: var_info -> var_info * bool
diff --git a/src/solveBounds.ml b/src/solveBounds.ml
index 216c435..ed3dea5 100644
--- a/src/solveBounds.ml
+++ b/src/solveBounds.ml
@@ -163,6 +163,7 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
         (* ... *)
 
         let env = {env with fixme; basic; non_basic} in
+        env.nb_pivots := !(env.nb_pivots) + 1;
         solve_rec env (round + 1)
 
 
@@ -340,6 +341,7 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
               update_valuation_without_pivot
                 env _x _use_x new_xi diff _should_incr, opt
             in
+            (* no pivot *)
             maximize_rec env opt (rnd + 1)
           | None ->
             if env.debug > 1 then
@@ -455,6 +457,7 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
 
 
         in
+        env.nb_pivots := !(env.nb_pivots) + 1;
         maximize_rec env opt (rnd + 1)
 
 
diff --git a/src/version.ml b/src/version.ml
index 3912526..faed81a 100644
--- a/src/version.ml
+++ b/src/version.ml
@@ -4,4 +4,4 @@
 (* Copyright (C) --- OCamlPro --- See README.md for information and licensing *)
 (******************************************************************************)
 
-let version="0.3"
+let version="0.4"

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/ocplib-simplex.git



More information about the Pkg-ocaml-maint-commits mailing list