Apache-License-2.0.txt

+
+                                 Apache License
+                           Version 2.0, January 2004
+                        http://www.apache.org/licenses/
+
+   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+   1. Definitions.
+
+      "License" shall mean the terms and conditions for use, reproduction,
+      and distribution as defined by Sections 1 through 9 of this document.
+
+      "Licensor" shall mean the copyright owner or entity authorized by
+      the copyright owner that is granting the License.
+
+      "Legal Entity" shall mean the union of the acting entity and all
+      other entities that control, are controlled by, or are under common
+      control with that entity. For the purposes of this definition,
+      "control" means (i) the power, direct or indirect, to cause the
+      direction or management of such entity, whether by contract or
+      otherwise, or (ii) ownership of fifty percent (50%) or more of the
+      outstanding shares, or (iii) beneficial ownership of such entity.
+
+      "You" (or "Your") shall mean an individual or Legal Entity
+      exercising permissions granted by this License.
+
+      "Source" form shall mean the preferred form for making modifications,
+      including but not limited to software source code, documentation
+      source, and configuration files.
+
+      "Object" form shall mean any form resulting from mechanical
+      transformation or translation of a Source form, including but
+      not limited to compiled object code, generated documentation,
+      and conversions to other media types.
+
+      "Work" shall mean the work of authorship, whether in Source or
+      Object form, made available under the License, as indicated by a
+      copyright notice that is included in or attached to the work
+      (an example is provided in the Appendix below).
+
+      "Derivative Works" shall mean any work, whether in Source or Object
+      form, that is based on (or derived from) the Work and for which the
+      editorial revisions, annotations, elaborations, or other modifications
+      represent, as a whole, an original work of authorship. For the purposes
+      of this License, Derivative Works shall not include works that remain
+      separable from, or merely link (or bind by name) to the interfaces of,
+      the Work and Derivative Works thereof.
+
+      "Contribution" shall mean any work of authorship, including
+      the original version of the Work and any modifications or additions
+      to that Work or Derivative Works thereof, that is intentionally
+      submitted to Licensor for inclusion in the Work by the copyright owner
+      or by an individual or Legal Entity authorized to submit on behalf of
+      the copyright owner. For the purposes of this definition, "submitted"
+      means any form of electronic, verbal, or written communication sent
+      to the Licensor or its representatives, including but not limited to
+      communication on electronic mailing lists, source code control systems,
+      and issue tracking systems that are managed by, or on behalf of, the
+      Licensor for the purpose of discussing and improving the Work, but
+      excluding communication that is conspicuously marked or otherwise
+      designated in writing by the copyright owner as "Not a Contribution."
+
+      "Contributor" shall mean Licensor and any individual or Legal Entity
+      on behalf of whom a Contribution has been received by Licensor and
+      subsequently incorporated within the Work.
+
+   2. Grant of Copyright License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      copyright license to reproduce, prepare Derivative Works of,
+      publicly display, publicly perform, sublicense, and distribute the
+      Work and such Derivative Works in Source or Object form.
+
+   3. Grant of Patent License. Subject to the terms and conditions of
+      this License, each Contributor hereby grants to You a perpetual,
+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+      (except as stated in this section) patent license to make, have made,
+      use, offer to sell, sell, import, and otherwise transfer the Work,
+      where such license applies only to those patent claims licensable
+      by such Contributor that are necessarily infringed by their
+      Contribution(s) alone or by combination of their Contribution(s)
+      with the Work to which such Contribution(s) was submitted. If You
+      institute patent litigation against any entity (including a
+      cross-claim or counterclaim in a lawsuit) alleging that the Work
+      or a Contribution incorporated within the Work constitutes direct
+      or contributory patent infringement, then any patent licenses
+      granted to You under this License for that Work shall terminate
+      as of the date such litigation is filed.
+
+   4. Redistribution. You may reproduce and distribute copies of the
+      Work or Derivative Works thereof in any medium, with or without
+      modifications, and in Source or Object form, provided that You
+      meet the following conditions:
+
+      (a) You must give any other recipients of the Work or
+          Derivative Works a copy of this License; and
+
+      (b) You must cause any modified files to carry prominent notices
+          stating that You changed the files; and
+
+      (c) You must retain, in the Source form of any Derivative Works
+          that You distribute, all copyright, patent, trademark, and
+          attribution notices from the Source form of the Work,
+          excluding those notices that do not pertain to any part of
+          the Derivative Works; and
+
+      (d) If the Work includes a "NOTICE" text file as part of its
+          distribution, then any Derivative Works that You distribute must
+          include a readable copy of the attribution notices contained
+          within such NOTICE file, excluding those notices that do not
+          pertain to any part of the Derivative Works, in at least one
+          of the following places: within a NOTICE text file distributed
+          as part of the Derivative Works; within the Source form or
+          documentation, if provided along with the Derivative Works; or,
+          within a display generated by the Derivative Works, if and
+          wherever such third-party notices normally appear. The contents
+          of the NOTICE file are for informational purposes only and
+          do not modify the License. You may add Your own attribution
+          notices within Derivative Works that You distribute, alongside
+          or as an addendum to the NOTICE text from the Work, provided
+          that such additional attribution notices cannot be construed
+          as modifying the License.
+
+      You may add Your own copyright statement to Your modifications and
+      may provide additional or different license terms and conditions
+      for use, reproduction, or distribution of Your modifications, or
+      for any such Derivative Works as a whole, provided Your use,
+      reproduction, and distribution of the Work otherwise complies with
+      the conditions stated in this License.
+
+   5. Submission of Contributions. Unless You explicitly state otherwise,
+      any Contribution intentionally submitted for inclusion in the Work
+      by You to the Licensor shall be under the terms and conditions of
+      this License, without any additional terms or conditions.
+      Notwithstanding the above, nothing herein shall supersede or modify
+      the terms of any separate license agreement you may have executed
+      with Licensor regarding such Contributions.
+
+   6. Trademarks. This License does not grant permission to use the trade
+      names, trademarks, service marks, or product names of the Licensor,
+      except as required for reasonable and customary use in describing the
+      origin of the Work and reproducing the content of the NOTICE file.
+
+   7. Disclaimer of Warranty. Unless required by applicable law or
+      agreed to in writing, Licensor provides the Work (and each
+      Contributor provides its Contributions) on an "AS IS" BASIS,
+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+      implied, including, without limitation, any warranties or conditions
+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+      PARTICULAR PURPOSE. You are solely responsible for determining the
+      appropriateness of using or redistributing the Work and assume any
+      risks associated with Your exercise of permissions under this License.
+
+   8. Limitation of Liability. In no event and under no legal theory,
+      whether in tort (including negligence), contract, or otherwise,
+      unless required by applicable law (such as deliberate and grossly
+      negligent acts) or agreed to in writing, shall any Contributor be
+      liable to You for damages, including any direct, indirect, special,
+      incidental, or consequential damages of any character arising as a
+      result of this License or out of the use or inability to use the
+      Work (including but not limited to damages for loss of goodwill,
+      work stoppage, computer failure or malfunction, or any and all
+      other commercial damages or losses), even if such Contributor
+      has been advised of the possibility of such damages.
+
+   9. Accepting Warranty or Additional Liability. While redistributing
+      the Work or Derivative Works thereof, You may choose to offer,
+      and charge a fee for, acceptance of support, warranty, indemnity,
+      or other liability obligations and/or rights consistent with this
+      License. However, in accepting such obligations, You may act only
+      on Your own behalf and on Your sole responsibility, not on behalf
+      of any other Contributor, and only if You agree to indemnify,
+      defend, and hold each Contributor harmless for any liability
+      incurred by, or claims asserted against, such Contributor by reason
+      of your accepting any such warranty or additional liability.
+
+   END OF TERMS AND CONDITIONS
+
+   APPENDIX: How to apply the Apache License to your work.
+
+      To apply the Apache License to your work, attach the following
+      boilerplate notice, with the fields enclosed by brackets "[]"
+      replaced with your own identifying information. (Don't include
+      the brackets!)  The text should be enclosed in the appropriate
+      comment syntax for the file format. We also recommend that a
+      file or class name and description of purpose be included on the
+      same "printed page" as the copyright notice for easier
+      identification within third-party archives.
+
+   Copyright [yyyy] [name of copyright owner]
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.

CHANGES

