/**CFile****************************************************************

  FileName    [kissatTest.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName []

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: kissatTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "kissatSolver.h"

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////
void kissat_solver_test() {
  int RetValue;
  int Lits[3];
  // test 1
  {
    kissat_solver *pSat = kissat_solver_new();
    int a = kissat_solver_addvar(pSat);
    int b = kissat_solver_addvar(pSat);
    int c = kissat_solver_addvar(pSat);
    assert(kissat_solver_nvars(pSat) == 3);
    Lits[0] = Abc_Var2Lit(a, 0);
    Lits[1] = Abc_Var2Lit(b, 0);
    Lits[2] = Abc_Var2Lit(c, 0);
    printf("adding (a, b, c)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 3);
    assert(RetValue);
    Lits[0] = Abc_Var2Lit(a, 0);
    Lits[1] = Abc_Var2Lit(b, 1);
    printf("adding (a, !b)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 2);
    assert(RetValue);
    Lits[0] = Abc_Var2Lit(a, 1);
    printf("adding (!a)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
    assert(RetValue);
    RetValue = kissat_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
    printf("solved: %d\n", RetValue);
    assert(RetValue == 1);
    int a_val = kissat_solver_get_var_value(pSat, a);
    int b_val = kissat_solver_get_var_value(pSat, b);
    int c_val = kissat_solver_get_var_value(pSat, c);
    printf("a = %d, b = %d, c = %d\n", a_val, b_val, c_val);
    assert(a_val == 0);
    assert(b_val == 0);
    assert(c_val == 1);
    kissat_solver_delete(pSat);
    printf("test 1 passed\n");
  }
  // test 2
  {
    kissat_solver *pSat = kissat_solver_new();
    kissat_solver_setnvars(pSat, 2);
    assert(kissat_solver_nvars(pSat) == 2);
    Lits[0] = Abc_Var2Lit(0, 0);
    Lits[1] = Abc_Var2Lit(1, 0);
    printf("adding (x0, x1)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 2);
    assert(RetValue);
    Lits[0] = Abc_Var2Lit(0, 0);
    Lits[1] = Abc_Var2Lit(1, 1);
    printf("adding (x0, !x1)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 2);
    assert(RetValue);
    Lits[0] = Abc_Var2Lit(0, 1);
    Lits[1] = Abc_Var2Lit(1, 1);
    printf("adding (!x0, !x1)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 2);
    assert(RetValue);
    RetValue = kissat_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
    printf("solved: %d\n", RetValue);
    assert(RetValue == 1);
    printf("x0 = %d, x1 = %d\n", kissat_solver_get_var_value(pSat, 0), kissat_solver_get_var_value(pSat, 1));
    assert(kissat_solver_get_var_value(pSat, 0) == 1);
    assert(kissat_solver_get_var_value(pSat, 1) == 0);
    kissat_solver_delete(pSat);
    printf("test 2 passed\n");
  }
  // test 3
  {
    kissat_solver *pSat = kissat_solver_new();
    kissat_solver_setnvars(pSat, 3);
    assert(kissat_solver_nvars(pSat) == 3);
    Lits[0] = Abc_Var2Lit(0, 1);
    Lits[1] = Abc_Var2Lit(1, 0);
    Lits[2] = Abc_Var2Lit(2, 1);
    printf("adding (!x0, x1, !x2)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 3);
    assert(RetValue);
    Lits[0] = Abc_Var2Lit(0, 0);
    printf("adding (x0)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
    assert(RetValue);
    Lits[0] = Abc_Var2Lit(1, 1);
    printf("adding (!x1)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
    assert(RetValue);
    Lits[0] = Abc_Var2Lit(2, 0);
    printf("adding (x2)\n");
    RetValue = kissat_solver_addclause(pSat, Lits, Lits + 1);
    RetValue = kissat_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
    printf("solved: %d\n", RetValue);
    assert(RetValue == -1);
    kissat_solver_delete(pSat);
    printf("test 3 passed\n");
  }
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////

ABC_NAMESPACE_IMPL_END
