dpllt_basic.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 *\file dpllt_basic.h
 *\brief Basic implementation of dpllt module based on xchaff
 *
 * Author: Clark Barrett
 *
 * Created: Mon Dec 12 19:06:58 2005
 */
/*****************************************************************************/

#ifndef _cvcl__sat__dpllt_basic_h_
#define _cvcl__sat__dpllt_basic_h_

#include "dpllt.h"
#include "sat_api.h"

namespace SAT {

class DPLLTBasic :public DPLLT {

  SatSolver* d_mng;
  bool d_ready;
  bool d_popScopes;
  std::vector<SatSolver*> d_mngStack;
  std::vector<CNF_Formula_Impl*> d_cnfStack;
  bool d_printStats;
  CNF_Formula_Impl* d_cnf;

  void createManager();
  void generate_CDB (CNF_Formula_Impl& cnf);
  void handle_result(SatSolver::SATStatus outcome);
  void verify_solution();

public:
  DPLLTBasic::DPLLTBasic(TheoryAPI* theoryAPI, Decider* decider,
                         bool printStats = false);
  virtual ~DPLLTBasic();

  bool popScopes(void) { return d_popScopes; }

  void addNewClause(const Clause& c);
  void addNewClauses(CNF_Formula_Impl& cnf);

  SatSolver::Lit cvcl2SAT(Lit l)
  { return l.isNull() ? SatSolver::Lit() :
      d_mng->MakeLit(d_mng->GetVar(l.getVar()), l.isPositive() ? 0 : 1); }

  Lit SAT2cvcl(SatSolver::Lit l)
  { return l.IsNull() ? Lit() :
                        Lit(d_mng->GetVarIndex(d_mng->GetVarFromLit(l)),
                            d_mng->GetPhaseFromLit(l) == 0); }

  SatSolver* satSolver() { return d_mng; }

  // Implementation of virtual DPLLT methods
  Result checkSat(const CNF_Formula& cnf);
  Result continueCheck(const CNF_Formula& cnf);
  Var::Val getValue(Var v) { return Var::Val(d_mng->GetVarAssignment(d_mng->GetVar(v))); }
  void returnFromSat();
  void reset(bool popScopes = false);

};

}

#endif

---