Česky
Kamil Dudka

Fast SAT Solver (C++, GAlib)

File detail

Name:DownloadSatProblem.h [Download]
Location: fss > src
Size:4.2 KB
Last modification:2008-11-05 23:03

Source code

/*
 * 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
 
/**
 * @file SatProblem.h
 * @brief SAT Problem representation
 * @author Kamil Dudka <xdudka00@gmail.com>
 * @date 2008-11-05
 * @ingroup SatProblem
 */
 
#include <string>
#include "Scanner.h"
 
namespace FastSatSolver {
  class ISatItem;
  class IFormulaEvaluator;
 
  /**
   * It can transform variable name to its integral index and vice versa.
   * @brief Container for variables names.
   * @ingroup SatProblem
   */
  class VariableContainer
  {
    public:
      VariableContainer();
      ~VariableContainer();
      /**
       * @brief @return Returns count of variables managed by container.
       */
      int getLength ( );
 
      /**
       * @brief Read name of variable on desired index.
       * @param index Index of variable should be in range <0, getLength()-1>
       * @return Returns variable's name as STL string.
       */
      std::string getVarName (int index );
 
      /**
       * @brief Add variable to container, if it wasn't there before.
       * @param name Name of variable to add.
       * @return Return variable's integral index.
       */
      int addVariable (std::string name );
 
    private:
      struct Private;
      Private *d;
  };
 
  /**
   * @note The only one known implementation is now InterpretedFormula, but
   * there is no restriction to this class. It can be any class implementing
   * IFormulaEvaluator interface.
   * @brief Container for evaluable formulas.
   * @ingroup SatProblem
   */
  class FormulaContainer
  {
    public:
      FormulaContainer();
      ~FormulaContainer();
 
      /**
       * @brief @return Returns count of formulas managed by container.
       */
      int getLength ( );
 
      /**
       * @brief Evaluate all formulas in container using given data and return
       * satisfaction ratio.
       * @param data Evaluation data to use for evaluation. Consider
       * FastSatSolver::ISatItem interface for detail.
       * @return Returns count of satisfaced formulas.
       */
      int evalAll (ISatItem *data);
 
      /**
       * @brief Add formula to container.
       * @param formula Formula object to add.
       */
      void addFormula (IFormulaEvaluator *formula );
 
    private:
      struct Private;
      Private *d;
  };
 
 
  /**
   * @brief SAT Problem module's facade.
   * @ingroup SatProblem
   */
  class SatProblem {
    public:
      SatProblem();
      ~SatProblem();
 
      /**
       * @brief Load SAT Problem specification from file
       * @param fileName File name to read and parse.
       */
      void loadFromFile (std::string fileName );
 
      /**
       * @brief Load SAT Problem specification from standard input.
       */
      void loadFromInput ( );
 
      /**
       * @brief @return Returns total count of variables managed by SatProblem.
       */
      int getVarsCount ( );
 
      /**
       * @brief @return Returns name of variable with desired index.
       * @param index Index of variable should be in range
       * <0, getVarsCount()-1>.
       */
      std::string getVarName (int index );
 
      /**
       * @brief @return Returns total count of formulas managed by SatProblem.
       */
      int getFormulasCount();
 
      /**
       * @brief @copydoc FastSatSolver::FormulaContainer::evalAll(ISatItem*)
       */
      int getSatsCount (ISatItem *data);
 
      /**
       * @brief @return Returns true if SAT Problem is @b not valid.
       */
      bool hasError ( );
 
    private:
      struct Private;
      Private *d;
  };
 
} // namespace FastSatSolver
 
 
#endif // SATPROBLEMIMPL_H