Minisat.h

Go to the documentation of this file.

 
#pragma once
 
// IWYU pragma: always_keep
 
#include <ogdf/lib/minisat/core/Solver.h> // IWYU pragma: export
#include <ogdf/lib/minisat/core/SolverTypes.h> // IWYU pragma: export
 
// IWYU pragma: begin_keep
#include <ogdf/basic/basic.h>
 
#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include <vector>
 
#include <stdarg.h>
#include <stdio.h>
 
// IWYU pragma: end_keep
 
namespace Minisat {
 
using std::endl;
using std::string;
 
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);
};
 
}