1 files changed, 0 insertions, 157 deletions
diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README
deleted file mode 100644
index af71779d5..000000000
--- a/src/prop/minisat/CVC4-README
+++ /dev/null
@@ -1,157 +0,0 @@
-================ CHANGES TO THE ORIGINAL CODE ==================================
-
-The only CVC4 connections passed to minisat are the proxy (defined in sat.h) and
-the context. The context is obtained from the SmtEngine, and the proxy is an 
-intermediary class that has all-access to the SatSolver so as to simplify the 
-interface to (possible) other sat solvers. These two are passed to minisat at 
-construction time and some additional flags are set. We use the SimpSolver 
-solver with simplifications.
-
-To compare with original minisat code in SVN you can compare to revision 6 on 
-the trunk.
-
-The PropEngine then uses the following
-
-// Create the sat solver (this is the proxy, which will create minisat)
-d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options);
-// Add some clauses
-d_cnfStream->convertAndAssert(node);
-// Check for satisfiabilty 
-bool result = d_satSolver->solve();
-
-* Adding theory literals:
-
-The newVar method has been changed from 
-  Var Solver::newVar(bool sign, bool dvar)
-to 
-  Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
-in order to mark the variables as theory literals. For that purpose there is a 
-new boolean array called "theory" that is true or false if the variables is for
-a theory literal.
-
-* Backtracking/Pushing
-
-Backtracking in minisat is performed through the cancelUntil() method, which is 
-now modified to pop the context the appropriate number of times.
-
-Minisat pushes the scope in the newDecisionLevel() method where we appropriately 
-also push the CVC4 context.
-
-* Phase caching
-
-In order to implement phase-caching (RSAT paper) we 
-(1) flag minisat to use the user-provided polarities first by setting the 
-minisat::SimpSolver::polarity_user flag when initializing the solver (in sat.h)
-(2) when a variable is set (in uncheckedEnqueue()) we remember the value in the
-"polarity" table.
-
-* Asserting the theory literals
-
-In the uncheckedEnqueue() method, if the literal is a theory literal (looking 
-in the "theory" table), it is passed to the prop engine thorough the proxy. 
-
-* Theory propagation (checking)
-
-The BCP propagation method was changed from propagate to propagateBool and 
-another method propagateTheory is defined to do the theory propagation. The 
-propagate method now looks like
-
-Clause* Solver::propagate()
-{
-    Clause* confl = NULL;
-
-    while(qhead < trail.size()) {
-      confl = propagateBool();
-      if (confl != NULL) break;
-      confl = propagateTheory();
-      if (confl != NULL) break;
-    }
-
-    return confl;
-}
-
-The propagateBool method will perform the BCP on the newly assigned variables 
-in the trail, and if a conflict is found it will break. Otherwise, the theory 
-propagation is given a chance to check for satisfiability and maybe enqueue some
-additional propagated literals. 
-
-* Conflict resolution
-
-If a conflict is detected during theory propagation we can rely on the minisat
-conflict resolution with a twist. Since a theory can return a conflict where
-all literals are assigned at a level lower than the current level, we must 
-backtrack to the highest level of any literal in the conflict. This is done
-already in the propagateTheory().  
-
-* Clause simplification
-
-Minisat performs some simplifications on the clause database:
-(1) variable elimination
-(2) subsumtion
-
-Subsumtion is complete even with theory reasoning, but eliminating theory 
-literals by resolution might be incomplete:
-
-(x = 0 \vee x = 1) \wedge (x != 1 \vee y = 1) \wedge x = y
-            ^^^^^          ^^^^^^
-              v              ~v
-
-would, after eliminating v, simplify to
-(x = 0) wedge (y = 1) wedge (x = y) which is unsatisfiable
-
-while x = 1, y = 1 is a satisfying assignment for the above.
-
-Minisat does not perform variable elimination on the variables that are marked
-as frozen (in the "frozen", SimSolver.h) table. We put all the theory literals 
-in the frozen table, which solves the incompleteness problem. 
-
-================ NOTES =========================================================
-
-* Accessing the internals of the SAT solver
-
-The non-public parts of the SAT solver are accessed via the static methods in 
-the SatSolver class. SatSolverProxy is declared as a friend of the 
-SatSolver and has all-privileges access to the internals -- use with care!!!
-
-* Clause Database and CNF
-
-The clause database consists of two parts:
-
-    vec<Clause*>        clauses;          // List of problem clauses.
-    vec<Clause*>        learnts;          // List of learnt clauses.
-
-Clauses is the original problem clauses, and learnts are the clauses learned 
-during the search. I have disabled removal of satisfied problem clauses by 
-setting the remove_satisfied flag to false.
-
-The learnt clauses get removed every once in a while by removing the half of
-clauses with the low activity (reduceDB())
-
-Since the clause database backtracks with the SMT solver, the CNF cache should
-be context dependent and everything will be in sync. 
-
-* Adding a Clause
-
-The only method in the interface that allows addition of clauses in MiniSAT is
-
-    bool Solver::addClause(vec<Lit>& ps),
-
-but it only adds the problem clauses. 
-
-In order to add the clauses to the removable database the interface is now 
-
-    bool Solver::addClause(vec<Lit>& ps, bool removable).      
-
-Clauses added with removable=true might get removed by the SAT solver when 
-compacting the database.
-
-The question is whether to add the propagation/conflict lemmas as removable or 
-not?
-
-* Literal Activities
-
-We do not backtrack literal activities. This does not semantically change the 
-equivalence of the context, but does change solve times if the same problem is
-run several times.
-
-* Do we need to assign literals that only appear in satisfied clauses?