32f040fa45
* Makefile.am: Add picosat to subdirs. * configure.ac: Add picosat/Makefile to AC_CONFIG_FILES. * README: Add picosat/ in the list of directories. * debian/copyright: Add picosat licence and details. * picosat/Makefile.am: Implement Makefile.am in picosat directory. * spot/Makefile.am: Tell the compiler to add libpico.la into libspot.la. * picosat/LICENSE: Add picosat licence. * picosat/NEWS: Add picosat NEWS. * picosat/VERSION: Add picosat VERSION. * picosat/picosat.c: Add picosat c file. * picosat/picosat.h: Add picosat header file. * spot/misc/satsolver.cc: Update functions. * spot/misc/satsolver.hh: Add documentation, clean code, change some functions visibility and separate templates functions. * spot/twaalgos/dtbasat.cc: Update dtba_to_sat function. * spot/twaalgos/dtwasat.cc: Update dtwa_to_sat function.
162 lines
4.6 KiB
Text
162 lines
4.6 KiB
Text
news for release 965 since 959
|
|
------------------------------
|
|
|
|
* ADC code works again (spotted by Himanshu Jain)
|
|
* include into R projects (with Christoph Muessel) (--rcode)
|
|
* fixed 'undefined' + 'ptrdiff_' issues (thanks to Christoph Muessel)
|
|
* added 'picosat_set_interrupt' and '-a <alarm>' command line option
|
|
* fixed various issues pointed out by Stefan Hengelein:
|
|
- fixed incremental usage of 'picosat_adjust'
|
|
- added CPP fixes (STATS, NO_BINARY_CLAUSE versus TRACE mix-ups)
|
|
- removed redundant explicit set to zero on reset
|
|
* fixed various usage bugs with 'picomus' (thanks to Stefan Hengelein)
|
|
* removed '-fno-strict-aliasing' (thanks to Jerry James)
|
|
|
|
news for release 959 since 953
|
|
------------------------------
|
|
|
|
* fixed header comments
|
|
|
|
* fixed minor compilation issues
|
|
|
|
* fixed unitialized memory access problem for 'picosat_deref_partial'
|
|
and another issue with partial models
|
|
|
|
* added 'picosat_add_arg' and 'picosat_add_lits'
|
|
|
|
* '--plain' and 'picosat_set_plain' to disable failed literal probing
|
|
|
|
* new '#define PICOSAT_REENTRANT_API' in 'picosat.h'
|
|
|
|
* added manager so no more global variables
|
|
(allows multiple instances, requires manager object)
|
|
|
|
news for release 951 since 941
|
|
------------------------------
|
|
|
|
* cleaned up code (based on comments by Donald Knuth)
|
|
|
|
* lreduce=O(conflicts^.5)
|
|
|
|
* added 'picosat_visits' and 'picosat_decisions'
|
|
|
|
* added '--partial' command line option
|
|
|
|
* added 'picosat_deref_partial' and 'picosat_save_original_clauses'
|
|
|
|
* added 'picomcs' as example for MSS computation
|
|
|
|
news for release 941 since 936
|
|
------------------------------
|
|
|
|
* added 'picogcnf'
|
|
|
|
* added All-SAT mode ('--all' command line option)
|
|
|
|
* statistics include time spent in failed literal preprocessing (probing)
|
|
|
|
* 'picosat_failed_context' for 'push & pop'
|
|
(and tested failed assumptions for 'push & pop')
|
|
|
|
* 'picosat_simplify' for forced garbage collection
|
|
|
|
* undefined NFL, defined NADC (= failed literals on, ADC's off)
|
|
|
|
* 'picosat_push' and 'picosat_pop' (beta version)
|
|
|
|
* fixed some issues related to binary clause handling and
|
|
generating list of failed assumptions
|
|
|
|
news for release 936 since 935
|
|
------------------------------
|
|
|
|
* simple minimal unsatisfiable core (MUS) extractor 'picomus'
|
|
(example for using 'picosat_mus_assumptions' and 'picosat_coreclause')
|
|
|
|
* added 'picosat_mus_assumptions'
|
|
|
|
* added 'picosat_{set_}propagations'
|
|
|
|
* new 'int' return value for 'picosat_enable_trace_generation' to
|
|
check for trace code being compiled
|
|
|
|
news for release 935 since 926
|
|
------------------------------
|
|
|
|
* added 'picosat_failed_assumptions' (plural)
|
|
|
|
* new '-A <failedlits>' command line option
|
|
|
|
* fixed failed assumption issues
|
|
|
|
* added 'picosat_remove_learned'
|
|
|
|
* added 'picosat_reset_{phases,scores}'
|
|
|
|
* added 'picosat_set_less_important_lit'
|
|
|
|
* added 'picosat_res'
|
|
|
|
news for release 926 since 846
|
|
------------------------------
|
|
|
|
* random initial phase (API of 'picosat_set_default_phase' changed)
|
|
|
|
* fixed accumulative failed assumption (multiple times)
|
|
|
|
* fixed missing original clause in core generation with assumptions
|
|
|
|
* fixed debugging code for memory allocation
|
|
|
|
* shared library in addition to static library
|
|
|
|
* removed potential UNKNOWN result without decision limit
|
|
|
|
* added picosat_set_more_important_lit
|
|
|
|
* added picosat_coreclause
|
|
|
|
* propagation of binary clauses until completion
|
|
|
|
* fixed API usage 'assume;sat;sat'
|
|
|
|
* literals move to front (LMTF) during traversal of visited clauses
|
|
|
|
* switched from inner/outer to Luby style restart scheduling
|
|
|
|
* less agressive reduce schedule
|
|
|
|
* replaced watched literals with head and tail pointers
|
|
|
|
* add 'picosat_failed_assumption', which allows to avoid tracing and core
|
|
generation, if one is only interested in assumptions in the core
|
|
|
|
* fixed a BUG in the generic iterator code of clauses
|
|
(should rarely happen unless you use a very sophisticated malloc lib)
|
|
|
|
news for release 846 since 632
|
|
------------------------------
|
|
|
|
* cleaned up assumption handling (actually removed buggy optimization)
|
|
|
|
* incremental core generation
|
|
|
|
* experimental 'all different constraint' handling as in our FMCAD'08 paper
|
|
|
|
* new API calls:
|
|
|
|
- picosat_add_ado_lit (add all different object literal)
|
|
- picosat_deref_top_level (deref top level assignment)
|
|
- picosat_changed (check whether extension was possible)
|
|
- picosat_measure_all_calls (per default do not measure adding time)
|
|
- picosat_set_prefix (set prefix for messages)
|
|
|
|
* 64 bit port (and compilation options)
|
|
|
|
* optional NVSIDS visualization code
|
|
|
|
* resource controlled failed literal implementation
|
|
|
|
* disconnect long clauses satisfied at lower decision level
|
|
|
|
* controlling restarts
|