Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extend Glucose42 API with randomness support #192

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Extend Glucose42 API with randomness support #192

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions pysat/solvers.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4358,6 +4358,48 @@ def set_phases(self, literals=[]):
if self.glucose:
pysolvers.glucose421_setphases(self.glucose, literals)

def set_rnd_seed(self, seed):
"""Sets the seed for the solver's PRNG.

Args:
seed (float): Value for seeding the PRNG
"""

pysolvers.glucose421_set_rnd_seed(self.glucose, seed)

def set_rnd_freq(self, freq):
"""Sets the frequency of random decisions.

Args:
freq (float): Frequency value, must be 0 <= freq <= 1
"""
pysolvers.glucose421_set_rnd_freq(self.glucose, freq)

def set_rnd_pol(self, rnd_pol):
"""Enables/disables random polarities.

Args:
rnd_pol (bool): If True, the solver will use random polarities.
"""
pysolvers.glucose421_set_rnd_pol(self.glucose, rnd_pol)

def set_rnd_init_act(self, rnd_pol):
"""Enables/disables random values for initial variable activities.

Args:
rnd_pol (bool): If True, the solver will randomly initialise variable activities.
"""
pysolvers.glucose421_set_rnd_init_act(self.glucose, rnd_pol)

def set_rnd_first_descent(self, enabled):
"""Sets the solver's behaviour during the first descent.

Args:
enabled (bool): If True, the solver will make random decision until the first conflict.
"""
pysolvers.glucose421_set_rnd_first_descent(self.glucose, enabled)


