1 files changed, 39 insertions, 106 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d60771e95..9aa1ecff8 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -19,118 +19,53 @@
 
 #include "cvc4_config.h"
 #include "expr/node.h"
-#include "util/decision_engine.h"
-#include "theory/theory_engine.h"
-#include "sat.h"
 #include "util/result.h"
 #include "util/options.h"
-
-#include <map>
+#include "util/decision_engine.h"
+#include "theory/theory_engine.h"
+#include "prop/sat.h"
 
 namespace CVC4 {
 namespace prop {
 
 class CnfStream;
 
-// In terms of abstraction, this is below (and provides services to)
-// Prover and above (and requires the services of) a specific
-// propositional solver, DPLL or otherwise.
-
+/**
+ * PropEngine is the abstraction of a Sat Solver, providing methods for
+ * solving the SAT problem and conversion to CNF (via the CnfStream).
+ */
 class PropEngine {
 
-  friend class CnfStream;
-
-  /** The global options */
-  const Options *d_opts;
-  /** The decision engine we will be using */
-  DecisionEngine *d_de;
-  /** The theory engine we will be using */
-  TheoryEngine *d_te;
-
   /**
-   * The SAT solver.
+   * Indicates that the sat solver is currently solving something and we should
+   * not mess with it's internal state.
    */
-  SatSolver* d_sat;
-
-  std::map<Node, SatVariable> d_atom2var;
-  std::map<SatVariable, Node> d_var2atom;
+  bool d_inCheckSat;
 
-  /** 
-   * Requests a fresh variable from d_sat, v.
-   * Adds mapping of n -> v to d_node2var, and
-   * a mapping of v -> n to d_var2node.
-   */
-  SatVariable registerAtom(const Node& node);
-
-  /**
-   * Requests a fresh variable from d_sat.
-   */
-  SatVariable requestFreshVar();
-
-  /**
-   * Returns true iff this Node is in the atom to variable mapping.
-   * @param n the Node to lookup
-   * @return true iff this Node is in the atom to variable mapping.
-   */
-  bool isAtomMapped(const Node& node) const;
+  /** The global options */
+  const Options *d_options;
 
-  /**
-   * Returns the variable mapped by the atom Node.
-   * @param n the atom to do the lookup by
-   * @return the corresponding variable
-   */
-  SatVariable lookupAtom(const Node& node) const;
+  /** The decision engine we will be using */
+  DecisionEngine *d_decisionEngine;
 
-  /**
-   * Flags whether the solver may need to have its state reset before
-   * solving occurs
-   */
-  bool d_restartMayBeNeeded;
+  /** The theory engine we will be using */
+  TheoryEngine *d_theoryEngine;
 
-  /**
-   * Cleans existing state in the PropEngine and reinitializes the state.
-   */
-  void restart();
+  /** The SAT solver*/
+  SatSolver* d_satSolver;
 
-  /**
-   * Keeps track of all of the assertions that need to be made.
-   */
+  /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
 
-  /**
-   * Returns true iff the variable from the sat solver has been mapped to
-   * an atom.
-   * @param var variable to check if it is mapped
-   * @return returns true iff the minisat var has been mapped.
-   */
-  bool isVarMapped(SatVariable var) const;
-
-  /**
-   * Returns the atom mapped by the variable v.
-   * @param var the variable to do the lookup by
-   * @return an atom
-   */
-  Node lookupVar(SatVariable var) const;
-
-  /**
-   * Asserts an internally constructed clause. Each literal is assumed to be in
-   * the 1-1 mapping contained in d_node2lit and d_lit2node.
-   * @param clause the clause to be asserted.
-   */
-  void assertClause(SatClause& clause);
-
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
-  void assertLit(SatLiteral lit);
-  void signalBooleanPropHasEnded();
-
 public:
 
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(const Options* opts, DecisionEngine*, TheoryEngine*);
+  PropEngine(const Options*, DecisionEngine*, TheoryEngine*);
 
   /**
    * Destructor.
@@ -139,36 +74,34 @@ public:
 
   /**
    * Converts the given formula to CNF and assert the CNF to the sat solver.
+   * The formula is asserted permanently for the current context.
+   * @param node the formula to assert
    */
   void assertFormula(const Node& node);
 
   /**
-   * Currently this takes a well-formed* Node,
-   * converts it to a propositionally equisatisifiable formula for a sat solver,
-   * and invokes the sat solver for a satisfying assignment.
-   * TODO: what does well-formed mean here?
+   * Converts the given formula to CNF and assert the CNF to the sat solver.
+   * The formula can be removed by the sat solver.
+   * @param node the formula to assert
    */
-  Result solve();
+  void assertLemma(const Node& node);
 
-};/* class PropEngine */
-
-inline bool PropEngine::isAtomMapped(const Node & n) const {
-  return d_atom2var.find(n) != d_atom2var.end();
-}
+  /**
+   * Checks the current context for satisfiability.
+   */
+  Result checkSat();
 
-inline SatVariable PropEngine::lookupAtom(const Node & n) const {
-  Assert(isAtomMapped(n));
-  return d_atom2var.find(n)->second;
-}
+  /**
+   * Push the context level.
+   */
+  void push();
 
-inline bool PropEngine::isVarMapped(SatVariable v) const {
-  return d_var2atom.find(v) != d_var2atom.end();
-}
+  /**
+   * Pop the context level.
+   */
+  void pop();
 
-inline Node PropEngine::lookupVar(SatVariable v) const {
-  Assert(isVarMapped(v));
-  return d_var2atom.find(v)->second;
-}
+};/* class PropEngine */
 
 }/* prop namespace */
 }/* CVC4 namespace */