+version 2.0.0-free, February 13, 2019
+=====================================
+
+* same as 2.0.0, except that "OCamlPro Non-Commercial Purpose License"
+is replaced with "Apache Software License version 2.0"
+
+
+version 2.0.0, November 14, 2017
+================================
+
+* integration of floating-point arithmetic reasoning: this is done via
+  the support of the rounding operator as done in the Gappa tool. FPA
+  reasoning can be enabled by calling Alt-Ergo as follows:
+
+  alt-ergo -use-fpa -prelude fpa-theory-2017-01-04-16h00.why file.why
+
+  where fpa-theory-2017-01-04-16h00.why is a prelude distributed with
+  Alt-Ergo. More details about the integration are given in this
+  paper: https://hal.inria.fr/hal-01522770, and dditional benchmarks
+  can be found here:
+  https://gitlab.com/OCamlPro-Iguernlala/Three-Tier-FPA-Benchs
+
+* a new lightweight reasoning step before SAT solving that enables a
+  kind of backward reasoning/goal unfolding (can be disabled with
+  option -no-backward)
+
+* integration of a simple cache mechanism for unit facts in the SAT
+  (learnt clauses, assumed facts, instances, theory deductions, ...)
+  to improve BCP (can be disabled with option -no-sat-learning)
+
+* the code of the profiler is now integrated in Alt-Ergo and is
+  statically linked
+
+* deep code refactoring. In particular, one can easily build an
+  Alt-Ergo library or define/register a new parser
+
+* add the ability to parse preludes with -prelude <prelude_1.why> ...
+  -prelude <prelude_n.why>
+
+* add the ability to disable weak pointers in hash-consing module
+  using option -disable-weaks (useful for more determinism)
+
+* GUI: goals are now shown in positive form
+
+* bugfix related to -timelimit option (use of ITIMER_VIRTUAL instead
+  of ITIMER_REAL except for the GUI)
+
+* bugfix in UF related to normalization of terms in presence of AC
+  symbols
+
+* new options -no-decisions and -no-fm to disable decisions in the SAT
+  and the Fourier-Motzkin algorithm, respectively
+
+* new improvements and heuristics in the SAT, terms, formulas,
+  congruence closure, profiler, ...
+
+* update licensing: most files are now licensed under the terms of the
+  Apache license v2. Some recent OCamlPro additions are licensed under
+  the terms of the OCamlPro Non-Commercial Purpose License v1
+
 version 1.30, November 21, 2016
 ==============================
 

COPYING.md

-## Copyright
-
+See LICENSE.md
\ No newline at end of file
-These software are distributed in the hope that they will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
-
-The resources are licensed as follows:
-
-### The "non-free" Directory
-
-Tools and plugins provided in the "non-free" directory are licensed
-under a Non-Commercial License. You are NOT allowed to redistribute
-them, to distribute the binaries resulting from their compilation, to
-modify the licensing, or to use them/the binaries for a commercial
-purpose without an approval from OCamlPro. See
-non-free/Non-Commercial-License.pdf for more details.
-
-### The Other Resources
-
-The other resources of this software are provided under the CeCILL-C
-(version 1) license. You can redistribute and/or modify them under the
-terms of the CeCILL-C FREE SOFTWARE LICENSE AGREEMENT. See enclosed
-CeCILL-C for more details.
-
-Please, do not use enclosed software until you have read and
-accepted the terms of the licensing above. The use of these
-software implies that you automatically agree with our terms and
-conditions.
\ No newline at end of file

INSTALL.md

 ## Build and Installation
 
-  You need OCaml >= 4.01.0, zarith, camlzip and ocplib-simplex >= 0.3
+  You need OCaml >= 4.04.0, zarith, camlzip, menhir and ocplib-simplex >= 0.4
   to compile the sources. You need LablGtk2 and the widget
   GSourceView2 to compile the GUI. You may need superuser permissions
   to perform the installation.
@@ -8,37 +8,40 @@
 #### Common Steps
 
   1. If a configure file is not distributed with the sources, then
-  execute "autoconf"
+  run "autoconf"
 
-  2. Configure with "./configure" to generate a Makefile
+  2. Configure with "./configure" to generate Makefile.configurable
 
   3. Alternatively, you can configure with "./configure -prefix
   some-absolute-path-prefix" to add a prefix for installation
-  directories You may also want to use "make show-dest-dirs" to see
+  directories. You may also want to use "make show-dest-dirs" to see
   directories where things will be installed.
 
 The steps below will build and install native or bytecode binaries
 depending on whether ocamlopt is installed or only ocamlc is detected.
 
-#### Alt-Ergo
+#### Everything (binaries, plugins, ...)
 
   1. Compile with "make"
 
   2. Install with "make install"
  
-#### AltGr-Ergo
+  3. Uninstall with "make uninstall"
 
-  1. Compile with "make gui"
+#### Alt-Ergo binary
 
-  2. Install with "make install-gui"
+  1. Compile with "make alt-ergo"
+
+  2. Install with "make install-ae"
  
-#### The Ctrl-Alt-Ergo wrapper
+#### AltGr-Ergo binary
+
+  1. Compile with "make gui"
   
-   - Compile with "make cae"
+  2. Install with "make install-gui"
 
-   - Install with "make install-cae"
 