def get_status(self):
"""
Returns solver's status.
Expand Down
190 changes: 151 additions & 39 deletions solvers/pysolvers.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -136,6 +136,19 @@ static char vreset_docstring[] = "Remove all the 'observed' variable flags"
"(CaDiCaL 1.9.5 only).";
static char isdeclit_docstring[] = "Get reason of valid observed literal "
"(CaDiCaL 1.9.5 only).";
static char set_rnd_seed_docstring[] = "Set PNRG seed "
"(Glucose 4.2.1 only).";
static char set_rnd_freq_docstring[] = "Set frequency of random decisions "
"(Glucose 4.2.1 only).";
static char set_rnd_pol_docstring[] = "Randomize polarities on branching "
"(Glucose 4.2.1 only).";
static char set_rnd_init_act_docstring[] = "Randomize initial activities "
"(Glucose 4.2.1 only).";
static char set_rnd_first_descent_docstring[] = "Randomize decisions until first conflict "
"(Glucose 4.2.1 only).";




static PyObject *SATError;
static jmp_buf env;
Expand Down Expand Up @@ -294,25 +307,30 @@ extern "C" {
static PyObject *py_glucose41_acc_stats (PyObject *, PyObject *);
#endif
#ifdef WITH_GLUCOSE421
static PyObject *py_glucose421_new (PyObject *, PyObject *);
static PyObject *py_glucose421_set_start (PyObject *, PyObject *);
static PyObject *py_glucose421_add_cl (PyObject *, PyObject *);
static PyObject *py_glucose421_solve (PyObject *, PyObject *);
static PyObject *py_glucose421_solve_lim (PyObject *, PyObject *);
static PyObject *py_glucose421_propagate (PyObject *, PyObject *);
static PyObject *py_glucose421_setphases (PyObject *, PyObject *);
static PyObject *py_glucose421_cbudget (PyObject *, PyObject *);
static PyObject *py_glucose421_pbudget (PyObject *, PyObject *);
static PyObject *py_glucose421_interrupt (PyObject *, PyObject *);
static PyObject *py_glucose421_clearint (PyObject *, PyObject *);
static PyObject *py_glucose421_setincr (PyObject *, PyObject *);
static PyObject *py_glucose421_tracepr (PyObject *, PyObject *);
static PyObject *py_glucose421_core (PyObject *, PyObject *);
static PyObject *py_glucose421_model (PyObject *, PyObject *);
static PyObject *py_glucose421_nof_vars (PyObject *, PyObject *);
static PyObject *py_glucose421_nof_cls (PyObject *, PyObject *);
static PyObject *py_glucose421_del (PyObject *, PyObject *);
static PyObject *py_glucose421_acc_stats (PyObject *, PyObject *);
static PyObject *py_glucose421_new (PyObject *, PyObject *);
static PyObject *py_glucose421_set_start (PyObject *, PyObject *);
static PyObject *py_glucose421_add_cl (PyObject *, PyObject *);
static PyObject *py_glucose421_solve (PyObject *, PyObject *);
static PyObject *py_glucose421_solve_lim (PyObject *, PyObject *);
static PyObject *py_glucose421_propagate (PyObject *, PyObject *);
static PyObject *py_glucose421_setphases (PyObject *, PyObject *);
static PyObject *py_glucose421_cbudget (PyObject *, PyObject *);
static PyObject *py_glucose421_pbudget (PyObject *, PyObject *);
static PyObject *py_glucose421_interrupt (PyObject *, PyObject *);
static PyObject *py_glucose421_clearint (PyObject *, PyObject *);
static PyObject *py_glucose421_setincr (PyObject *, PyObject *);
static PyObject *py_glucose421_tracepr (PyObject *, PyObject *);
static PyObject *py_glucose421_core (PyObject *, PyObject *);
static PyObject *py_glucose421_model (PyObject *, PyObject *);
static PyObject *py_glucose421_nof_vars (PyObject *, PyObject *);
static PyObject *py_glucose421_nof_cls (PyObject *, PyObject *);
static PyObject *py_glucose421_del (PyObject *, PyObject *);
static PyObject *py_glucose421_acc_stats (PyObject *, PyObject *);
static PyObject *py_glucose421_set_rnd_seed (PyObject *, PyObject *);
static PyObject *py_glucose421_set_rnd_freq (PyObject *, PyObject *);
static PyObject *py_glucose421_set_rnd_pol (PyObject *, PyObject *);
static PyObject *py_glucose421_set_rnd_init_act (PyObject *, PyObject *);
static PyObject *py_glucose421_set_rnd_first_descent (PyObject *, PyObject *);
#endif
#ifdef WITH_LINGELING
static PyObject *py_lingeling_new (PyObject *, PyObject *);
Expand Down Expand Up @@ -618,25 +636,30 @@ static PyMethodDef module_methods[] = {
{ "glucose41_acc_stats", py_glucose41_acc_stats, METH_VARARGS, acc_stat_docstring },
#endif
#ifdef WITH_GLUCOSE421
{ "glucose421_new", py_glucose421_new, METH_VARARGS, new_docstring },
{ "glucose421_set_start", py_glucose421_set_start, METH_VARARGS, setstart_docstring },
{ "glucose421_add_cl", py_glucose421_add_cl, METH_VARARGS, addcl_docstring },
{ "glucose421_solve", py_glucose421_solve, METH_VARARGS, solve_docstring },
{ "glucose421_solve_lim", py_glucose421_solve_lim, METH_VARARGS, lim_docstring },
{ "glucose421_propagate", py_glucose421_propagate, METH_VARARGS, prop_docstring },
{ "glucose421_setphases", py_glucose421_setphases, METH_VARARGS, phases_docstring },
{ "glucose421_cbudget", py_glucose421_cbudget, METH_VARARGS, cbudget_docstring },
{ "glucose421_pbudget", py_glucose421_pbudget, METH_VARARGS, pbudget_docstring },
{ "glucose421_interrupt", py_glucose421_interrupt, METH_VARARGS, interrupt_docstring },
{ "glucose421_clearint", py_glucose421_clearint, METH_VARARGS, clearint_docstring },
{ "glucose421_setincr", py_glucose421_setincr, METH_VARARGS, setincr_docstring },
{ "glucose421_tracepr", py_glucose421_tracepr, METH_VARARGS, tracepr_docstring },
{ "glucose421_core", py_glucose421_core, METH_VARARGS, core_docstring },
{ "glucose421_model", py_glucose421_model, METH_VARARGS, model_docstring },
{ "glucose421_nof_vars", py_glucose421_nof_vars, METH_VARARGS, nvars_docstring },
{ "glucose421_nof_cls", py_glucose421_nof_cls, METH_VARARGS, ncls_docstring },
{ "glucose421_del", py_glucose421_del, METH_VARARGS, del_docstring },
{ "glucose421_acc_stats", py_glucose421_acc_stats, METH_VARARGS, acc_stat_docstring },
{ "glucose421_new", py_glucose421_new, METH_VARARGS, new_docstring },
{ "glucose421_set_start", py_glucose421_set_start, METH_VARARGS, setstart_docstring },
{ "glucose421_add_cl", py_glucose421_add_cl, METH_VARARGS, addcl_docstring },
{ "glucose421_solve", py_glucose421_solve, METH_VARARGS, solve_docstring },
{ "glucose421_solve_lim", py_glucose421_solve_lim, METH_VARARGS, lim_docstring },
{ "glucose421_propagate", py_glucose421_propagate, METH_VARARGS, prop_docstring },
{ "glucose421_setphases", py_glucose421_setphases, METH_VARARGS, phases_docstring },
{ "glucose421_cbudget", py_glucose421_cbudget, METH_VARARGS, cbudget_docstring },
{ "glucose421_pbudget", py_glucose421_pbudget, METH_VARARGS, pbudget_docstring },
{ "glucose421_interrupt", py_glucose421_interrupt, METH_VARARGS, interrupt_docstring },
{ "glucose421_clearint", py_glucose421_clearint, METH_VARARGS, clearint_docstring },
{ "glucose421_setincr", py_glucose421_setincr, METH_VARARGS, setincr_docstring },
{ "glucose421_tracepr", py_glucose421_tracepr, METH_VARARGS, tracepr_docstring },
{ "glucose421_core", py_glucose421_core, METH_VARARGS, core_docstring },
{ "glucose421_model", py_glucose421_model, METH_VARARGS, model_docstring },
{ "glucose421_nof_vars", py_glucose421_nof_vars, METH_VARARGS, nvars_docstring },
{ "glucose421_nof_cls", py_glucose421_nof_cls, METH_VARARGS, ncls_docstring },
{ "glucose421_del", py_glucose421_del, METH_VARARGS, del_docstring },
{ "glucose421_acc_stats", py_glucose421_acc_stats, METH_VARARGS, acc_stat_docstring },
{ "glucose421_set_rnd_seed", py_glucose421_set_rnd_seed, METH_VARARGS, set_rnd_seed_docstring },
{ "glucose421_set_rnd_freq", py_glucose421_set_rnd_freq, METH_VARARGS, set_rnd_freq_docstring },
{ "glucose421_set_rnd_pol", py_glucose421_set_rnd_pol, METH_VARARGS, set_rnd_pol_docstring },
{ "glucose421_set_rnd_init_act", py_glucose421_set_rnd_init_act, METH_VARARGS, set_rnd_init_act_docstring },
{ "glucose421_set_rnd_first_descent", py_glucose421_set_rnd_first_descent, METH_VARARGS, set_rnd_first_descent_docstring },
#endif
#ifdef WITH_LINGELING
{ "lingeling_new", py_lingeling_new, METH_VARARGS, new_docstring },
Expand Down Expand Up @@ -5837,7 +5860,6 @@ static PyObject *py_glucose421_new(PyObject *self, PyObject *args)
"Cannot create a new solver.");
return NULL;
}

return void_to_pyobj((void *)s);
}

Expand Down Expand Up @@ -6205,6 +6227,96 @@ static PyObject *py_glucose421_setincr(PyObject *self, PyObject *args)
Py_RETURN_NONE;
}

//
//=============================================================================
static PyObject *py_glucose421_set_rnd_seed(PyObject *self, PyObject *args)
{
PyObject *s_obj;
double dbl;

if (!PyArg_ParseTuple(args, "Od", &s_obj, &dbl))
return NULL;

// get pointer to solver
Glucose421::Solver *s = (Glucose421::Solver *)pyobj_to_void(s_obj);

s->random_seed = dbl;

Py_RETURN_NONE;
}

//
//=============================================================================
static PyObject *py_glucose421_set_rnd_freq(PyObject *self, PyObject *args)
{
PyObject *s_obj;
double dbl;

if (!PyArg_ParseTuple(args, "Od", &s_obj, &dbl))
return NULL;

// get pointer to solver
Glucose421::Solver *s = (Glucose421::Solver *)pyobj_to_void(s_obj);

s->random_var_freq = dbl;

Py_RETURN_NONE;
}

//
//=============================================================================
static PyObject *py_glucose421_set_rnd_pol(PyObject *self, PyObject *args)
{
PyObject *s_obj;
int b;

if (!PyArg_ParseTuple(args, "Op", &s_obj, &b))
return NULL;

// get pointer to solver
Glucose421::Solver *s = (Glucose421::Solver *)pyobj_to_void(s_obj);

s->rnd_pol = (bool) b;

Py_RETURN_NONE;
}

//
//=============================================================================
static PyObject *py_glucose421_set_rnd_init_act(PyObject *self, PyObject *args)
{
PyObject *s_obj;
int b;

if (!PyArg_ParseTuple(args, "Op", &s_obj, &b))
return NULL;

// get pointer to solver
Glucose421::Solver *s = (Glucose421::Solver *)pyobj_to_void(s_obj);

s->rnd_init_act = (bool) b;

Py_RETURN_NONE;
}

//
//=============================================================================
static PyObject *py_glucose421_set_rnd_first_descent(PyObject *self, PyObject *args)
{
PyObject *s_obj;
int b;

if (!PyArg_ParseTuple(args, "Op", &s_obj, &b))
return NULL;

// get pointer to solver
Glucose421::Solver *s = (Glucose421::Solver *)pyobj_to_void(s_obj);

s->randomizeFirstDescent = (bool) b;

Py_RETURN_NONE;
}

//
//=============================================================================
static PyObject *py_glucose421_tracepr(PyObject *self, PyObject *args)
Expand Down