#include "util/minisatsolver.h"

#include "util/conversions.h"

#include "core/SolverTypes.h"

#include <cmath>

namespace satlab
{
    
MinisatSolver::MinisatSolver(const KSATinstance& ksat)
{
    for(auto& clause : ksat.getClauses())
    {
        addClause(clause);
    }
    
}

bool MinisatSolver::solve()
{
    satisfiable = BASE::solve();
}

void MinisatSolver::addClause(const KSATinstance::CLAUSE& clause)
{
    Minisat::vec<Minisat::Lit> clauseVec;
    
    types::convertRef<>(clauseVec, clause);
    
    addMissingVars(clauseVec);
    
    BASE::addClause(clauseVec);
}

void MinisatSolver::addMissingVars(const MINISAT_CLAUSE& clause)
{
    for(int i=0; i < clause.size(); i++)
    {
        while(BASE::nVars() <= Minisat::var(clause[i]))
        {
            BASE::newVar();
        }
    }
}

MinisatResult MinisatSolver::getResult() const
{
    MinisatResult result;
    
    KSATinstance::LITERAL lit;
    for(int i = 0; i < BASE::model.size(); i++)
    {
        lit = BASE::model[i] == Minisat::lbool(true) ? i + 1 : -(i + 1);
        
        result.addLiteralToModel(lit);
    }
    
    result.setStats(getStats());
    result.setSatisfiable(satisfiable);
    
    return result;
}

MinisatStats MinisatSolver::getStats() const
{
    MinisatStats stats;
    
    stats.setSolves(BASE::solves);
    stats.setStarts(BASE::starts);
    stats.setDecisions(BASE::decisions);
    stats.setRndDecisions(BASE::rnd_decisions);
    stats.setPropagations(BASE::propagations);
    stats.setConflicts(BASE::conflicts);
    stats.setDecVars(BASE::dec_vars);
    stats.setClausesLiterals(BASE::clauses_literals);
    stats.setLearntsLiterals(BASE::learnts_literals);
    stats.setMaxLiterals(BASE::max_literals);
    stats.setTotLiterals(BASE::tot_literals);
    
    return stats;
}

}
