From e87c14798b99ccb586751d291b0eeb3208265bd8 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 25 May 2010 05:30:40 +0000
Subject: Some initial changes to allow for lemmas on demand.

To be done:
* Add erasable map Clause* to bool to minisat (backtracks with the solver)
* Add map from Clause* to Node (clauses that came from a node)
* Add reference counting Literal -> Node to CNFManager
* If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable)
* If clause is erased for each L in clause L -> Node refcount goes down
---
 src/prop/cnf_stream.h | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

(limited to 'src/prop/cnf_stream.h')

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 7546a8880..1ea600322 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -39,7 +39,9 @@ class PropEngine;
  * @author Tim King <taking@cs.nyu.edu>
  */
 class CnfStream {
+
 public:
+
   /** Cache of what nodes have been registered to a literal. */
   typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
 
@@ -56,24 +58,31 @@ private:
 
 protected:
 
+  /**
+   * Are we asserting a lemma (true) or a permanent clause (false).
+   * This is set at the begining of convertAndAssert so that it doesn't
+   * need to be passed on over the stack.
+   */
+  bool d_assertingLemma;
+
   /**
    * Asserts the given clause to the sat solver.
    * @param clause the clasue to assert
    */
-  void assertClause(SatClause& clause);
+  void assertClause(TNode node, SatClause& clause);
 
   /**
    * Asserts the unit clause to the sat solver.
    * @param a the unit literal of the clause
    */
-  void assertClause(SatLiteral a);
+  void assertClause(TNode node, SatLiteral a);
 
   /**
    * Asserts the binary clause to the sat solver.
    * @param a the first literal in the clause
    * @param b the second literal in the clause
    */
-  void assertClause(SatLiteral a, SatLiteral b);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b);
 
   /**
    * Asserts the ternary clause to the sat solver.
@@ -81,7 +90,7 @@ protected:
    * @param b the second literal in the clause
    * @param c the thirs literal in the clause
    */
-  void assertClause(SatLiteral a, SatLiteral b, SatLiteral c);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
 
   /**
    * Returns true if the node has been cashed in the translation cache.
@@ -137,7 +146,7 @@ public:
    * @param node node to convert and assert
    * @param whether the sat solver can choose to remove this clause
    */
-  virtual void convertAndAssert(TNode node) = 0;
+  virtual void convertAndAssert(TNode node, bool lemma = false) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -175,8 +184,9 @@ public:
   /**
    * Convert a given formula to CNF and assert it to the SAT solver.
    * @param node the formula to assert
+   * @param lemma is this a lemma that is erasable
    */
-  void convertAndAssert(TNode node);
+  void convertAndAssert(TNode node, bool lemma);
 
   /**
    * Constructs the stream to use the given sat solver.
-- 
cgit v1.2.3