SatProblem.h

Go to the documentation of this file.

/*
 * Copyright (C) 2008 Kamil Dudka <xdudka00@stud.fit.vutbr.cz>
 *
 * This file is part of fss (Fast SAT Solver).
 *
 * fss is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * any later version.
 *
 * fss is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with fss.  If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef SATPROBLEMIMPL_H
#define SATPROBLEMIMPL_H

#include <string>
#include "Scanner.h"

namespace FastSatSolver {
  class ISatItem;
  class IFormulaEvaluator;

  class VariableContainer
  {
    public:
      VariableContainer();
      ~VariableContainer();
      int getLength ( );

      std::string getVarName (int index );

      int addVariable (std::string name );

    private:
      struct Private;
      Private *d;
  };

  class FormulaContainer
  {
    public:
      FormulaContainer();
      ~FormulaContainer();

      int getLength ( );

      int evalAll (ISatItem *data);

      void addFormula (IFormulaEvaluator *formula );

    private:
      struct Private;
      Private *d;
  };


  class SatProblem {
    public:
      SatProblem();
      ~SatProblem();

      void loadFromFile (std::string fileName );

      void loadFromInput ( );

      int getVarsCount ( );

      std::string getVarName (int index );

      int getFormulasCount();

      int getSatsCount (ISatItem *data);

      bool hasError ( );

    private:
      struct Private;
      Private *d;
  };

} // namespace FastSatSolver


#endif // SATPROBLEMIMPL_H

---