eSLIM::KissatSolver Class Reference

#include <satInterfaces.hpp>

Public Member Functions
	KissatSolver ()
	~KissatSolver ()
void	init (int max_var)
void	addClause (int *pLits, int nLits)
int	solve ()
Vec_Int_t *	getModelVec ()

Detailed Description

Definition at line 63 of file satInterfaces.hpp.

Constructor & Destructor Documentation

KissatSolver()

eSLIM::KissatSolver::KissatSolver ( )

inline

Definition at line 147 of file satInterfaces.hpp.

                                    {
    solver = kissat_init();
  }

Here is the call graph for this function:

~KissatSolver()

eSLIM::KissatSolver::~KissatSolver ( )

inline

Definition at line 151 of file satInterfaces.hpp.

                                     {
    kissat_release(solver);
  }

Here is the call graph for this function:

Member Function Documentation

addClause()

void eSLIM::KissatSolver::addClause ( int * pLits, int nLits )

inline

Definition at line 160 of file satInterfaces.hpp.

                                                             {
    for ( int i = 0; i < nLits; i++ ) {
      if (pLits[i] == 0) {
        continue;
      }
      kissat_add (solver, Abc_LitIsCompl(pLits[i]) ? -Abc_Lit2Var(pLits[i]) :  Abc_Lit2Var(pLits[i]));
    }
    kissat_add (solver, 0);
  }

Here is the call graph for this function:

getModelVec()

Vec_Int_t * eSLIM::KissatSolver::getModelVec ( )

inline

Definition at line 185 of file satInterfaces.hpp.

                                              {
    Vec_Int_t* assignment = Vec_IntAlloc( max_var );
    for (int v = 1; v <= max_var; v++) {
      Vec_IntSetEntryFull( assignment, Abc_AbsInt(val(v)), val(v) > 0 );
    }
    return assignment;
  }

init()

void eSLIM::KissatSolver::init ( int max_var )

inline

Definition at line 155 of file satInterfaces.hpp.

                                            {
    this->max_var = max_var;
    kissat_reserve(solver, max_var);
  }

Here is the call graph for this function:

solve()

int eSLIM::KissatSolver::solve ( )

inline

Definition at line 170 of file satInterfaces.hpp.

                                 {
    int status = kissat_solve(solver);
    return status;
  }

Here is the call graph for this function:

---

The documentation for this class was generated from the following file:

• src/opt/eslim/satInterfaces.hpp