released sr2019

Author: Armin Biere

.travis.yml

@@ -6,4 +6,5 @@ os:
 - linux
 - osx
 branches:
+#- development
 - master

BUILD.md

@@ -0,0 +1,69 @@
+# CaDiCaL Build
+
+Use `./configure && make` to configure and build `cadical` in the default
+`build` sub-directory.
+
+This will also build the library `libcadical.a` as well as the model based
+tester `mobical`:
+  
+    build/cadical
+    build/mobical
+    build/libcadical.a
+
+The header file of the library is in
+
+    src/cadical.hpp
+
+The build process requires GNU make.  Using the generated `makefile` with
+GNU make compiles separate object files, which can be cached (for instance
+with `ccache`).  The `makefile` uses parallel compilation by default (`-j`).
+
+You might want to check out options of `./configure -h`, such as
+
+    ./configure -c # include assertion checking code
+
+    ./configure -l # include code to really see what the solver is doing
+
+    ./configure -a # both above and in addition `-g` for debugging.
+
+You can easily use multiple build directories, e.g.,
+
+    mkdir debug; cd debug; ../configure -g; make
+
+which compiles and builds a debugging version in the sub-directory `debug`,
+since `-g` was specified as parameter to `configure`.  The object files,
+the library and the binaries are all independent of those in the default
+build directory `build`.
+
+All source files reside in the `src` directory.  The library `libcadical.a`
+is compiled from all the `.cpp` files except `cadical.cpp` and
+`mobical.cpp`, which provide the applications, i.e., the stand alone solver
+`cadical` and the model based tester `mobical`.
+
+If you can not or do not want to rely on our `configure` script nor on our
+build system based on GNU `make`, then this is easily doable as follows.
+
+    mkdir build
+    cd build
+    for f in ../src/*.cpp; do g++ -O3 -DNDEBUG -DNBUILD -c $f; done
+    ar rc libcadical.a `ls *.o | grep -v ical.o`
+    g++ -O3 -DNDEBUG -DNBUILD -o cadical cadical.o -L. -lcadical
+    g++ -O3 -DNDEBUG -DNBUILD -o mobical mobical.o -L. -lcadical
+
+Note that application object files are excluded from the library.
+Of course you can use different compilation options as well.
+  
+Since `build.hpp` is not generated in this flow the `-DNBUILD` flag is
+necessary though, which avoids dependency of `version.cpp` on `build.hpp`.
+Consequently you will only get very basic version information compiled into
+the library and binaries (guaranteed is in essence just the version number
+of the library).
+
+Further note that the `configure` script provides some feature checks and
+might generate additional compiler flags necessary for compilation.  You
+might need to set those yourself or just use a modern C++11 compiler.
+
+This manual build process using object files is fast enough in combination
+with caching solutions such as `ccache`.  But it lacks the ability of our
+GNU make solution to run compilation in parallel without additional parallel
+process scheduling solutions.

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2016-2018 Armin Biere, Johannes Kepler University Linz, Austria
+Copyright (c) 2016-2019 Armin Biere, Johannes Kepler University Linz, Austria
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -1,4 +1,4 @@
-# CaDiCaL
+# CaDiCaL Overview
 
 CaDiCaL Simplified Satisfiability Solver
 
@@ -7,50 +7,25 @@ which is easy to understand and change, while at the same time not being
 much slower than other state-of-the-art CDCL solvers.  Originally we wanted
 to also radically simplify the design and internal data structures, but that
 goal was only achieved partially, at least for instance compared to
-Lingeling. On the other hand CaDiCaL actually became in general faster than
-Lingeling even though it is missing some preprocessors (mostly parity and
-cardinality constraint reasoning), which would be crucial to solve certain
-instances. The incremental API is incomplete.
+Lingeling.
 
-Use './configure && make' to configure and build 'cadical' in the default
-'build' sub-directory.  This will also build the library 'libcadical.a'.
-  
-  - ./build/libcadical.a
-
-  - ./build/cadical
-
-The build process requires GNU make.  Using the generated 'makefile' with
-GNU make compiles separate object files, which can be cached (for instance
-with 'ccache').  The 'makefile' uses parallel compilation by default ('-j').
-
-The header file of the library is in 'src/cadical.hpp'.
-
-You might want to check out options of './configure -h', such as
-
-  - ./configure -c # include assertion checking code
-
-  - ./configure -l # include code to really see what the solver is doing
+However, the code is much better documented and on the other hand CaDiCaL
+actually became in general faster than Lingeling even though it is missing
+some preprocessors (mostly parity and cardinality constraint reasoning),
+which would be crucial to solve certain instances.
 
-  - ./configure -a # both above and in addition '-g' for debugging.
-
-You can easily use multiple build directories, e.g.,
-
-  - mkdir debug; cd debug; ../configure -g; make
-
-which compiles and builds a debugging version in the sub-directory 'debug',
-since '-g' was specified as parameter to 'configure'.  The object files,
-the library and the binary are all independent of those in the default
-build directory 'build'.
-
-The latest version of CaDiCaL can be found on 'github'
-
-  - http://github.com/arminbiere/cadical
-
-which also contains a test suite.  Use 'make test' to run it.
+Use `./configure && make` to configure and build `cadical` and the library
+`libcadical.a` in the default `build` sub-directory.  The header file of
+the library is [`src/cadical.hpp`](src/cadical.hpp) and includes an example
+for API usage.
+  
+See [`BUILD.md`](BUILD.md) for options and more details related to the build
+process and [`test/README.md`](test/README.md) for testing the library and
+the solver.
 
-A plain stable source release can also be found at
+The solver has the following usage `cadical [ dimacs [ proof ] ]`.
+See `cadical -h` for more options.
 
-  - http://fmv.jku.at/cadical
+The latest version can be found at <http://fmv.jku.at/cadical>.
 
 Armin Biere
-Sat Mar 24 11:52:12 CET 2018

TODO.md

@@ -1 +1 @@
-sc18
+sr2019