Minisat.h

Go to the documentation of this file.

 
#pragma once
 
#include <ogdf/basic/basic.h>
 
#include <ogdf/lib/minisat/core/Solver.h>
#include <ogdf/lib/minisat/core/SolverTypes.h>
 
#include <stdio.h>
#include <iostream>
#include <fstream>
 
#include <stdarg.h>
 
#include <string>
#include <sstream>
 
#include <vector>
 
namespace Minisat
{
 
using std::string;
using std::endl;
 
class OGDF_EXPORT Clause
{
public:
    Internal::vec<Internal::Lit> m_ps;
    Clause(){}
    Clause( const Clause &src ) { src.m_ps.copyTo(m_ps); }
    virtual ~Clause(){}
 
    // this function allows to put signed Vars directly
    // because Vars in Solver are starting with 0 (not signable with "-")
    // values in input are staring with 1/-1 and are recalculated to 0-base in this function
 
    void add(Internal::Var signedVar)
    {
        Internal::Lit lit;
        if ( signedVar >= 0 )
        {
            lit = Internal::mkLit(signedVar-1, true);
        }
        else
        {
            lit = Internal::mkLit(-(signedVar+1), false);
        }
        m_ps.push(lit);
    }
 
 
    void addMultiple ( int Amount, ... );
 
    void setSign(Internal::Var x, bool sign)
    {
        for ( int i = 0; i < m_ps.size(); i++ )
        {
            if (Internal::var(m_ps[i]) == x) {
                m_ps[i] = Internal::mkLit(x, sign);
                break;
            }
        }
    }
 
    bool getSign(Internal::Var x)
    {
        for (int i = 0; i < m_ps.size(); i++) {
            if (Internal::var(m_ps[i]) == x) {
                return Internal::sign(m_ps[i]);
            }
        }
        std::cout << "Variable not in Clause" << std::endl;
        return false;
    }
 
    void removeLit(Internal::Var x)
    {
        //the vec-class doesn't allow to erase elements at a position
        Internal::vec<Internal::Lit> help;
        m_ps.copyTo(help);
        m_ps.clear();
        for ( int i = 0; i < m_ps.size(); i++ )
        {
            if (Internal::var(m_ps[i]) != x) {
                m_ps.push( help[i] );
            }
 
        }
    }
 
    static char convertLitSign(Internal::Lit lit)
    {
        if ( sign(lit) == 0 )
            return '-';
        else
            return ' ';
    }
 
    void writeToConsole()
    {
        for ( int i = 0; i < m_ps.size() - 1; i++ )
            std::cout << convertLitSign( m_ps[i] ) << Internal::var(m_ps[i]) + 1 << " || ";
        std::cout << convertLitSign( m_ps[ m_ps.size() - 1 ] ) << Internal::var(m_ps[m_ps.size() - 1]) + 1 << std::endl;
    }
};
 
using clause = Clause*;
 
class OGDF_EXPORT Model
{
private:
    std::vector<int> m_vModel;
 
    void reset()
    {
        m_vModel.clear();
    }
 
public:
    Internal::Solver::SolverStatus solverStatus;
 
    Model() {};
    virtual ~Model() { reset(); }
 
    bool getValue (int var) const
    {
        OGDF_ASSERT(var > 0);
        OGDF_ASSERT(var <= (int)m_vModel.size());
        return m_vModel[var-1] != 0;
    }
 
    void setModel(Internal::Solver &S)
    {
        reset();
 
        m_vModel.reserve( S.model.size() );
        for ( int i = 0; i < S.model.size() ; i++ )
        {
            m_vModel.push_back(Internal::toInt(S.model[i]));
        }
    }
 
    void printModel()
    {
        for ( int i = 0; i < (int)m_vModel.size(); i++ )
        {
            std::cout << "Var " << i << " = " << m_vModel[i] << " ";
        }
        std::cout << std::endl;
    }
 
    std::string intToString ( const int i )
    {
        std::string s;
        switch ( i )
        {
            case 0:
                s = "False";
                break;
            case 1:
                s = "True";
                break;
            case 2:
                s = "Undefined";
                break;
            default :
                s = "";
        };
        return s;
    };
};
 
class OGDF_EXPORT Formula : private Internal::Solver
{
private:
    std::stringstream m_messages;
    std::vector<Clause*> m_Clauses;
 
    void free();
 
public:
    Formula() {}
    virtual ~Formula(){ free(); }
 
void newVar ()
{
    Solver::newVar();
}
 
void newVars ( unsigned int Count )
{
    //proofs if variables from clause are valid (still known to formula)
    for ( unsigned int i = 0; i < Count; i++ )
        Solver::newVar();
}
 
 
Clause *newClause();
 
 
void finalizeClause( const clause cl );
 
template<class Iteratable>
void addClause(const Iteratable &literals)
{
    auto cl = newClause();
    for (auto literal : literals) {
        cl->add(literal);
    }
    finalizeClause(cl);
}
 
 
bool finalizeNotExtensibleClause ( const clause cl );
 
Clause *getClause ( const int pos );
 
void removeClause( int i );
 
int getProblemClauseCount()
{
    return nClauses();
}
 
int getClauseCount()
{
    return (int)m_Clauses.size();
}
 
int getVariableCount()
{
    return nVars();
}
 
 
bool solve( Model &ReturnModel );
 
 
bool solve( Model &ReturnModel, double& timeLimit );
 
Internal::Var getVarFromLit(const Internal::Lit &lit)
{
    return Internal::var(lit);
}
 
void clauseAddLiteral(unsigned int clausePos, Internal::Var signedVar)
{
    removeClause( clausePos );
    m_Clauses[clausePos]->add(signedVar);
    Solver::addClause( m_Clauses[clausePos]->m_ps );
}
 
void reset();
 
bool readDimacs(const char *filename);
 
bool readDimacs(const string &filename);
 
bool readDimacs(std::istream &in);
 
bool writeDimacs(const char *filename);
 
bool writeDimacs(const string &filename);
 
bool writeDimacs(std::ostream &f);
};
 
}