// Try to test to Solver.h interface of minisat
#include "SimpSolver.h"
#include <iostream>
int main(int argc, char* argv[]) {
  SimpSolver     S;
  S.verbosity = 1;
  vec<Lit> clause;
  S.newVar(); // create a variable
  clause.push(Lit(0));
  S.addClause(clause);
  if (!S.simplify()) {
    std::cout << "Solved by Unit Propagation" << std::endl;
    return 0;
  }
  {
    bool ret = S.solve(true,true);
    std::cout << (ret?"SATISFIABLE":"UNSATISFIABLE") << std::endl;
    if (ret) {
      std::cout << "SAT" << std::endl;
      for (int i=0; i < S.nVars(); i++)
	if (S.model[i] != l_Undef)
	  std::cout << (i==0?"":" ") <<
	    ((S.model[i]==l_True)?"":"=") << (i+1);
      std::cout << std::endl;
    }
    else {
      std::cout << "UNSAT" << std::endl;
    }
  }
  return 0;
}