Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Moved Minisat solver in a separate sub-folder. Adjusted build accordi…

…ngly
  • Loading branch information...
commit 709479ef9bb0d276b75b774740594a8b24fa78b1 1 parent 3ed4509
@mwolf76 authored
Showing with 0 additions and 112 deletions.
  1. +0 −79 src/sat/doc/ReleaseNotes-2.2.0.txt
  2. 0  src/sat/{ → minisat}/core/Main.cc
  3. 0  src/sat/{ → minisat}/core/Solver.cc
  4. 0  src/sat/{ → minisat}/core/Solver.hh
  5. 0  src/sat/{ → minisat}/core/SolverTypes.hh
  6. 0  src/sat/{ → minisat}/mtl/Alg.hh
  7. 0  src/sat/{ → minisat}/mtl/Alloc.hh
  8. 0  src/sat/{ → minisat}/mtl/Heap.hh
  9. 0  src/sat/{ → minisat}/mtl/IntTypes.hh
  10. 0  src/sat/{ → minisat}/mtl/Map.hh
  11. 0  src/sat/{ → minisat}/mtl/Queue.hh
  12. 0  src/sat/{ → minisat}/mtl/Set.hh
  13. 0  src/sat/{ → minisat}/mtl/Sort.hh
  14. 0  src/sat/{ → minisat}/mtl/Vec.hh
  15. 0  src/sat/{ → minisat}/mtl/XAlloc.hh
  16. 0  src/sat/{ → minisat}/simp/Main.cc
  17. 0  src/sat/{ → minisat}/simp/SimpSolver.cc
  18. 0  src/sat/{ → minisat}/simp/SimpSolver.hh
  19. 0  src/sat/{ → minisat}/utils/Options.cc
  20. 0  src/sat/{ → minisat}/utils/Options.hh
  21. 0  src/sat/{ → minisat}/utils/ParseUtils.hh
  22. 0  src/sat/{ → minisat}/utils/System.cc
  23. 0  src/sat/{ → minisat}/utils/System.hh
  24. 0  src/sat/{proof → }/proof.cc
  25. 0  src/sat/{proof → }/proof.hh
  26. +0 −9 src/sat/utils/solverlogger.cc
  27. +0 −24 src/sat/utils/solverlogger.hh
