modernize for asdf3

fix minisat compile on modern c++ compilers

modernize autotools usage

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

add missing configure.ac and ltmain.sh in minisat subtree

update to newer libtool, keep in-tree

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

another round of default test predicate mess

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

messing with default test predicate in macro again

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

.gitignore update

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

fixes for package name confusion in swig-lispify

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Reduce consing in flush-to-backend

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Add vector variant for clause-valid method

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Reduce consing and recursion in split-delimited-string

ACL did not recognize tail-recursion

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Allow assumptions to be lists or vectors in backend

Implement vector variant for minisat backend

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Avoid double mapping from symbolic literals to variables in CNF creation

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix NNF generation if explicit :ATOMs are used

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

fix add-formula to drop :AND and :OR-symbols before adding clauses

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix macro expansion time confusion in with-index-hash

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

remove debugging output and ensure empty clauses are deleted from CNFs

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix call to minisat solve()

Assumptions don't play well with presolve. Forum answer by Niklas:

"I could repeat the problem and realized that it has to do with one of
the undocumented constraints of the solver-API. More specificly, it
has to do with preprocessing. If you turn that off it gives consistent
results: both turning on the literal as an assumption or as a unit
clause gives an unsatisfiable result.

The cause of this problem is that when you call solve the first time
you specify that the preprocessing should be turned off at the end of
the call. This means that all data-structures that has to do with
preprocessing are deleted, and it is no longer possible to refer to
any of the variables that may have been removed by the preprocessor.
In this case the literal you pass as an assumption was indeed removed.

The way to work around this is to either use preprocessing throughout,
by replacing all calls of the form "solve(xxx, true, true)" with calls
to "solve(xxx)", or to initially turn off all preprocessing, which can
be done with a call to "eliminate(true)" before anything else.

Which alternative works best depends on your application, but as
preprocessing can be pretty unpredictable in some incremental settings
your best bet may be to turn it off.

I hope this helps,"

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix non-cnf formula addition interface

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix with-sat-solver macro to correctly reference *default-sat-backend* at run time

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

(minisat backend ) Return number of queued assumptions from add_assumption

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Also build minisat backend

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix assumption handling in precosat backend

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Add CNF builder convenience functions

WIP, Still broken and incomplete

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

add-clauses convenience function

New method synchronize-backend to allow incremental flushing

Avoid re-creation of the whole problem in the backend during
get-essential-variables computations, with backends that support it (like minisat)

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Add minisat backend to lisp code, make it the default

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Minimalistic minisat header and SWIG integration

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Autotools setup for minisat

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix first line in dimacs format export

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Import minisat2-070721

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Really fix memory issue: Precosat Solver->reset() was actually dysfunction in NDEBUG build

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Fix with-index-hash

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Properly dispose of precosat objects.

The solver destructor does not call reset, probably to save time in satrace competition. Urgs

Signed-off-by: Utz-Uwe Haus <haus@uuhaus.de>

Add get-essential-variables implementation.

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>

Add with-sat-solver and with-index-hash macros.

Signed-off-by: Utz-Uwe Haus <haus@uuhaus.de>

Add dimacs reader/writer

Signed-off-by: Utz-Uwe Haus <haus@uuhaus.de>

Proper garbage collection of foreign objects using trivial-garbage.

Also fix for SBCL (wants .so in foreign library names in the asd file)

Signed-off-by: Utz-Uwe Haus <haus@uuhaus.de>

SWIG wrapper layer and .i file for precosat, minimalistic generic interface

Signed-off-by: Utz-Uwe Haus <haus@uuhaus.de>

Import precosat-465r2-2ce82ba-100514

Signed-off-by: Utz-Uwe Haus <haus@uuhaus.de>

Initial layout

Signed-off-by: Utz-Uwe Haus <haus@uuhaus.de>