-The steps below will build and install OCamlPro plugins (extension
+The steps below will build and install additional plugins (extension
 .cmxs if ocamlopt is installed or .cma if only ocamlc is detected).
 
 #### The SatML Plugin
@@ -53,13 +56,9 @@ The steps below will build and install OCamlPro plugins (extension
 
   2. Install with "make install-fm-simplex"
 
+#### The profiler plugin
 
-#### The Profiler Plugin
-
-  1. Compile with "make profiler"
-
-  2. Install with "make install-profiler"
-
+This plugin has been "inlined" in Alt-Ergo sources.
 
 ## Usage
 
@@ -76,7 +75,7 @@ The steps below will build and install OCamlPro plugins (extension
 
    Alt-Ergo will try to load a local plugin called
    "satML-plugin.cmxs". If this fails, Alt-Ergo tries to load it from
-   the default plugins directory (execute "alt-ergo -where plugins" to
+   the default plugins directory (run "alt-ergo -where plugins" to
    see its absolute path). You can also provide a relative or an
    absolute path as shown by the second command above. Also, you
    should replace ".cmxs" by ".cma" if you are working with bytcode
@@ -88,41 +87,25 @@ The steps below will build and install OCamlPro plugins (extension
         $ alt-ergo -inequalities-plugin some-path/fm-simplex-plugin.cmxs [other-options] file.why
 
    Alt-Ergo will try to load a local plugin called
-   "fm-simplex-plugin.cmxs". If this fails, Alt-Ergo tries to load it from
-   the default plugins directory (execute "alt-ergo -where plugins" to
-   see its absolute path). You can also provide a relative or an
+   "fm-simplex-plugin.cmxs". If this fails, Alt-Ergo tries to load it
+   from the default plugins directory (run "alt-ergo -where plugins"
+   to see its absolute path). You can also provide a relative or an
    absolute path as shown by the second command above. Also, you
    should replace ".cmxs" by ".cma" if you are working with bytcode
    binaries.
 
-- The profiler plugin can be used as follows:
-
-        $ alt-ergo -profiling 1. -profiling-plugin profiler-plugin.cmxs [other-options] file.why
-        $ alt-ergo -profiling 1. -profiling-plugin some-path/profiler-plugin.cmxs [other-options] file.why
-
-   Alt-Ergo will try to load a local plugin called
-   "profiler-plugin.cmxs". If this fails, Alt-Ergo tries to load it from
-   the default plugins directory (execute "alt-ergo -where plugins" to
-   see its absolute path). You can also provide a relative or an
-   absolute path as shown by the second command above. Also, you
-   should replace ".cmxs" by ".cma" if you are working with bytcode
-   binaries.
-
-- Ctrl-Alt-Ergo can be executed as shown below:
-
-        $ ctrl-alt-ergo "timeout" "sat-plugin" "alt-ergo" [options to alt-ergo]
+- Preludes can be passed to Alt-Ergo as follows:
 
-  1. "timeout" should be a positive integer. It will be divided by the
-  number of strategies that Alt-Ergo will try. 
+        $ alt-ergo -prelude p.why -prelude some-path/q.why [other-options] file.why
 
-  2. "sat-plugin" should be substituted with the external SAT plugin
-  you would like to load (typically satML-plugin.cmxs), or you can
-  replace it with "" to deactivate strategies that use external SAT
-  solvers.
+   Alt-Ergo will try to load a local plugin called "p.why". If this
+   fails, Alt-Ergo tries to load it from the default preludes
+   directory (run "alt-ergo -where preludes" to see its absolute
+   path). You can also provide a relative or an absolute path as shown
+   by "some-path/q.why".
 
-  3. "alt-ergo" should be substituted with the binary you would like
-  to use for Alt-Ergo (typically alt-ergo, if you have already
-  installed it).
+   For instance, the following command-line enables floating-point
+   arithmetic reasoning in Alt-Ergo and indicates that the FPA prelude
+   should be loaded:
 
-  4. [options to alt-ergo] should contain the arguments that will be
-   passed to Alt-Ergo (input file, options, ...)
+   $ alt-ergo -use-fpa -prelude fpa-theory-2017-01-04-16h00.why <file.why>

LICENSE.md

+## Copyright
+
+These software are distributed in the hope that they will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+
+Please, do not use enclosed software until you have read and accepted
+the terms of the licensing below. The use of these software implies
+that you automatically agree with our terms and conditions. In case of
+doubt, please contact us to clarify licensing.
+
+The resources are licensed as follows:
+
+### OCaml source files and Alt-Ergo preludes
+
+Some of these files are Copyright (C) 2006-2013 --- CNRS - INRIA -
+Universite Paris Sud, and Copyright (C) 2013-2017 --- OCamlPro SAS.
+They are distributed under the terms of the Apache Software License
+version 2.0.
+
+The other files are Copyright (C) --- OCamlPro SAS. They are
+distributed under the terms of the license indicated in the file
+'License.OCamlPro'.
+
+You may want to refer to the header of each file to know under which
+license it is distributed.
+
+
+### Binaries generated from the source files
+
+The binaries (tools, plugins, ...) that are generated from the OCaml
+source files are Copyright (C) --- OCamlPro SAS. They are distributed
+under the terms of the license indicated in the file
+'License.OCamlPro'.

License.OCamlPro

+Files referring to the license indicated in this file are licensed
+under the terms of the Apache Software License version 2.0 (see
+Apache-License-2.0.txt file).

Makefile.configurable.in

-#****************************************************************************#
-#     The Alt-Ergo theorem prover                                            #
-#     Copyright (C) 2006-2013                                                #
-#     CNRS - INRIA - Universite Paris Sud                                    #
-#                                                                            #
-#     Sylvain Conchon                                                        #
-#     Evelyne Contejean                                                      #
-#                                                                            #
-#     Francois Bobot                                                         #
-#     Mohamed Iguernelala                                                    #
-#     Stephane Lescuyer                                                      #
-#     Alain Mebsout                                                          #
-#                                                                            #
-#   This file is distributed under the terms of the CeCILL-C licence         #
-#****************************************************************************#
-
 
 # sample Makefile for Objective Caml
 # Copyright (C) 2001 Jean-Christophe FILLIATRE
@@ -36,6 +20,7 @@ exec_prefix=@exec_prefix@
 BINDIR=$(DESTDIR)@bindir@
 LIBDIR=$(DESTDIR)@libdir@/alt-ergo
 PLUGINSDIR=$(LIBDIR)/plugins
+PRELUDESDIR=$(LIBDIR)/preludes
 DATADIR=$(DESTDIR)@datadir@/alt-ergo
 
 # where to install the man page
@@ -46,7 +31,8 @@ OCAMLC   = @OCAMLC@
 OCAMLOPT = @OCAMLOPT@
 OCAMLDEP = @OCAMLDEP@
 OCAMLLEX = @OCAMLLEX@
-OCAMLYACC= @OCAMLYACC@
+#OCAMLYACC= @OCAMLYACC@
+MENHIR= @MENHIR@
 OCAMLBEST = @OCAMLBEST@
 OCAMLVERSION = @OCAMLVERSION@
 OCAMLWIN32 = @OCAMLWIN32@

Makefile.developers

+COMMIT_ID = $(shell git log -1 | grep commit | cut -d " " -f 2)
+
+edit: 
+	emacs lib/*/*ml* tools/text/*.ml* tools/gui/*.ml* parsers/*/*.ml* plugins/*/*.ml* &
+
+# Modules Architecture
+###############################################################################
+
+poor-archi: .depend
+	cat .depend | ocamldot | dot -Tpdf > poor-archi.pdf
+
+rich-archi:opt gui
+	ocamldoc.opt $(INCLUDES) -dot -dot-reduce -dot-include-all lib/util/*.ml lib/structures/*.ml lib/reasoners/*.ml lib/frontend/*.ml tools/text/*.ml tools/gui/*.ml \
+        parsers/why/*.ml lib/util/*.mli lib/structures/*.mli lib/reasoners/*.mli lib/frontend/*.mli tools/text/*.mli tools/gui/*.mli parsers/why/*.mli -verbose
+	grep -v "}" ocamldoc.out > archi.dot
+	rm ocamldoc.out
+	cat ../extra/subgraphs.dot >> archi.dot
+	echo "}" >> archi.dot
+	dot -Tpdf archi.dot > archi.pdf
+
+archi:$(NAME).byte $(GUINAME).byte
+	ocamldoc.opt $(INCLUDES) -dot -dot-reduce lib/util/*.ml lib/structures/*.ml lib/reasoners/*.ml lib/frontend/*.ml tools/text/*.ml tools/gui/*.ml \
+        parsers/why/*.ml lib/util/*.mli lib/structures/*.mli lib/reasoners/*.mli lib/frontend/*.mli tools/text/*.mli tools/gui/*.mli parsers/why/*.mli -verbose
+	grep -v "}" ocamldoc.out > archi.dot
+	rm ocamldoc.out
+	cat ../extra/subgraphs.dot >> archi.dot
+	echo "}" >> archi.dot
+	dot -Tpdf archi.dot > archi.pdf
+	evince archi.pdf 2> /dev/null > /dev/null &
+
+# try-alt-ergo
+##########################################################################################
+
+try-alt-ergo:
+	make clean
+	cp -rf ../alt-ergo ../try-alt-ergo/
+	cp -rf ../try-alt-ergo/extra/Makefile ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/extra/Makefile.js ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/lib-num ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/js ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/extra/src__main__main_js.ml ../try-alt-ergo/alt-ergo/tools/javascript/main_js.ml
+	cp -rf ../try-alt-ergo/extra/src__util__myUnix.ml ../try-alt-ergo/alt-ergo/lib/util/myUnix.ml
+	cp -rf ../try-alt-ergo/extra/src__util__numbers.ml ../try-alt-ergo/alt-ergo/lib/util/numbers.ml
+	cp -rf ../try-alt-ergo/extra/src__util__myZip.ml ../try-alt-ergo/alt-ergo/lib/util/myZip.ml
+	make depend -C ../try-alt-ergo/alt-ergo
+	make byte -C ../try-alt-ergo/alt-ergo
+	make try -C ../try-alt-ergo/alt-ergo
+	cp ../try-alt-ergo/alt-ergo/try-alt-ergo.js ../try-alt-ergo/html-interface/try-alt-ergo/alt-ergo.js
+	firefox ../try-alt-ergo/html-interface/try.html
+
+
+try-alt-ergo-mini:
+	make clean
+	cp -rf ../alt-ergo ../try-alt-ergo/
+	cp -rf ../try-alt-ergo/extra/Makefile ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/extra/Makefile.js ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/lib-num ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/js ../try-alt-ergo/alt-ergo/
+	cp -rf ../try-alt-ergo/extra/src__main__main_js_mini.ml ../try-alt-ergo/alt-ergo/tools/javascript/main_js.ml
+	cp -rf ../try-alt-ergo/extra/src__util__myUnix.ml ../try-alt-ergo/alt-ergo/lib/util/myUnix.ml
+	cp -rf ../try-alt-ergo/extra/src__util__numbers.ml ../try-alt-ergo/alt-ergo/lib/util/numbers.ml
+	cp -rf ../try-alt-ergo/extra/src__util__myZip.ml ../try-alt-ergo/alt-ergo/lib/util/myZip.ml
+	make depend -C ../try-alt-ergo/alt-ergo
+	make byte -C ../try-alt-ergo/alt-ergo
+	make try -C ../try-alt-ergo/alt-ergo
+	cp ../try-alt-ergo/alt-ergo/try-alt-ergo.js ../try-alt-ergo/html-interface/try-alt-ergo/alt-ergo-mini.js
+	firefox ../try-alt-ergo/html-interface/try-mini.html
+
+
+# TESTS
+##########################################################################################
+
+non-regression:$(OPT) satML fm-simplex
+	cp alt-ergo.opt ../non-regression/alt-ergo.opt
+	cd ../non-regression &&  ./non-regression.sh
+	rm ../non-regression/alt-ergo.opt
+
+
+
+
+# try to make all the targets
+##########################################################################################
+
+test-everything:
+	make configure
+	./configure --prefix=`pwd`/test-make-everything
+	rm -rf `pwd`/test-make-everything
+	mkdir `pwd`/test-make-everything
+	make show-dest-dirs
+	make depend
+	make all
+	make gui
+	make alt-ergo.byte
+	make opt
+	make alt-ergo.opt
+	make altgr-ergo.opt
+	make byte
+	make altgr-ergo.byte
+	make satML
+	make fm-simplex
+	make satML-plugin.cma
+	make fm-simplex-plugin.cma
+	make satML-plugin.cmxs
+	make fm-simplex-plugin.cmxs
+	make non-regression
+	make archi
+	make META
+	make install-opt
+	make install
+	make install-byte
+	make install-satML
+	make install-fm-simplex
+	make install-gui
+	make install-man
+	make stripped-arch-binary
+#	make try-alt-ergo
+#	make public-release # also performs opam-public, which needs public-export
+
+
+
+# headers
+##############
+headers:
+	cd ../extra/headers &&  ./headers.sh
+
+
+
+# STATIC
+##########################################################################################
+
+BIBBYTE_STATIC = zarith.cma nums.cma unix.cma str.cma zip.cma # = BIBBYTE minus dynlink.cma
+BIBOPT_STATIC = $(BIBBYTE_STATIC:.cma=.cmxa)
+
+hide-dynlink-in-wrapper-MyDynlink:
+	sed -i 's/include Dynlink/include DummyDL/g' lib/util/myDynlink.ml
+
+static: hide-dynlink-in-wrapper-MyDynlink depend $(MAINCMX)
+	$(OCAMLOPT) -ccopt -static $(OFLAGS) -o $@ $(BIBOPT_STATIC) $(MAINCMX)
+	sed -i 's/include DummyDL/include Dynlink/g' lib/util/myDynlink.ml
+	strip $@
+	mv static alt-ergo-static-$(VERSION)-$(ARCH)
+
+
+# PUBLIC RELEASES
+##########################################################################################
+PUBLIC_VERSION=$(VERSION)
+PUBLIC_RELEASE=alt-ergo-free-$(PUBLIC_VERSION)
+PUBLIC_TARGZ=$(PUBLIC_RELEASE).tar.gz
+FILES_DEST=../public-release/$(PUBLIC_RELEASE)/$(PUBLIC_RELEASE)
+
+public-release: # test-everything
+	rm -rf ../public-release
+	mkdir -p $(FILES_DEST)
+	cp configure $(FILES_DEST)
+	git clean -dfx
+	cp ../License.OCamlPro ../LGPL-License.txt ../Apache-License-2.0.txt $(FILES_DEST)/
+	cp ../README.md ../LICENSE.md ../COPYING.md $(FILES_DEST)/
+	cp configure.in Makefile.configurable.in Makefile.users Makefile Makefile.developers $(FILES_DEST)/
+	cp INSTALL.md opam CHANGES $(FILES_DEST)/
+	cp -rf lib tools parsers plugins preludes examples doc $(FILES_DEST)/
+	#echo "let version=\"$(PUBLIC_VERSION)\"" >> $(FILES_DEST)/lib/util/version.ml
+	echo "let release_commit = \"$(COMMIT_ID)\"" >> $(FILES_DEST)/lib/util/version.ml
+	echo "let release_date = \""`LANG=en_US; date`"\"" >> $(FILES_DEST)/lib/util/version.ml
+	cd $(FILES_DEST)/.. && tar cfz $(PUBLIC_TARGZ) $(PUBLIC_RELEASE)
+	rm -rf $(FILES_DEST)
+	autoconf && ./configure
+
+# Targets that work only after the modification in Makefile.XX and/or Alt-Ergo
+###############################################################################
+
+bisect-report:
+	bisect-report -dump - -html report bisect*.out
+
+
+
+
+
+
+
+ 

Makefile.users

 ARCH = $(shell uname -m)
 
-VERSION=$(shell grep "=" src/util/version.ml | cut -d"=" -f2 | head -n 1)
+VERSION=$(shell grep "=" lib/util/version.ml | cut -d"=" -f2 | head -n 1)
 
-LOCAL_INC = -I src/util -I src/structures -I src/theories -I src/instances \
-    -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main \
-    -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler \
-    -I non-free/plugins/fm-simplex
+LOCAL_INC = -I lib/util -I lib/structures -I lib/reasoners \
+    -I lib/frontend -I tools/text -I tools/gui \
+    -I parsers/why \
+    -I plugins/common -I plugins/satML \
+    -I plugins/fm-simplex
 
 INCLUDES = $(ZARITHLIB) $(LABLGTK2LIB)  $(CAMLZIPLIB) $(OCPLIBSIMPLEXLIB) $(LOCAL_INC)
 #for coverage # -I /usr/local/lib/ocaml/3.12.1/bisect -pp "camlp4o str.cma /usr/local/lib/ocaml/3.12.1/bisect/bisect_pp.cmo"
 
 BFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -g $(INCLUDES)
-OFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 $(INCLUDES)
-# -for-pack AltErgo
+OFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 $(INCLUDES) -for-pack AltErgo
 
 BIBBYTE = zarith.cma nums.cma unix.cma dynlink.cma str.cma zip.cma ocplibSimplex.cma
 # for coverage bisect.cma 
@@ -34,85 +34,94 @@ LIBNAME = altErgo
 BYTE=$(NAME).byte
 OPT=$(NAME).opt
 
+all: alt-ergo gui satML fm-simplex
+
 ifeq ($(OCAMLBEST),opt)
-all: opt
+alt-ergo: opt
 else
-all: byte
+alt-ergo: byte
 endif
 
-GENERATED = src/util/config.ml \
-            src/parsing/why_parser.ml \
-            src/parsing/why_parser.mli \
-            src/parsing/why_lexer.ml
+GENERATED = lib/util/config.ml \
+            lib/util/cmdline_parser.ml \
+            parsers/why/why_parser.ml \
+            parsers/why/why_parser.mli \
+            parsers/why/why_lexer.ml
 
 # bytecode and native-code compilation
 ######################################
 
-CMO = src/util/config.cmo \
-      src/util/version.cmo \
-      src/util/emap.cmo \
-      src/util/myUnix.cmo \
-      src/util/myDynlink.cmo \
-      src/util/myZip.cmo \
-      src/util/util.cmo \
-      src/util/lists.cmo \
-      src/util/numsNumbers.cmo \
-      src/util/zarithNumbers.cmo \
-      src/util/numbers.cmo \
-      src/util/timers.cmo \
-      src/util/options.cmo \
-      src/util/gc_debug.cmo \
-      src/util/loc.cmo \
-      src/util/hashcons.cmo \
-      src/util/hstring.cmo \
-      src/structures/exception.cmo \
-      src/structures/symbols.cmo \
-      src/structures/ty.cmo \
-      src/structures/parsed.cmo \
-      src/structures/typed.cmo \
-      src/structures/term.cmo \
-      src/structures/literal.cmo \
-      src/structures/formula.cmo \
-      src/structures/explanation.cmo \
-      src/structures/errors.cmo \
-      src/util/profiling_default.cmo \
-      src/util/profiling.cmo \
-      src/parsing/why_parser.cmo \
-      src/parsing/why_lexer.cmo \
-      src/preprocess/existantial.cmo \
-      src/preprocess/triggers.cmo \
-      src/preprocess/why_typing.cmo \
-      src/preprocess/cnf.cmo \
-      src/instances/matching.cmo \
-      src/instances/instances.cmo \
-      src/theories/polynome.cmo \
-      src/theories/ac.cmo \
-      src/theories/uf.cmo \
-      src/theories/use.cmo \
-      src/theories/intervals.cmo \
-      src/theories/inequalities.cmo \
-      src/theories/intervalCalculus.cmo \
-      src/theories/arith.cmo \
-      src/theories/records.cmo \
-      src/theories/bitv.cmo \
-      src/theories/arrays.cmo \
-      src/theories/sum.cmo \
-      src/theories/combine.cmo \
-      src/theories/ccx.cmo \
-      src/theories/theory.cmo \
-      src/sat/sat_solvers.cmo
-
-CMOFRONT = src/main/frontend.cmo
-
-MAINCMO = $(CMO) $(CMOFRONT) src/main/main_text.cmo
+CMO = lib/util/config.cmo \
+      lib/util/version.cmo \
+      lib/util/emap.cmo \
+      lib/util/myUnix.cmo \
+      lib/util/myDynlink.cmo \
+      lib/util/myZip.cmo \
+      lib/util/util.cmo \
+      lib/util/lists.cmo \
+      lib/util/numsNumbers.cmo \
+      lib/util/zarithNumbers.cmo \
+      lib/util/numbers.cmo \
+      lib/util/options.cmo \
+      lib/util/cmdline_parser.cmo \
+      lib/util/timers.cmo \
+      lib/util/gc_debug.cmo \
+      lib/util/loc.cmo \
+      lib/util/hconsing.cmo \
+      lib/util/hstring.cmo \
+      lib/structures/exception.cmo \
+      lib/structures/symbols.cmo \
+      lib/structures/ty.cmo \
+      lib/structures/parsed.cmo \
+      lib/structures/errors.cmo \
+      lib/structures/typed.cmo \
+      lib/structures/term.cmo \
+      lib/structures/fpa_rounding.cmo \
+      lib/structures/literal.cmo \
+      lib/structures/formula.cmo \
+      lib/structures/explanation.cmo \
+      lib/structures/commands.cmo \
+      lib/structures/profiling.cmo \
+      lib/reasoners/matching.cmo \
+      lib/reasoners/instances.cmo \
+      lib/reasoners/polynome.cmo \
+      lib/reasoners/ac.cmo \
+      lib/reasoners/uf.cmo \
+      lib/reasoners/use.cmo \
+      lib/reasoners/intervals.cmo \
+      lib/reasoners/inequalities.cmo \
+      lib/reasoners/intervalCalculus.cmo \
+      lib/reasoners/arith.cmo \
+      lib/reasoners/records.cmo \
+      lib/reasoners/bitv.cmo \
+      lib/reasoners/arrays.cmo \
+      lib/reasoners/sum.cmo \
+      lib/reasoners/combine.cmo \
+      lib/reasoners/ccx.cmo \
+      lib/reasoners/theory.cmo \
+      lib/reasoners/fun_sat.cmo \
+      lib/reasoners/sat_solver.cmo \
+      lib/frontend/triggers.cmo \
+      lib/frontend/typechecker.cmo \
+      lib/frontend/cnf.cmo \
+      lib/frontend/parsed_interface.cmo \
+      lib/frontend/frontend.cmo \
+      lib/frontend/parsers.cmo
+
+CMOFRONT = parsers/why/why_parser.cmo parsers/why/why_lexer.cmo
+
+# parsers/why/why_parser.cmo parsers/why/why_lexer.cmo
+
+MAINCMO = $(CMO) $(CMOFRONT) tools/text/main_text.cmo
 
 ifeq ($(ENABLEGUI),yes)
 	GUICMO = $(CMO) $(CMOFRONT) \
-                 src/gui/gui_session.cmo \
-                 src/gui/why_annoted.cmo \
-	         src/gui/why_connected.cmo \
-                 src/gui/gui_replay.cmo \
-                 src/main/main_gui.cmo
+                 tools/gui/gui_session.cmo \
+                 tools/gui/gui_config.cmo \
+                 tools/gui/annoted_ast.cmo \
+	         tools/gui/connected_ast.cmo \
+                 tools/gui/gui_replay.cmo \
+                 tools/gui/main_gui.cmo
 else 
 	GUICMO = 
 endif
@@ -127,11 +136,11 @@ opt: $(NAME).opt
 
 
 #### LIBRARY
-#$(LIBNAME).cmo: $(CMO) 
-#	$(OCAMLC) $(BFLAGS) -pack -o $(LIBNAME).cmo $^
+$(LIBNAME).cmo: $(CMO) $(CMOFRONT) lib/reasoners/sig.cmi
+	$(OCAMLC) $(BFLAGS) -pack -o $(LIBNAME).cmo $^
 
-#$(LIBNAME).cmx: $(CMX)
-#	$(OCAMLOPT) $(INCLUDES)  -pack -o $(LIBNAME).cmx $^
+$(LIBNAME).cmx: $(CMX) $(CMXFRONT) lib/reasoners/sig.cmi
+	$(OCAMLOPT) $(INCLUDES)  -pack -o $(LIBNAME).cmx $^
 
 
 
@@ -159,13 +168,24 @@ endif
 
 .PHONY: gui
 
-src/util/config.ml: config.status
-	@echo "let date = \""`LANG=en_US; date`"\"" >> src/util/config.ml
-	@echo "let bindir = \""$(BINDIR)"\"" >> src/util/config.ml
-	@echo "let libdir = \""$(LIBDIR)"\"" >> src/util/config.ml
-	@echo "let pluginsdir = \""$(PLUGINSDIR)"\"" >> src/util/config.ml
-	@echo "let datadir = \""$(DATADIR)"\"" >> src/util/config.ml
-	@echo "let mandir = \""$(MANDIR)"\"" >> src/util/config.ml
+lib/util/config.ml: config.status
+	@echo "let bindir = \""$(BINDIR)"\"" >> lib/util/config.ml
+	@echo "let libdir = \""$(LIBDIR)"\"" >> lib/util/config.ml
+	@echo "let pluginsdir = \""$(PLUGINSDIR)"\"" >> lib/util/config.ml
+	@echo "let preludesdir = \""$(PRELUDESDIR)"\"" >> lib/util/config.ml
+	@echo "let datadir = \""$(DATADIR)"\"" >> lib/util/config.ml
+	@echo "let mandir = \""$(MANDIR)"\"" >> lib/util/config.ml
+
+lib/util/cmdline_parser.ml: config.status
+	@echo "(* parse_args () should be called as soon as possible (put earlier" > lib/util/cmdline_parser.ml
+	@echo "   when linking) because some choices during compilation depend on" >> lib/util/cmdline_parser.ml
+	@echo "   given options (e.g. dfs-sat)" >> lib/util/cmdline_parser.ml
+	@echo "\n   -> The following call:" >> lib/util/cmdline_parser.ml
+	@echo "   1 - should be kept when builtind Alt-Ergo tools" >> lib/util/cmdline_parser.ml
+	@echo "   2 - should be removed to build and use only the library." >> lib/util/cmdline_parser.ml
+	@echo "\n   Alternatively to 2, one can just remove cmdline_parser.cmo/cmx in" >> lib/util/cmdline_parser.ml
+	@echo "   Makefile.users *)" >> lib/util/cmdline_parser.ml
+	@echo "\nlet () = Options.parse_cmdline_arguments ()" >> lib/util/cmdline_parser.ml
 
 META: config.status
 	@echo "description = \"API of Alt-Ergo: An automatic theorem prover dedicated to program verification\"" > META
@@ -179,26 +199,33 @@ META: config.status
 # installation
 ##############
 
-install-byte: install-man
+install-byte: install-man install-preludes
 	mkdir -p $(BINDIR)
 	cp -f $(NAME).byte $(BINDIR)/$(NAME)$(EXE)
 
-install-opt: install-man
+install-opt: install-man install-preludes
 	mkdir -p $(BINDIR)
 	cp -f $(NAME).opt $(BINDIR)/$(NAME)$(EXE)
 
 install-man:
 	mkdir -p $(MANDIR)/man1
-	cp -f doc/*.1 $(MANDIR)/man1
+	cp -f doc/alt-ergo.1 $(MANDIR)/man1
+
+install-preludes:
+	mkdir -p $(PRELUDESDIR)
+	cp -f preludes/fpa-theory-2017-01-04-16h00.why $(PRELUDESDIR)/
 
-install: install-man
+install-ae: install-man install-preludes
 	mkdir -p $(BINDIR)
 	cp -f $(NAME).$(OCAMLBEST) $(BINDIR)/$(NAME)$(EXE)
 
 install-gui:
+ifeq ($(ENABLEGUI),yes)
+	mkdir -p $(BINDIR)
 	cp -f $(GUINAME).$(OCAMLBEST) $(BINDIR)/$(GUINAME)$(EXE)
 	mkdir -p $(DATADIR)/gtksourceview-2.0/language-specs
 	cp -f doc/gtk-lang/alt-ergo.lang $(DATADIR)/gtksourceview-2.0/language-specs/alt-ergo.lang
+endif
 
 # install-pack-opt: xpack
 # 	mkdir -p $(LIBDIR)
@@ -216,6 +243,18 @@ install-gui:
 # install-pack:: install-pack-opt
 # endif
 
+install: install-ae install-gui install-fm-simplex install-satML
+
+uninstall:
+	@rm $(BINDIR)/$(NAME)$(EXE)
+	@rm $(MANDIR)/man1/alt-ergo.1
+	-@rm $(BINDIR)/$(GUINAME)$(EXE)
+	-@rm $(DATADIR)/gtksourceview-2.0/language-specs/alt-ergo.lang
+	@rm $(PLUGINSDIR)/satML-plugin.cm*
+	@rm $(PLUGINSDIR)/fm-simplex-plugin.cm*
+	@rm $(PRELUDESDIR)/fpa-theory-2017-01-04-16h00.why
+
+
 # generic rules
 ###############
 
@@ -237,54 +276,38 @@ install-gui:
 	$(OCAMLLEX) $< > /dev/null
 
 .mly.ml:
-	$(OCAMLYACC) -v $< 
+	$(MENHIR) -v $< 
 
 .mly.mli:
-	$(OCAMLYACC) -v $< 
+	$(MENHIR) -v $< 
 
 
 # clean
 #######
 
 clean:
-	@for dd in src/util src/structures src/theories src/instances src/sat src/preprocess src/parsing src/gui src/main non-free/plugins/common non-free/plugins/satML non-free/plugins/common non-free/plugins/common non-free/plugins/profiler non-free/plugins/fm-simplex non-free/plugins/ctrl-alt-ergo; do \
+	@for dd in lib/util lib/structures lib/reasoners lib/frontend tools/text tools/gui parsers/why plugins/common plugins/satML plugins/common plugins/common plugins/fm-simplex ; do \
 	rm -f $$dd/*.cm[ioxtp] $$dd/*.cmti $$dd/*.o $$dd/*~ $$dd/*.annot $$dd/*.owz;\
 	rm -f $(GENERATED) $$dd/*.output META ; \
 	rm -f $(NAME).byte $(NAME).opt $(GUINAME).opt $(GUINAME).byte *~; \
 	done
-	@rm -rf altErgo.cm* altErgo.o *.log archi.dot archi.pdf src/*~ *.cmxs *.cmos ctrl-alt-ergo.* alt-ergo-static* *.cmxs *.cma essentiel essentiel.tar.bz2 alt-ergo-$(VERSION)-$(ARCH)
+	@rm -rf altErgo.cm* altErgo.o *.log archi.dot archi.pdf lib/*~ *.cmxs *.cmos alt-ergo-static* *.cmxs *.cma essentiel essentiel.tar.bz2 alt-ergo-$(VERSION)-$(ARCH)
 
 
 # depend
 ########
 
 .depend depend: $(GENERATED)
-	$(OCAMLDEP) -slash $(LOCAL_INC) src/util/*.ml* src/structures/*.ml* src/theories/*.ml* src/instances/*.ml* src/sat/*.ml* src/preprocess/*.ml* src/parsing/*.ml* src/gui/*.ml* src/main/*.ml* non-free/plugins/common/*ml* non-free/plugins/satML/*ml* non-free/plugins/fm-simplex/*ml* non-free/plugins/profiler/*ml* > .depend
+	$(OCAMLDEP) -slash $(LOCAL_INC) lib/util/*.ml* lib/structures/*.ml* lib/reasoners/*.ml* lib/frontend/*.ml* tools/text/*.ml* \
+        tools/gui/*.ml* parsers/why/*.ml* plugins/common/*ml* plugins/satML/*ml* plugins/fm-simplex/*ml* > .depend
 
 include .depend
 
-#### BUILD & INSTALL non-free plugins and tools
+#### BUILD & INSTALL additional plugins
 
-ifeq ($(OCAMLBEST),opt)
-cae: ctrl-alt-ergo.opt
-else
-cae: ctrl-alt-ergo.byte
-endif
-
-ctrl-alt-ergo.opt:
-	cd non-free/ctrl-alt-ergo && $(OCAMLOPT) $(OFLAGS) -o ../../ctrl-alt-ergo.opt $(BIBOPT) ctrlAltErgo.mli ctrlAltErgo.ml
-
-ctrl-alt-ergo.byte:
-	cd non-free/ctrl-alt-ergo && $(OCAMLC) $(BFLAGS) -o ../../ctrl-alt-ergo.byte $(BIBBYTE) ctrlAltErgo.mli ctrlAltErgo.ml
-
-install-cae: ctrl-alt-ergo.$(OCAMLBEST)
-	mkdir -p $(BINDIR)
-	cp -f ctrl-alt-ergo.$(OCAMLBEST) $(BINDIR)/ctrl-alt-ergo$(EXE)
-
-
-SATML-CMO = non-free/plugins/common/vec.cmo \
-            non-free/plugins/satML/satml.cmo \
-            non-free/plugins/satML/satml_frontend.cmo
+SATML-CMO = plugins/common/vec.cmo \
+            plugins/satML/satml.cmo \
+            plugins/satML/satml_frontend.cmo
 
 SATML-CMX = $(SATML-CMO:.cmo=.cmx)
 
@@ -310,10 +333,10 @@ else
 endif
 
 
-FM-SIMPLEX-CMO = non-free/plugins/common/vec.cmo \
-                 non-free/plugins/fm-simplex/simplex_cache.cmo \
-                 non-free/plugins/fm-simplex/simplex.cmo \
-                 non-free/plugins/fm-simplex/fmSimplexIneqs.cmo
+FM-SIMPLEX-CMO = plugins/common/vec.cmo \
+                 plugins/fm-simplex/simplex_cache.cmo \
+                 plugins/fm-simplex/simplex.cmo \
+                 plugins/fm-simplex/fmSimplexIneqs.cmo
 
 FM-SIMPLEX-CMX = $(FM-SIMPLEX-CMO:.cmo=.cmx)
 
@@ -339,31 +362,11 @@ else
 endif
 
 
-profiler-plugin.cmxs: $(CMX) non-free/plugins/profiler/profiler.cmx
-	$(if $(QUIET),@echo 'Library $@' &&) $(OCAMLOPT) $(INCLUDES)  -shared -o $@ non-free/plugins/profiler/profiler.cmx
-
-profiler-plugin.cma: $(CMO) non-free/plugins/profiler/profiler.cmo
-	$(if $(QUIET),@echo 'Library $@' &&) $(OCAMLC) $(INCLUDES)  -a        -o $@ non-free/plugins/profiler/profiler.cmo
-
-ifeq ($(OCAMLBEST),opt)
-profiler: profiler-plugin.cmxs
-else
-profiler: profiler-plugin.cma
-endif
-
-install-profiler: profiler
-ifeq ($(OCAMLBEST),opt)
-	mkdir -p $(PLUGINSDIR)
-	cp -f profiler-plugin.cmxs $(PLUGINSDIR)
-else
-	mkdir -p $(PLUGINSDIR)
-	cp -f profiler-plugin.cma $(PLUGINSDIR)
-endif
-
 show-dest-dirs:
 	@echo BINDIR      = $(BINDIR)
 	@echo LIBDIR      = $(LIBDIR)
 	@echo PLUGINSDIR  = $(PLUGINSDIR)
+	@echo PRELUDESDIR = $(PRELUDESDIR)
 	@echo DATADIR     = $(DATADIR)
 	@echo MANDIR      = $(MANDIR)
 
@@ -388,4 +391,4 @@ stripped-arch-binary: $(OPT)
 	strip alt-ergo-$(VERSION)-$(ARCH)
 
 opam-deps:
-	opam install zarith camlzip conf-gtksourceview ocplib-simplex
+	opam install zarith camlzip conf-gtksourceview ocplib-simplex menhir

README.md

+next | master
+------------ | -------------
+[![Travis-CI Build Status](https://travis-ci.org/OCamlPro/alt-ergo.svg?branch=next)](https://travis-ci.org/OCamlPro/alt-ergo) | [![Travis-CI Build Status](https://travis-ci.org/OCamlPro/alt-ergo.svg?branch=master)](https://travis-ci.org/OCamlPro/alt-ergo) 
+
 # Alt-Ergo
 
 Alt-Ergo is an automatic theorem prover of mathematical formulas. It
@@ -8,12 +12,12 @@ See more details on http://alt-ergo.ocamlpro.com/
 
 ## Copyright
 
-See enclosed COPYING.md file
+See enclosed LICENSE.md file
 
 
 ## Build, Installation and Usage
 
-See enclosed INSTALL.md file
+See enclosed sources/INSTALL.md file
 
 
 ## Support

configure

@@ -581,7 +581,7 @@ PACKAGE_STRING=
 PACKAGE_BUGREPORT=
 PACKAGE_URL=
 
-ac_unique_file="src/main/frontend.ml"
+ac_unique_file="lib/util/options.ml"
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
 EXE
@@ -596,7 +596,7 @@ OCAMLLIB
 OCAMLVERSION
 OCAMLBEST
 OCAMLWEB
-OCAMLYACC
+MENHIR
 OCAMLLEXDOTOPT
 OCAMLLEX
 OCAMLDEP
@@ -624,6 +624,7 @@ infodir
 docdir
 oldincludedir
 includedir
+runstatedir
 localstatedir
 sharedstatedir
 sysconfdir
@@ -688,6 +689,7 @@ datadir='${datarootdir}'
 sysconfdir='${prefix}/etc'
 sharedstatedir='${prefix}/com'
 localstatedir='${prefix}/var'
+runstatedir='${localstatedir}/run'
 includedir='${prefix}/include'
 oldincludedir='/usr/include'
 docdir='${datarootdir}/doc/${PACKAGE}'
@@ -940,6 +942,15 @@ do
   | -silent | --silent | --silen | --sile | --sil)
     silent=yes ;;
 
+  -runstatedir | --runstatedir | --runstatedi | --runstated \
+  | --runstate | --runstat | --runsta | --runst | --runs \
+  | --run | --ru | --r)
+    ac_prev=runstatedir ;;
+  -runstatedir=* | --runstatedir=* | --runstatedi=* | --runstated=* \
+  | --runstate=* | --runstat=* | --runsta=* | --runst=* | --runs=* \
+  | --run=* | --ru=* | --r=*)
+    runstatedir=$ac_optarg ;;
+
   -sbindir | --sbindir | --sbindi | --sbind | --sbin | --sbi | --sb)
     ac_prev=sbindir ;;
   -sbindir=* | --sbindir=* | --sbindi=* | --sbind=* | --sbin=* \
@@ -1077,7 +1088,7 @@ fi
 for ac_var in	exec_prefix prefix bindir sbindir libexecdir datarootdir \
 		datadir sysconfdir sharedstatedir localstatedir includedir \
 		oldincludedir docdir infodir htmldir dvidir pdfdir psdir \
-		libdir localedir mandir
+		libdir localedir mandir runstatedir
 do
   eval ac_val=\$$ac_var
   # Remove trailing slashes.
@@ -1230,6 +1241,7 @@ Fine tuning of the installation directories:
   --sysconfdir=DIR        read-only single-machine data [PREFIX/etc]
   --sharedstatedir=DIR    modifiable architecture-independent data [PREFIX/com]
   --localstatedir=DIR     modifiable single-machine data [PREFIX/var]
+  --runstatedir=DIR       modifiable per-process data [LOCALSTATEDIR/run]
   --libdir=DIR            object code libraries [EPREFIX/lib]
   --includedir=DIR        C header files [PREFIX/include]
   --oldincludedir=DIR     C header files for non-gcc [/usr/include]
@@ -2277,15 +2289,20 @@ fi
     fi
 fi
 
-# Extract the first word of "ocamlyacc", so it can be a program name with args.
-set dummy ocamlyacc; ac_word=$2
+#AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no)
+#if test "$OCAMLYACC" = no ; then
+#	AC_MSG_ERROR(Cannot find ocamlyacc.)
+#fi
+
+# Extract the first word of "menhir", so it can be a program name with args.
+set dummy menhir; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_OCAMLYACC+:} false; then :
+if ${ac_cv_prog_MENHIR+:} false; then :
   $as_echo_n "(cached) " >&6
 else
-  if test -n "$OCAMLYACC"; then
-  ac_cv_prog_OCAMLYACC="$OCAMLYACC" # Let the user override the test.
+  if test -n "$MENHIR"; then
+  ac_cv_prog_MENHIR="$MENHIR" # Let the user override the test.
 else
 as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
 for as_dir in $PATH
@@ -2294,7 +2311,7 @@ do
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
   if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
-    ac_cv_prog_OCAMLYACC="ocamlyacc"
+    ac_cv_prog_MENHIR="menhir"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
   fi
@@ -2302,21 +2319,21 @@ done
   done
 IFS=$as_save_IFS
 
-  test -z "$ac_cv_prog_OCAMLYACC" && ac_cv_prog_OCAMLYACC="no"
+  test -z "$ac_cv_prog_MENHIR" && ac_cv_prog_MENHIR="no"
 fi
 fi
-OCAMLYACC=$ac_cv_prog_OCAMLYACC
-if test -n "$OCAMLYACC"; then
-  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $OCAMLYACC" >&5
-$as_echo "$OCAMLYACC" >&6; }
+MENHIR=$ac_cv_prog_MENHIR
+if test -n "$MENHIR"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $MENHIR" >&5
+$as_echo "$MENHIR" >&6; }
 else
   { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
 $as_echo "no" >&6; }
 fi
 
 
-if test "$OCAMLYACC" = no ; then
-	as_fn_error $? "Cannot find ocamlyacc." "$LINENO" 5
+if test "$MENHIR" = no ; then
+	as_fn_error $? "Cannot find menhir." "$LINENO" 5
 fi
 
 # checking for lablgtk2
@@ -2424,6 +2441,7 @@ fi
 
 
 
+#AC_SUBST(OCAMLYACC)
 
 
 

configure.in

-#****************************************************************************#
-#     The Alt-Ergo theorem prover                                            #
-#     Copyright (C) 2006-2013                                                #
-#     CNRS - INRIA - Universite Paris Sud                                    #
-#                                                                            #
-#     Sylvain Conchon                                                        #
-#     Evelyne Contejean                                                      #
-#                                                                            #
-#     Francois Bobot                                                         #
-#     Mohamed Iguernelala                                                    #
-#     Stephane Lescuyer                                                      #
-#     Alain Mebsout                                                          #
-#                                                                            #
-#   This file is distributed under the terms of the CeCILL-C licence         #
-#****************************************************************************#
-
 #
 # autoconf input for Objective Caml programs
 # Copyright (C) 2001 Jean-Christophe Filli�tre
@@ -48,7 +32,7 @@
 
 # check for one particular file of the sources 
 # ADAPT THE FOLLOWING LINE TO YOUR SOURCES!
-AC_INIT(src/main/frontend.ml)
+AC_INIT(lib/util/options.ml)
 
 # Check for Ocaml compilers
 
@@ -231,9 +215,14 @@ else
     fi
 fi
 
-AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no)
-if test "$OCAMLYACC" = no ; then
-	AC_MSG_ERROR(Cannot find ocamlyacc.)
+#AC_CHECK_PROG(OCAMLYACC,ocamlyacc,ocamlyacc,no)
+#if test "$OCAMLYACC" = no ; then
+#	AC_MSG_ERROR(Cannot find ocamlyacc.)
+#fi
+
+AC_CHECK_PROG(MENHIR,menhir,menhir,no)
+if test "$MENHIR" = no ; then
+	AC_MSG_ERROR(Cannot find menhir.)
 fi
 
 # checking for lablgtk2
@@ -287,7 +276,8 @@ AC_SUBST(OCAMLC)
 AC_SUBST(OCAMLOPT)
 AC_SUBST(OCAMLDEP)
 AC_SUBST(OCAMLLEX)
-AC_SUBST(OCAMLYACC)
+#AC_SUBST(OCAMLYACC)
+AC_SUBST(MENHIR)
 AC_SUBST(OCAMLBEST)
 AC_SUBST(OCAMLVERSION)
 AC_SUBST(OCAMLLIB)

debian/changelog

+alt-ergo (2.0.0-1) UNRELEASED; urgency=medium
+
+  * Adjust debian/watch to the new *-free releases
+  * New upstream release
+    - refreshed patch 0001-dont-activate-debug-flags
+    - dropped patch 0002-non-free-dropped which is no longer needed as upstream
+      now publishes a completely free version
+    - dropped patch 0003-allow-set-build-date since upstream has replaced
+      the build-date by a release-date.
+    - dropped patch spelling which has been applied upstream
+    - dropped patch ocplib-simplex-0.4 since issue solved by upstream
+  * debian/copyright:
+    - license changed from CeCILL-C to Apache 2.0
+    - https in format header
+  * Added minimal version on build-dependency ocplib-simplex as indicated
+    by upstream.
+    
+ -- Ralf Treinen <treinen@debian.org>  Wed, 13 Feb 2019 17:41:57 +0100
+
 alt-ergo (1.30+dfsg1-2) unstable; urgency=medium
 
   * Since lablgtk2 does no longer build liblablgtksourceview2-ocaml-dev:

debian/control

@@ -12,7 +12,7 @@ Build-Depends:
  libocamlgraph-ocaml-dev (>= 1.8.5~),
  libzarith-ocaml-dev,
  libzip-ocaml-dev,
- ocplib-simplex-ocaml-dev,
+ ocplib-simplex-ocaml-dev (>= 0.4),
  dh-ocaml (>= 0.9.0~)
 Homepage: http://alt-ergo.lri.fr
 Standards-Version: 4.2.1

debian/patches/0001-dont-activate-debug-flag

@@ -4,16 +4,16 @@ Subject: No need to activate debug flag
 
 Index: alt-ergo/Makefile.users
 ===================================================================
---- alt-ergo.orig/Makefile.users	2016-11-29 21:30:02.550935423 +0100
-+++ alt-ergo/Makefile.users	2016-11-29 21:30:22.759016581 +0100
-@@ -10,8 +10,8 @@
+--- alt-ergo.orig/Makefile.users	2019-02-13 16:46:56.499585886 +0100
++++ alt-ergo/Makefile.users	2019-02-13 16:47:28.211441067 +0100
+@@ -11,8 +11,8 @@
  INCLUDES = $(ZARITHLIB) $(LABLGTK2LIB)  $(CAMLZIPLIB) $(OCPLIBSIMPLEXLIB) $(LOCAL_INC)
  #for coverage # -I /usr/local/lib/ocaml/3.12.1/bisect -pp "camlp4o str.cma /usr/local/lib/ocaml/3.12.1/bisect/bisect_pp.cmo"
  
 -BFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -g $(INCLUDES)
--OFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 $(INCLUDES)
+-OFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -g -inline 100 $(INCLUDES) -for-pack AltErgo
 +BFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence $(INCLUDES)
-+OFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -inline 100 $(INCLUDES)
- # -for-pack AltErgo
++OFLAGS = -annot -absname -bin-annot -short-paths -strict-sequence -inline 100 $(INCLUDES) -for-pack AltErgo
  
  BIBBYTE = zarith.cma nums.cma unix.cma dynlink.cma str.cma zip.cma ocplibSimplex.cma
+ # for coverage bisect.cma 

debian/patches/0002-non-free-dropped

-Author: Ralf Treinen <treinen@debian.org>
-Description: adapt Makefile to the removal of the non-free directory
-
-Index: alt-ergo/Makefile.users
-===================================================================
---- alt-ergo.orig/Makefile.users	2016-11-29 21:31:31.135291477 +0100
-+++ alt-ergo/Makefile.users	2016-11-29 21:31:31.131291461 +0100
-@@ -4,8 +4,6 @@
- 
- LOCAL_INC = -I src/util -I src/structures -I src/theories -I src/instances \
-     -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main \
--    -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler \
--    -I non-free/plugins/fm-simplex
- 
- INCLUDES = $(ZARITHLIB) $(LABLGTK2LIB)  $(CAMLZIPLIB) $(OCPLIBSIMPLEXLIB) $(LOCAL_INC)
- #for coverage # -I /usr/local/lib/ocaml/3.12.1/bisect -pp "camlp4o str.cma /usr/local/lib/ocaml/3.12.1/bisect/bisect_pp.cmo"
-@@ -247,7 +245,7 @@
- #######
- 
- clean:
--	@for dd in src/util src/structures src/theories src/instances src/sat src/preprocess src/parsing src/gui src/main non-free/plugins/common non-free/plugins/satML non-free/plugins/common non-free/plugins/common non-free/plugins/profiler non-free/plugins/fm-simplex non-free/plugins/ctrl-alt-ergo; do \
-+	@for dd in src/util src/structures src/theories src/instances src/sat src/preprocess src/parsing src/gui src/main ; do \
- 	rm -f $$dd/*.cm[ioxtp] $$dd/*.cmti $$dd/*.o $$dd/*~ $$dd/*.annot $$dd/*.owz;\
- 	rm -f $(GENERATED) $$dd/*.output META ; \
- 	rm -f $(NAME).byte $(NAME).opt $(GUINAME).opt $(GUINAME).byte *~; \
-@@ -259,11 +257,11 @@
- ########
- 
- .depend depend: $(GENERATED)
--	$(OCAMLDEP) -slash $(LOCAL_INC) src/util/*.ml* src/structures/*.ml* src/theories/*.ml* src/instances/*.ml* src/sat/*.ml* src/preprocess/*.ml* src/parsing/*.ml* src/gui/*.ml* src/main/*.ml* non-free/plugins/common/*ml* non-free/plugins/satML/*ml* non-free/plugins/fm-simplex/*ml* non-free/plugins/profiler/*ml* > .depend
-+	$(OCAMLDEP) -slash $(LOCAL_INC) src/util/*.ml* src/structures/*.ml* src/theories/*.ml* src/instances/*.ml* src/sat/*.ml* src/preprocess/*.ml* src/parsing/*.ml* src/gui/*.ml* src/main/*.ml*  > .depend
- 
- include .depend
- 
--#### BUILD & INSTALL non-free plugins and tools
-+#### BUILD & INSTALL  plugins and tools
- 
- ifeq ($(OCAMLBEST),opt)
- cae: ctrl-alt-ergo.opt
-@@ -271,21 +269,11 @@
- cae: ctrl-alt-ergo.byte
- endif
- 
--ctrl-alt-ergo.opt:
--	cd non-free/ctrl-alt-ergo && $(OCAMLOPT) $(OFLAGS) -o ../../ctrl-alt-ergo.opt $(BIBOPT) ctrlAltErgo.mli ctrlAltErgo.ml
--
--ctrl-alt-ergo.byte:
--	cd non-free/ctrl-alt-ergo && $(OCAMLC) $(BFLAGS) -o ../../ctrl-alt-ergo.byte $(BIBBYTE) ctrlAltErgo.mli ctrlAltErgo.ml
--
- install-cae: ctrl-alt-ergo.$(OCAMLBEST)
- 	mkdir -p $(BINDIR)
- 	cp -f ctrl-alt-ergo.$(OCAMLBEST) $(BINDIR)/ctrl-alt-ergo$(EXE)
- 
- 
--SATML-CMO = non-free/plugins/common/vec.cmo \
--            non-free/plugins/satML/satml.cmo \
--            non-free/plugins/satML/satml_frontend.cmo
--
- SATML-CMX = $(SATML-CMO:.cmo=.cmx)
- 
- satML-plugin.cmxs: $(CMX) $(SATML-CMX)
-@@ -310,11 +298,6 @@
- endif
- 
- 
--FM-SIMPLEX-CMO = non-free/plugins/common/vec.cmo \
--                 non-free/plugins/fm-simplex/simplex_cache.cmo \
--                 non-free/plugins/fm-simplex/simplex.cmo \
--                 non-free/plugins/fm-simplex/fmSimplexIneqs.cmo
--
- FM-SIMPLEX-CMX = $(FM-SIMPLEX-CMO:.cmo=.cmx)
- 
- fm-simplex-plugin.cmxs: $(CMX) $(FM-SIMPLEX-CMX)
-@@ -339,12 +322,6 @@
- endif
- 
- 
--profiler-plugin.cmxs: $(CMX) non-free/plugins/profiler/profiler.cmx
--	$(if $(QUIET),@echo 'Library $@' &&) $(OCAMLOPT) $(INCLUDES)  -shared -o $@ non-free/plugins/profiler/profiler.cmx
--
--profiler-plugin.cma: $(CMO) non-free/plugins/profiler/profiler.cmo
--	$(if $(QUIET),@echo 'Library $@' &&) $(OCAMLC) $(INCLUDES)  -a        -o $@ non-free/plugins/profiler/profiler.cmo
--
- ifeq ($(OCAMLBEST),opt)
- profiler: profiler-plugin.cmxs
- else

debian/patches/0003-allow-set-build-date

-Description: Allow set the build date
- This patch moves the date command used for setting the build date to a
- variable, allowing to set the build date externally.
-Author: Juan Picca <jumapico@gmail.com>,
- updated by Jakub Wilk <jwilk@debian.org>
-Last-Update: 2015-05-25
----
-Index: alt-ergo/Makefile.users
-===================================================================
---- alt-ergo.orig/Makefile.users	2016-11-29 21:32:45.203589705 +0100
-+++ alt-ergo/Makefile.users	2016-11-29 21:32:45.199589689 +0100
-@@ -1,4 +1,5 @@
- ARCH = $(shell uname -m)
-+BUILD_DATE ?= $(shell LANG=C date)
- 
- VERSION=$(shell grep "=" src/util/version.ml | cut -d"=" -f2 | head -n 1)
- 
-@@ -158,7 +159,7 @@
- .PHONY: gui
- 
- src/util/config.ml: config.status
--	@echo "let date = \""`LANG=en_US; date`"\"" >> src/util/config.ml
-+	@echo "let date = \""$(BUILD_DATE)"\"" >> src/util/config.ml
- 	@echo "let bindir = \""$(BINDIR)"\"" >> src/util/config.ml
- 	@echo "let libdir = \""$(LIBDIR)"\"" >> src/util/config.ml
- 	@echo "let pluginsdir = \""$(PLUGINSDIR)"\"" >> src/util/config.ml