#include "minisat2Solver.h"
#include "SimpSolver.h"


namespace minisat2 { 

Minisat_Solver::Minisat_Solver()
{
s = new SimpSolver();
s->verbosity = 0;
s->polarity_mode = s->polarity_rnd;
}


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


////////////////////////////////////
bool Minisat_Solver::simplify()
{
	return s->simplify();
}



 /*bool sat=false;

  for ( int i=0; i<cnf.get_var_count(); i++ )
		{
		 s->newVar();      
		}
//setting clauses 
 for ( int i=0;i<cnf.get_clauses().length();i++ )
   {
     sat=false;

	// cout << "clause("<< cnf.get_clause(i)->get_var_count()<< ") " << i << " : " <<endl;
	   //////////////////////////////////////////////////
	/* for(int j=0;j<(*cnf.get_clause(i)).get_var_count();j++){
         cout << cnf.get_clause(i)->var(j)+1 << " ";
		 /*if(cnf.get_clause(i)->var(j)<=vct.length()){
			 if(vct[cnf.get_clause(i)->var(j)]==1){ // kdyz je nastavena ve vektoru ale v termu je 0
				 if(cnf.get_clause(i)->polarity(j)!=true){
					cout <<" (" <<cnf.get_clause(i)->var(j) << ") ";
				    cnf.clauses[i]->remove_var(j);
				 }else sat=true;
			 }
			 if(vct[cnf.get_clause(i)->var(j)]==0){ // kdyz je nastavena ve vektoru ale v termu je 1
				 if(cnf.get_clause(i)->polarity(j)!=false){
                   cout <<" (" <<cnf.get_clause(i)->var(j) << ") ";				
				   cnf.clauses[i]->remove_var(j);
				 }else sat=true;
			 }
			 /// doresit "nevkladani" termu kdzy je splnen .... 
		 }else{
           cout <<" "<<cnf.get_clause(i)->var(j) <<" ";	
		 }*/
	// }
    ////////////////////////////////////////////
	// if(cnf.get_clause(i)->get_var_count()==0)sat=true;
//	 cout <<endl;
	// cout << "clause " << i << "hotovo - pridavam ? : " << sat<<endl;
	// if(sat==false){
//	   if (!add_clause(*cnf.get_clause ( i )))return false;
	 //}


 // }
 //return true;


/*bool Minisat_Solver::solveA(string assign){
	s->polarity_mode=s->polarity_user;
	


	for(int i=0;i<assign.size();i++){
		//cout << i <<" - " << var(toLit(i)) << " - " << toInt(s->assigns[i]) <<endl;
		//if(var(toLit(i))==0)s->assigns[i]=0;//toInt(l_Undef);
		//if(var(toLit(i))==0 || var(toLit(i))==1 || var(toLit(i))==2){
		s->setPolarity(i,true);
		s->assumptions.push(toLit(i));
       
		//}
		//cout <<"hodnota : " << toInt(s->value(toLit(i))) << endl;
		
		cout << i <<"* - " << var(toLit(i)) << " -  pol : "<< toInt(s->polarity[i]) <<" / " << s->assumptions.size() <<endl;
		//cout << i << "* - " << toInt(s->assigns[i]) <<endl;
	}
	
	
	s->simplify();


return s->solve(s->assumptions,true,false);;
}*/
//////////////////////////////////////




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


bool Minisat_Solver::set_cnf(Cnf &cnf)
{
	//cout << "var : "<< cnf.get_var_count() << "clause : "<< cnf.get_clauses().length() <<endl;
  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 true;
}

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

bool Minisat_Solver::preprocess()
{
 return s->simplify();
}

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

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 ) ) );
   }
 return (s->addClause( lits ));
}						

}
				
