dpllt.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file dpllt.h
 *\brief Generic DPLL(T) module
 *
 * Author: Clark Barrett
 *
 * Created: Mon Dec 12 16:28:08 2005
 */
/*****************************************************************************/

#ifndef _cvcl__include__dpllt_h_
#define _cvcl__include__dpllt_h_

#include "cnf.h"

namespace SAT {

class DPLLT {
public:

  enum Result {UNSAT, SATISFIABLE, ABORT };
  enum ConsistentResult {INCONSISTENT, MAYBE_CONSISTENT, CONSISTENT };

  class TheoryAPI {
  public:
    TheoryAPI() {}
    virtual ~TheoryAPI() {}

    //! Set a checkpoint for backtracking
    virtual void push() = 0;
    //! Restore most recent checkpoint
    virtual void pop() = 0;

    //! Notify theory when a literal is set to true
    virtual void assertLit(Lit l) = 0;

    //! Check consistency of the current assignment.
    /*! The result is either INCONSISTENT, MAYBE_CONSISTENT, or CONSISTENT
     * Most of the time, fullEffort should be false, and the result will most
     * likely be either INCONSISTENT or MAYBE_CONSISTENT.  To force a full
     * check, set fullEffort to true.  When fullEffort is set to true, the
     * only way the result can be MAYBE_CONSISTENT is if there are new clauses
     * to get (via getNewClauses).
     * \param c should be empty initially.  If INCONSISTENT is returned,
     * then c will contain a conflict clause when it returns.  Otherwise, c is
     * unchanged.
     */
    virtual ConsistentResult checkConsistent(Clause& c, bool fullEffort) = 0;

    //! Get a literal that is implied by the current assignment.
    /*! This is theory propagation.  It can be called repeatedly and returns a
     * Null literal when there are no more literals to propagate.  It should
     * only be called when the assignment is not known to be inconsistent.
     */
    virtual Lit getImplication() = 0;

    //! Get an explanation for a literal that was implied
    /*! Given a literal l that is true in the current assignment as a result of
     * an earlier call to getImplication(), this method returns a clause which
     * justifies the propagation of that literal.  The clause will contain the
     * literal l as well as other literals that are in the current assignment.
     * The clause is such that it would have caused a unit propagation at the
     * time getImplication() was called.
     * \param c should be empty initially. */
    virtual void getExplanation(Lit l, Clause& c) = 0;

    //! Get new clauses from the theory.
    /*! This is extended theory learning.  Returns false if there are no new
     * clauses to get.  Otherwise, returns true and new clauses are added to
     * cnf.  Note that the new clauses (if any) are theory lemmas, i.e. clauses
     * that are valid in the theory and not dependent on the current
     * assignment.  The clauses may contain new literals as well as literals
     * that are true in the current assignment.
     * \param cnf should be empty initially. */
    virtual bool getNewClauses(CNF_Formula& cnf) = 0;

  };

  class Decider {
  public:
    Decider() {}
    virtual ~Decider() {}

    //! Make a decision.
    /* Returns a NULL Lit if there are no more decisions to make */
    virtual Lit makeDecision() = 0;

  };

protected:
  TheoryAPI* d_theoryAPI;
  Decider* d_decider;

public:
  //! Constructor
  /*! The client constructing DPLLT must provide an implementation of
   * TheoryAPI.  It may also optionally provide an implementation of Decider.
   * If decider is NULL, then the DPLLT class must make its own decisions.
   */
  DPLLT(TheoryAPI* theoryAPI, Decider* decider)
    : d_theoryAPI(theoryAPI), d_decider(decider) {}
  virtual ~DPLLT() {}

  TheoryAPI* theoryAPI() { return d_theoryAPI; }
  Decider* decider() { return d_decider; }

  //! Check the satisfiability of a set of clauses in the current context
  /*! If the result is SATISFIABLE, the DPLLT engine should remain in the state
   * containing the satisfiable assignment until returnFromSat() is called.  If
   * the result is UNSAT or ABORT, the DPLLT engine should return to the state
   * it was in when called.  Note that it should be possible to call checkSat
   * multiple times, even if the result is true (each additional call should
   * use the context left by the previous call).
   */
  virtual Result checkSat(const CNF_Formula& cnf) = 0;

  //! Continue checking the last check with additional constraints
  /*! Should only be called after a previous call to checkSat (or
   * continueCheck) that returned SATISFIABLE.  It should add the clauses in
   * cnf to the existing clause database and search for a satisfying
   * assignment.  As with checkSat, if the result is SATISFIABLE, the DPLLT
   * engine should remain in the state containing the satisfiable assignment
   * until returnFromSat() is called.  Note that returnFromSat should return to
   * the state just before the last call to checkSat, NOT the last call to
   * continueCheck.  Similarly, if the result is UNSAT or ABORT, the DPLLT
   * engine should return to the state it was in when checkSat was last called.
   */
  virtual Result continueCheck(const CNF_Formula& cnf) = 0;

  //! Get value of variable: unassigned, false, or true
  virtual Var::Val getValue(Var v) = 0;

  //! Return to the state just before the last satisfiable call to checkSat
  /*! Each time a call to checkSat returns SATISFIABLE, the resulting
   * assignment is retained.  Multiple calls to checkSat can be used to refine
   * assignments, adding additional constraints each time.  returnFromSat()
   * returns to the state just before the last call to checkSat which returned
   * SATISFIABLE. */
  virtual void returnFromSat() = 0;

};

}

#endif

---