eSLIM::CadicalSolver Class Reference

#include <satInterfaces.hpp>

Classes
class	TimeoutTerminator

Public Member Functions
void	addClause (int *pLits, int nLits)
void	assume (const std::vector< int > &assumptions)
int	solve (double timeout)
int	solve ()
Vec_Int_t *	getModelVec ()
double	getRunTime () const

Detailed Description

Definition at line 37 of file satInterfaces.hpp.

Member Function Documentation

addClause()

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

inline

Definition at line 92 of file satInterfaces.hpp.

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

assume()

void eSLIM::CadicalSolver::assume ( const std::vector< int > & assumptions )

inline

Definition at line 102 of file satInterfaces.hpp.

                                                                     {
    for (auto& l: assumptions) {
      solver.assume(l);
    }
  }

getModelVec()

Vec_Int_t * eSLIM::CadicalSolver::getModelVec ( )

inline

Definition at line 129 of file satInterfaces.hpp.

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

getRunTime()

double eSLIM::CadicalSolver::getRunTime ( ) const

inline

Definition at line 88 of file satInterfaces.hpp.

                                                {
    return last_runtime;
  }

solve() [1/2]

int eSLIM::CadicalSolver::solve ( )

inline

Definition at line 108 of file satInterfaces.hpp.

                                  {
    std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
    int status = solver.solve();
    last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
    return status;
  }

solve() [2/2]

int eSLIM::CadicalSolver::solve ( double timeout )

inline

Definition at line 115 of file satInterfaces.hpp.

                                                {
    std::chrono::time_point<std::chrono::steady_clock> start = std::chrono::steady_clock::now();
    TimeoutTerminator terminator(timeout);
    solver.connect_terminator(&terminator);
    int status = solver.solve();
    last_runtime = std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::steady_clock::now() - start).count();
    if (solver.state() == CaDiCaL::INVALID) {
      std::cerr<<"Solver is in invalid state"<<std::endl;
      return -1;
    }
    solver.disconnect_terminator();
    return status;
  }

---

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

• src/opt/eslim/satInterfaces.hpp