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; }