#include "dcSolver.h"
#include "minisatDcSolver.h"

namespace minisat_dc {

Minisat_Solver::Minisat_Solver()
{
  s = new Solver(); 
  s->verbosity = 0;
}

Minisat_Solver::~Minisat_Solver()
{
 delete s;
}

bool Minisat_Solver::solve()
{
 s->solve();
 return s->okay();
}


bool Minisat_Solver::set_cnf(Cnf &cnf)
{
  for ( int i=0; i<cnf.get_var_count(); i++ )
		{
		 s->newVar();      
		}
//setting clauses 
 for ( int i=0;i<cnf.get_clauses().length();i++ )
   {
	if (!add_clause(*cnf.get_clause ( i )))
		return false;
  }
 return true;
}

bool Minisat_Solver::has_preprocess()
{
 return false;
}

bool Minisat_Solver::can_add_clause_later()
{
 return true;
}

bool Minisat_Solver::preprocess()
{
 return true;
}

void Minisat_Solver::assign_solution(Cnf &cnf)
 {
  {
   for ( int i = 0; i < s->nVars(); i++ )
     if ( s->model[i] == l_Undef )
       {
	 cnf.set_value(i,l_dc);
       }	
    else
	{
         for (int i = 0; i < s->nVars(); i++)
            cnf.set_value ( i, ( ( s->model[i]==l_True )?l_true:((s->model[i]==l_False)?l_false:l_dc ) ));
        }
  }
}

bool Minisat_Solver::add_clause(My_Clause &m_c) 
{
 vec<Lit> lits;
 lits.clear();
 for ( int i=0; i< m_c.get_var_count(); i++ )
   {
    lits.push ( ( m_c.polarity ( i ) ) ? Lit ( m_c.var ( i ) ) : ~Lit ( m_c.var ( i ) ) );
   }
 s->addClause( lits );
 return s->okay();
}						

}
				
