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 <trei...@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.iguernl...@ocamlpro.com>" maintainer: "Mohamed Iguernlala <mohamed.iguernl...@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 _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits