1 files changed, 157 insertions, 0 deletions
diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README
new file mode 100644
index 000000000..af71779d5
--- /dev/null
+++ b/src/prop/minisat/CVC4-README
@@ -0,0 +1,157 @@
+================ 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?