class RicoSAT

Constants

SATISFIABLE
UNKNOWN
UNSATISFIABLE
VERSION

Public Instance Methods

add(p1) click to toggle source
static VALUE add(VALUE self, VALUE lit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_add(sat, NUM2INT(lit)));
}
added_original_clauses() click to toggle source
static VALUE added_original_clauses(VALUE self)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_added_original_clauses(sat));
}
assume(p1) click to toggle source
static VALUE assume(VALUE self, VALUE lit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_assume(sat, NUM2INT(lit));
    return self;
}
coreclause(p1) click to toggle source
static VALUE coreclause(VALUE self, VALUE i)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_coreclause(sat, NUM2INT(i)));
}
corelit(p1) click to toggle source
static VALUE corelit(VALUE self, VALUE lit)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_corelit(sat, NUM2INT(lit)));
}
deref(p1) click to toggle source
static VALUE deref(VALUE self, VALUE lit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    switch(picosat_deref(sat, NUM2INT(lit))) {
        case 1:
            return Qtrue;
        case -1:
            return Qfalse;
        case 0:
            return Qnil;
    }
    return Qnil;
}
enable_trace_generation() click to toggle source
static VALUE enable_trace_generation(VALUE self)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_enable_trace_generation(sat));
}
failed_assumption(p1) click to toggle source
static VALUE failed_assumption(VALUE self, VALUE lit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);

    if (picosat_failed_assumption(sat, NUM2INT(lit))) {
        return Qtrue;
    } else {
        return Qfalse;
    }
}
failed_assumptions() click to toggle source
static VALUE failed_assumptions(VALUE self) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);

    VALUE failed_list = rb_ary_new();
    const int * failed = picosat_failed_assumptions(sat);
    while(*failed) {
        rb_ary_push(failed_list, INT2NUM(*failed));
        failed++;
    }
    return failed_list;
}
global_default_phase=(p1) click to toggle source
static VALUE set_global_default_phase(VALUE self, VALUE val)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_set_global_default_phase(sat, NUM2INT(val));
    return self;
}
inc_max_var() click to toggle source
static VALUE inc_max_var(VALUE self) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_inc_max_var(sat));
}
less_important(p1) click to toggle source
static VALUE set_less_important_lit(VALUE self, VALUE lit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_set_less_important_lit(sat, NUM2INT(lit));
    return self;
}
measure_all_calls() click to toggle source
static VALUE measure_all_calls(VALUE self) {
    PicoSAT * sat;

    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_measure_all_calls(sat);
    return self;
}
more_important(p1) click to toggle source
static VALUE set_more_important_lit(VALUE self, VALUE lit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_set_more_important_lit(sat, NUM2INT(lit));
    return self;
}
reset_phases() click to toggle source
static VALUE reset_phases(VALUE self)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_reset_phases(sat);
    return self;
}
reset_scores() click to toggle source
static VALUE reset_scores(VALUE self)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_reset_scores(sat);
    return self;
}
set_default_phase(p1, p2) click to toggle source
static VALUE set_default_phase(VALUE self, VALUE lit, VALUE val) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_set_default_phase_lit(sat, NUM2INT(lit), NUM2INT(val));
    return self;
}
solve(p1) click to toggle source
static VALUE solve(VALUE self, VALUE limit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_sat(sat, NUM2INT(limit)));
}
variables() click to toggle source
static VALUE variables(VALUE self) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_variables(sat));
}
verbosity=(p1) click to toggle source
static VALUE set_verbosity(VALUE self, VALUE verbosity) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_set_verbosity(sat, NUM2INT(verbosity));
    return self;
}
write_extended_trace(p1) click to toggle source
static VALUE write_extended_trace(VALUE self, VALUE io)
{
    PicoSAT * sat;
    rb_io_t * out;

    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    GetOpenFile(io, out);
    picosat_write_extended_trace(sat, fdopen(out->fd, "w"));
    return self;
}