Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.

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 */