View
79 src/sat/doc/ReleaseNotes-2.2.0.txt
@@ -1,79 +0,0 @@
-Release Notes for MiniSat 2.2.0
-===============================
-
-Changes since version 2.0:
-
- * Started using a more standard release numbering.
-
- * Includes some now well-known heuristics: phase-saving and luby
- restarts. The old heuristics are still present and can be activated
- if needed.
-
- * Detection/Handling of out-of-memory and vector capacity
- overflow. This is fairly new and relatively untested.
-
- * Simple resource controls: CPU-time, memory, number of
- conflicts/decisions.
-
- * CPU-time limiting is implemented by a more general, but simple,
- asynchronous interruption feature. This means that the solving
- procedure can be interrupted from another thread or in a signal
- handler.
-
- * Improved portability with respect to building on Solaris and with
- Visual Studio. This is not regularly tested and chances are that
- this have been broken since, but should be fairly easy to fix if
- so.
-
- * Changed C++ file-extention to the less problematic ".cc".
-
- * Source code is now namespace-protected
-
- * Introducing a new Clause Memory Allocator that brings reduced
- memory consumption on 64-bit architechtures and improved
- performance (to some extent). The allocator uses a region-based
- approach were all references to clauses are represented as a 32-bit
- index into a global memory region that contains all clauses. To
- free up and compact memory it uses a simple copying garbage
- collector.
-
- * Improved unit-propagation by Blocking Literals. For each entry in
- the watcher lists, pair the pointer to a clause with some
- (arbitrary) literal from the clause. The idea is that if the
- literal is currently true (i.e. the clause is satisfied) the
- watchers of the clause does not need to be altered. This can thus
- be detected without touching the clause's memory at all. As often
- as can be done cheaply, the blocking literal for entries to the
- watcher list of a literal 'p' is set to the other literal watched
- in the corresponding clause.
-
- * Basic command-line/option handling system. Makes it easy to specify
- options in the class that they affect, and whenever that class is
- used in an executable, parsing of options and help messages are
- brought in automatically.
-
- * General clean-up and various minor bug-fixes.
-
- * Changed implementation of variable-elimination/model-extension:
-
- - The interface is changed so that arbitrary remembering is no longer
- possible. If you need to mention some variable again in the future,
- this variable has to be frozen.
-
- - When eliminating a variable, only clauses that contain the variable
- with one sign is necessary to store. Thereby making the other sign
- a "default" value when extending models.
-
- - The memory consumption for eliminated clauses is further improved
- by storing all eliminated clauses in a single contiguous vector.
-
- * Some common utility code (I/O, Parsing, CPU-time, etc) is ripped
- out and placed in a separate "utils" directory.
-
- * The DIMACS parse is refactored so that it can be reused in other
- applications (not very elegant, but at least possible).
-
- * Some simple improvements to scalability of preprocessing, using
- more lazy clause removal from data-structures and a couple of
- ad-hoc limits (the longest clause that can be produced in variable
- elimination, and the longest clause used in backward subsumption).
View
0  src/sat/core/Main.cc → src/sat/minisat/core/Main.cc
File renamed without changes
View
0  src/sat/core/Solver.cc → src/sat/minisat/core/Solver.cc
File renamed without changes
View
0  src/sat/core/Solver.hh → src/sat/minisat/core/Solver.hh
File renamed without changes
View
0  src/sat/core/SolverTypes.hh → src/sat/minisat/core/SolverTypes.hh
File renamed without changes
View
0  src/sat/mtl/Alg.hh → src/sat/minisat/mtl/Alg.hh
File renamed without changes
View
0  src/sat/mtl/Alloc.hh → src/sat/minisat/mtl/Alloc.hh
File renamed without changes
View
0  src/sat/mtl/Heap.hh → src/sat/minisat/mtl/Heap.hh
File renamed without changes
View
0  src/sat/mtl/IntTypes.hh → src/sat/minisat/mtl/IntTypes.hh
File renamed without changes
View
0  src/sat/mtl/Map.hh → src/sat/minisat/mtl/Map.hh
File renamed without changes
View
0  src/sat/mtl/Queue.hh → src/sat/minisat/mtl/Queue.hh
File renamed without changes
View
0  src/sat/mtl/Set.hh → src/sat/minisat/mtl/Set.hh
File renamed without changes
View
0  src/sat/mtl/Sort.hh → src/sat/minisat/mtl/Sort.hh
File renamed without changes
View
0  src/sat/mtl/Vec.hh → src/sat/minisat/mtl/Vec.hh
File renamed without changes
View
0  src/sat/mtl/XAlloc.hh → src/sat/minisat/mtl/XAlloc.hh
File renamed without changes
View
0  src/sat/simp/Main.cc → src/sat/minisat/simp/Main.cc
File renamed without changes
View
0  src/sat/simp/SimpSolver.cc → src/sat/minisat/simp/SimpSolver.cc
File renamed without changes
View
0  src/sat/simp/SimpSolver.hh → src/sat/minisat/simp/SimpSolver.hh
File renamed without changes
View
0  src/sat/utils/Options.cc → src/sat/minisat/utils/Options.cc
File renamed without changes
View
0  src/sat/utils/Options.hh → src/sat/minisat/utils/Options.hh
File renamed without changes
View
0  src/sat/utils/ParseUtils.hh → src/sat/minisat/utils/ParseUtils.hh
File renamed without changes
View
0  src/sat/utils/System.cc → src/sat/minisat/utils/System.cc
File renamed without changes
View
0  src/sat/utils/System.hh → src/sat/minisat/utils/System.hh
File renamed without changes
View
0  src/sat/proof/proof.cc → src/sat/proof.cc
File renamed without changes
View
0  src/sat/proof/proof.hh → src/sat/proof.hh
File renamed without changes
View
9 src/sat/utils/solverlogger.cc
@@ -1,9 +0,0 @@
-// -*- C++ -*-
-// solverlogger.cc: Output operators for various solver types (Lit, Clause, ...)
-// Author: Alberto Griggio
-
-#include "utils/solverlogger.hh"
-
-namespace Minisat {
-
-}
View
24 src/sat/utils/solverlogger.hh
@@ -1,24 +0,0 @@
-// -*- C++ -*-
-// solverlogger.h: Output operators for various solver types (Lit, Clause, ...)
-// Author: Alberto Griggio
-// $Id: solverlogger.h,v 1.1 2007-06-06 09:03:55 nusmv Exp $
-
-#ifndef SOLVERLOGGER_H_INCLUDED
-#define SOLVERLOGGER_H_INCLUDED
-
-#include <ostream>
-#include "Vec.hh"
-#include "SolverTypes.hh"
-
-namespace Minisat {
-
- using std::ostream;
-
- ostream &operator<<(ostream &out, const Lit &lit);
- ostream &operator<<(ostream &out, const Clause *clause);
- ostream &operator<<(ostream &out, const Clause &clause);
- ostream &operator<<(ostream &out, const vec<Lit> &lits);
-
-} // namespace msat
-
-#endif // SOLVERLOGGER_H_INCLUDED
Please sign in to comment.
Something went wrong with that request. Please try again.