| 37dc6c6 | Niklas Sorensson | 25 September 2013, 12:16:18 UTC | Support returning actual peak-memory instead of reverting to current usage | 25 September 2013, 12:16:18 UTC |
| cd3a2d6 | Niklas Sorensson | 19 November 2012, 13:50:09 UTC | Also relocate clauses on the subsumption queue. | 19 November 2012, 13:50:09 UTC |
| 386e4f3 | Niklas Sorensson | 31 October 2012, 12:20:45 UTC | Silence DIMACS warnings by default. Added a -strict flag that checks correctness of "p cnf" line. | 31 October 2012, 12:20:45 UTC |
| 080d3db | Niklas Sorensson | 29 March 2012, 15:15:59 UTC | Move the random-generator to a more generic location. | 29 March 2012, 15:15:59 UTC |
| 149205a | Niklas Sorensson | 16 March 2012, 15:11:35 UTC | Introduce a minimum limit for learned clauses. | 16 March 2012, 15:11:35 UTC |
| 1732cff | Niklas Sorensson | 08 March 2012, 11:26:04 UTC | Introduce literal sets (LSet) and use it to store 'conflict'. | 08 March 2012, 11:26:04 UTC |
| f7cd4c6 | Niklas Sorensson | 08 March 2012, 11:25:30 UTC | New specialized 'addClause' for 4-clauses. | 08 March 2012, 11:25:30 UTC |
| 146346b | Niklas Sorensson | 27 February 2012, 12:15:25 UTC | Fix more parentheses warnings. | 27 February 2012, 12:19:12 UTC |
| d699be0 | Niklas Sorensson | 27 February 2012, 11:36:43 UTC | Patch submitted by Niklas Een. Support for defining minisat constants as real constants rather than macro's. This should be reevaluated from a performance perspective; maybe it is fine to remove completely the macro variants at this point. Also some patches for that removes gcc's -Wparentheses warnings. | 27 February 2012, 12:15:47 UTC |
| 369fc3f | Niklas Sorensson | 05 December 2011, 15:55:56 UTC | Fix an ancient bug in 'SimpSolver::implied()'. | 05 December 2011, 15:55:56 UTC |
| a1f981a | Niklas Sorensson | 11 October 2011, 15:39:54 UTC | Revert "Extend a couple of parsing functions to treat newline as significant." This reverts commit 4d3aa55f8e8c82e14352d25c43dc675bad750158. | 11 October 2011, 15:39:54 UTC |
| 30909ac | Niklas Sorensson | 05 October 2011, 11:17:41 UTC | Add iterators to IntMap. | 05 October 2011, 11:17:41 UTC |
| 1d2e1fc | Niklas Sorensson | 26 September 2011, 13:29:33 UTC | Simple way to disable extending models. | 26 September 2011, 13:29:33 UTC |
| 0c0bb0d | Niklas Sorensson | 26 September 2011, 12:48:24 UTC | Add preliminary support for "releaseVar()" method. Can be used to recycle variables that is guaranteed to not be referred to in the future (for instance activation variables for temporary clauses). | 26 September 2011, 12:48:24 UTC |
| 1e0fd32 | Niklas Sorensson | 22 September 2011, 12:03:37 UTC | Generalize remove/find to work on vector-like types with unsigned size. | 22 September 2011, 12:03:37 UTC |
| 6820591 | Niklas Sorensson | 22 September 2011, 12:02:44 UTC | Revert to using copy constructor in Vec::push() rather than assignment. | 22 September 2011, 12:02:44 UTC |
| 4d3aa55 | Niklas Sorensson | 12 September 2011, 11:04:02 UTC | Extend a couple of parsing functions to treat newline as significant. | 12 September 2011, 11:04:02 UTC |
| 5ecc5b0 | Niklas Sorensson | 10 August 2011, 10:48:04 UTC | Main: Allow writing dimacs at the end of interrupted solve. To get the old behavior a new command line flag was introduced to not call solve after preprocessing (-no-solve). | 10 August 2011, 10:48:04 UTC |
| 8d018ed | Niklas Sorensson | 10 August 2011, 10:24:10 UTC | Add a remove method to the Heap class. | 10 August 2011, 10:27:02 UTC |
| 94aef63 | Niklas Sorensson | 30 June 2011, 14:25:00 UTC | Add an 'implies()' method that allows to check result of one propagation. | 08 July 2011, 14:34:21 UTC |
| 5a01f08 | Niklas Sorensson | 06 July 2011, 15:02:49 UTC | Change the heap implementation to use IntMaps for the heap-indices. | 08 July 2011, 14:34:15 UTC |
| 9aa56a7 | Niklas Sorensson | 06 July 2011, 15:02:25 UTC | Add the 'has()' operation to IntMaps. | 06 July 2011, 15:02:25 UTC |
| 26f8354 | Niklas Sorensson | 01 July 2011, 15:07:38 UTC | Complete re-factoring to use VMaps for Solver data. | 01 July 2011, 15:07:38 UTC |
| d4fea75 | Niklas Sorensson | 01 July 2011, 13:28:51 UTC | Use VMap for variable activity. | 01 July 2011, 13:28:51 UTC |
| a451687 | Niklas Sorensson | 01 July 2011, 13:19:08 UTC | Add new IntMap class: essentially a restricted vector parametrized on keys. | 01 July 2011, 13:19:08 UTC |
| c008424 | Niklas Sorensson | 01 July 2011, 13:17:14 UTC | Parametrize vector class with respect to the "size-type". | 01 July 2011, 13:17:14 UTC |
| 7de6232 | Niklas Sorensson | 30 May 2011, 14:13:01 UTC | Lazier removal of deleted clauses in 'propagate()'. This may need to be further evaluated from a performance perspective. | 30 May 2011, 14:13:01 UTC |
| 5c24ca6 | Niklas Sorensson | 25 May 2011, 16:20:55 UTC | Forgot to remove declaration. | 25 May 2011, 16:20:55 UTC |
| fc702b3 | Niklas Sorensson | 25 May 2011, 15:34:48 UTC | Refactor garbage collection slightly. | 25 May 2011, 15:34:48 UTC |
| 33def9c | Niklas Sorensson | 18 May 2011, 15:50:51 UTC | Introduce new simpler freeze/thaw interface to SimpSolver. The old 'setFrozen()' method will be kept for a while, but it is not safe to mix the two freeze APIs. | 18 May 2011, 15:50:51 UTC |
| 3652e21 | Niklas Sorensson | 06 May 2011, 13:04:47 UTC | Don't allocate StreamBuffers on the stack. | 06 May 2011, 13:04:47 UTC |
| 4c4b466 | Niklas Sorensson | 06 May 2011, 11:55:13 UTC | Remove a warning on non-posix Windows builds. | 06 May 2011, 11:55:13 UTC |
| a74ac81 | Niklas Sorensson | 06 May 2011, 11:48:49 UTC | Only call "limitXXX" if the user actually set a limit. This avoids warning messages on architectures that dont's support the setrlimit calls. | 06 May 2011, 11:48:49 UTC |
| 93b1810 | Niklas Sorensson | 28 April 2011, 16:33:33 UTC | Portability fixes for resources, signals, etc + some cleanups. | 28 April 2011, 16:33:33 UTC |
| d5b3bf1 | Niklas Sorensson | 26 September 2010, 14:27:58 UTC | Added new CMake build system. | 18 April 2011, 14:27:54 UTC |
| 3ad9f5d | Niklas Sorensson | 15 April 2011, 11:54:58 UTC | Changed 'litRedundant()' to more efficient version with negative caching. This is more or less an obfuscation of the simple recursive implementation. The reason this is preferred at the moment is that the stack usage of the explicitly recursive version is unpredictable an may cause stack overflow. In the future it may be worth changing to the saner pure recursive implementation as it even may be faster with some compilers. Note also that the level-based pruning has been removed as it does not seem to make a real difference with this implementation. | 15 April 2011, 14:58:01 UTC |
| cec52e9 | Niklas Sorensson | 07 April 2011, 14:10:39 UTC | Added a 'printStats()' method to the Solver class. This could probably be moved to some "utilities" module, since it does not depend on any Solver internals. | 07 April 2011, 14:10:39 UTC |
| 054ac66 | Niklas Sorensson | 28 March 2011, 14:06:34 UTC | Add user-level iterators for clauses and assignments. | 28 March 2011, 14:06:34 UTC |
| 0b2667a | Niklas Sorensson | 28 March 2011, 13:32:55 UTC | Add 'install-debug' target to buildsystem. | 28 March 2011, 13:32:55 UTC |
| 7d0d749 | Niklas Sorensson | 16 March 2011, 16:52:26 UTC | Also handle the SIGTERM signal. | 16 March 2011, 16:52:26 UTC |
| eca5b99 | Niklas Sorensson | 23 February 2011, 15:32:45 UTC | Change gitignore to exclude everything in "build" subdirectory. | 23 February 2011, 15:32:45 UTC |
| b06c247 | Niklas Sorensson | 21 February 2011, 13:30:20 UTC | Clean up the ClauseAllocator slightly. | 21 February 2011, 13:31:17 UTC |
| b4eb192 | Niklas Sorensson | 21 February 2011, 12:38:50 UTC | Make relocation code nicer by a new "copy-constructor" for clauses. | 21 February 2011, 13:31:11 UTC |
| 9e99301 | Niklas Sorensson | 21 February 2011, 12:48:34 UTC | Buildsystem: fix dependency generation to separate build-types. | 21 February 2011, 12:48:34 UTC |
| be23388 | Niklas Sorensson | 07 February 2011, 15:39:41 UTC | More minor build system tweaks. | 07 February 2011, 15:39:41 UTC |
| 71875c1 | Niklas Sorensson | 07 February 2011, 15:12:52 UTC | Also use LDFLAGS when building shared libraries. | 07 February 2011, 15:12:52 UTC |
| 8f7bb56 | Niklas Sorensson | 01 February 2011, 13:26:02 UTC | Always respect user polarities. Note that this changes the interface for setting variable polarities. | 01 February 2011, 13:26:02 UTC |
| 5ae731c | Niklas Sorensson | 01 February 2011, 10:34:00 UTC | Minor fix to build core executable in static and profile versions. | 01 February 2011, 10:34:00 UTC |
| 330a696 | Niklas Sorensson | 27 January 2011, 13:24:42 UTC | Add library files to gitignore. | 27 January 2011, 13:24:42 UTC |
| 2e80302 | Niklas Sorensson | 27 January 2011, 13:23:47 UTC | Fix dependencies for shared library links in build system. | 27 January 2011, 13:23:47 UTC |
| dd1b19f | Niklas Sorensson | 24 January 2011, 12:39:57 UTC | Some fixes to the build system mostly related to dynamic linking. Thanks to Michael Tautschnig <mt@debian.org> suggesting the fixes. | 24 January 2011, 12:39:57 UTC |
| ed456c5 | Niklas Sorensson | 13 January 2011, 14:38:46 UTC | Add install-bin target to Makefile. | 13 January 2011, 14:38:46 UTC |
| eadc3ef | Niklas Sorensson | 11 January 2011, 15:17:25 UTC | Updated README file with some instructions on configure/build/install. | 11 January 2011, 15:17:25 UTC |
| 6736d2f | Niklas Sorensson | 10 January 2011, 13:22:23 UTC | More build system clean ups. | 10 January 2011, 13:22:23 UTC |
| cf61320 | Niklas Sorensson | 07 January 2011, 15:29:54 UTC | Adding clean target to build system. | 07 January 2011, 15:29:54 UTC |
| 36ca1c7 | Niklas Sorensson | 07 January 2011, 13:03:48 UTC | More buildsystem work. Mainly fixes a problem with builds that needs multiple modes (release, dynamic, etc). The current solution is ugly (cut'n'paste), but I haven't found something better that works yet. | 07 January 2011, 13:03:48 UTC |
| f00fca8 | Niklas Sorensson | 07 January 2011, 13:00:29 UTC | Fix warning + use better approach to disallow copying. | 07 January 2011, 13:00:29 UTC |
| 5a71d18 | Niklas Sorensson | 07 January 2011, 12:56:31 UTC | Fix various warnings. | 07 January 2011, 12:56:31 UTC |
| 25c9975 | Niklas Sorensson | 07 January 2011, 12:56:12 UTC | Bugfix: really use the passed assumptions in 'toDimacs()'. | 07 January 2011, 12:56:12 UTC |
| b647459 | Niklas Sorensson | 03 January 2011, 13:27:44 UTC | Add install target to Makefile. | 03 January 2011, 13:27:44 UTC |
| 09cad4f | Niklas Sorensson | 18 December 2010, 17:25:04 UTC | Updated the .gitignore file. | 18 December 2010, 17:25:04 UTC |
| bf3176c | Niklas Sorensson | 18 December 2010, 17:21:58 UTC | Initial support for build configuration. | 18 December 2010, 17:21:58 UTC |
| 4e6288d | Niklas Sorensson | 16 December 2010, 16:21:18 UTC | First attempt at shared library support. | 16 December 2010, 16:21:18 UTC |
| 1328a8d | Niklas Sorensson | 10 December 2010, 18:01:22 UTC | Refactoring + new GNU Make system Moved all source files to a "minisat" subdirectory and changed includes to take this into account. NOTE: all usages of MiniSat will also have to adapt to this new directory layout. | 10 December 2010, 18:01:22 UTC |
| 6d59595 | Niklas Sorensson | 23 November 2010, 14:51:40 UTC | Added a .gitignore file. | 23 November 2010, 14:51:40 UTC |
| cfae873 | Niklas Sorensson | 06 September 2010, 15:28:25 UTC | Fix build and minor cleanup of System module. | 06 September 2010, 15:28:25 UTC |
| a074316 | Niklas Sorensson | 02 September 2010, 12:36:00 UTC | Portability-patch contributed by Michael Tautschnig. | 02 September 2010, 12:36:00 UTC |
| 9bd8749 | Niklas Sorensson | 12 July 2010, 08:28:57 UTC | Fix typo in BSD-specific code. | 12 July 2010, 08:28:57 UTC |
| eb01ad6 | Niklas Sorensson | 10 July 2010, 16:07:36 UTC | Remove a file that is not used in main branch. | 10 July 2010, 16:07:36 UTC |
| d0dd522 | Niklas Sorensson | 10 July 2010, 06:35:36 UTC | Add a first version of release notes. | 10 July 2010, 06:35:36 UTC |
| d4c8795 | Niklas Sorensson | 10 July 2010, 06:34:27 UTC | Fixing weirdness of RegionAllocator. | 10 July 2010, 06:34:27 UTC |
| fa6a96c | Niklas Sorensson | 23 June 2010, 14:31:12 UTC | Split memory-usage functions into current and peak versions. This needs to be further tested/improved on different platforms. | 23 June 2010, 14:31:12 UTC |
| 1cc7ae6 | Niklas Sorensson | 10 June 2010, 13:20:46 UTC | Non-branching implementations of ternary conjunction/disjunction. This is essentially a truth-table encoded into a single word, and look-up implemented as a single shift and mask. | 10 June 2010, 13:20:46 UTC |
| 272eea5 | Niklas Sorensson | 22 May 2010, 12:56:02 UTC | In 'toDimacs()', handle case where solver is in a contradictory state. | 22 May 2010, 12:56:02 UTC |
| 909de43 | Niklas Sorensson | 10 May 2010, 16:41:26 UTC | Move DIMACS writing function from SimpSolver to Solver. | 10 May 2010, 16:41:26 UTC |
| a4ed186 | Niklas Sorensson | 02 May 2010, 18:50:55 UTC | Fix exit-values for non optimized builds. | 02 May 2010, 18:50:55 UTC |
| 7fde68d | Niklas Sorensson | 10 April 2010, 13:11:12 UTC | Added some missing comments. | 10 April 2010, 13:11:12 UTC |
| cf79f61 | Niklas Sorensson | 10 April 2010, 13:07:09 UTC | First tweak of the README file. | 10 April 2010, 13:07:09 UTC |
| 85bf53a | Niklas Sorensson | 10 April 2010, 13:04:52 UTC | Make it it possible to use traditional restart sequence. | 10 April 2010, 13:04:52 UTC |
| 2410de9 | Niklas Sorensson | 04 August 2009, 18:39:52 UTC | Add possibility to control the application of phase-saving. There are three levels: 0 - turn it off 1 - save phases only for assignments not on the conflicting level 2 - save all phases | 10 April 2010, 12:18:42 UTC |
| e7c0ec1 | Niklas Sorensson | 10 April 2010, 11:59:57 UTC | Made Solver verbosity default 0. | 10 April 2010, 11:59:57 UTC |
| cc10435 | Niklas Sorensson | 10 April 2010, 11:41:43 UTC | Correct indentation for help-printing of boolean options. | 10 April 2010, 11:41:43 UTC |
| 85e2be1 | Niklas Sorensson | 18 March 2010, 13:57:35 UTC | Comment on the remaining potential overflow in vectors. | 18 March 2010, 13:57:35 UTC |
| 8fa1cf3 | Niklas Sorensson | 15 March 2010, 18:29:08 UTC | Fix unused variable warning. | 15 March 2010, 18:29:08 UTC |
| 327c1a7 | Niklas Sorensson | 13 March 2010, 16:05:17 UTC | Let the memory-limit option be given in megabytes. | 13 March 2010, 16:05:17 UTC |
| 20f7981 | Niklas Sorensson | 12 March 2010, 16:16:47 UTC | More overflow detections for capacities. | 12 March 2010, 16:16:47 UTC |
| 6c457d6 | Niklas Sorensson | 12 March 2010, 15:46:12 UTC | Make single argument constructors explicit to avoid unwanted conversions. | 12 March 2010, 15:46:12 UTC |
| d752954 | Niklas Sorensson | 10 March 2010, 16:54:15 UTC | Add a method to query vector capacities. | 10 March 2010, 16:54:15 UTC |
| 732b418 | Niklas Sorensson | 10 March 2010, 16:53:55 UTC | Further streamlining and sanity-checking in Vec.h. | 10 March 2010, 16:53:55 UTC |
| 72b895e | Niklas Sorensson | 08 March 2010, 14:58:36 UTC | More Vec-fixes. | 08 March 2010, 15:00:48 UTC |
| 2d19964 | Niklas Sorensson | 07 March 2010, 17:51:09 UTC | In 'OccLists::cleanAll()', avoid cleaning the same variable twice. | 07 March 2010, 17:51:09 UTC |
| 60e4d74 | Niklas Sorensson | 07 March 2010, 17:43:59 UTC | Fix a warning. | 07 March 2010, 17:43:59 UTC |
| d08fb27 | Niklas Sorensson | 07 March 2010, 17:00:26 UTC | Fix closing bracket of namespaces. | 07 March 2010, 17:00:26 UTC |
| 2bbdafc | Niklas Sorensson | 04 March 2010, 17:16:48 UTC | Simple variant of RegionAllocator that does not rely on vectors. This makes the whole 32-bit range of clause-references available as opposed to the previous vector based solution that had a smaller limit because of the fact that vecor indices uses signed integers. | 04 March 2010, 17:16:48 UTC |
| 6f17434 | Niklas Sorensson | 04 March 2010, 15:29:09 UTC | Slight improvement to clause garbage collection. Since we have an estimation of the size of all active clauses we can use that to initialize the size of the target region. This avoids some reallocations as this target otherwise grows from the minimum up to the needed size. Note however that it is just an estimation at the moment and the actual needed space is usually smaller. There are couple of reasons for this. Firstly, during preprocessing some clauses are destructively shrunk and this is not accounted for. Secondly, the extra clause-field for abstractions can be dropped in between collections and this also reduces the total needed space. | 04 March 2010, 15:29:09 UTC |
| 66d833c | Niklas Sorensson | 03 March 2010, 13:33:33 UTC | Avoid overflow in calculation of vector capacity. | 03 March 2010, 13:33:33 UTC |
| 267c943 | Niklas Sorensson | 02 March 2010, 18:07:48 UTC | Initial support for passing assumptions to 'toDimacs()'-method. Not sure how well this works yet, this method is kindof fragile for some reason. Would be good to reimplement. | 02 March 2010, 18:07:48 UTC |
| 6074c4e | Niklas Sorensson | 28 February 2010, 15:57:11 UTC | Tweak the signal handling in the Main's. Previously it was not possible to interrupt MiniSat until after parsing when MiniSat starts polling the asynchronous interrupt. Now we use a signal handler that forcibly quits until this point. These interrupt features maybe should not be exposed in the simple MiniSat main, but it is still helpful as a way to test that the features work. I will keep it at least until I have some other test-cases for this. | 28 February 2010, 15:57:11 UTC |
| 1db1c13 | Niklas Sorensson | 28 February 2010, 15:22:00 UTC | Update the copyright-lines. | 28 February 2010, 15:22:00 UTC |
| 45566db | Niklas Sorensson | 28 February 2010, 14:20:48 UTC | Remove some scripts that should not be part of the repository (for now). | 28 February 2010, 14:20:48 UTC |
