Class: RicoSAT

Inherits:
Object
  • Object
show all
Defined in:
lib/ricosat.rb,
ext/ricosat/ricosat.c

Constant Summary collapse

VERSION = 
'1.0.3'
UNKNOWN = 
INT2NUM(PICOSAT_UNKNOWN)
SATISFIABLE = 
INT2NUM(PICOSAT_SATISFIABLE)
UNSATISFIABLE = 
INT2NUM(PICOSAT_UNSATISFIABLE)

Instance Method Summary collapse

Instance Method Details

#add(lit) ⇒ Object 



59
60
61
62
63
 
# File 'ext/ricosat/ricosat.c', line 59

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 ⇒ Object 



154
155
156
157
158
159
 
# File 'ext/ricosat/ricosat.c', line 154

static VALUE added_original_clauses(VALUE self)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_added_original_clauses(sat));
}

#assume(lit) ⇒ Object 



109
110
111
112
113
114
 
# File 'ext/ricosat/ricosat.c', line 109

static VALUE assume(VALUE self, VALUE lit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_assume(sat, NUM2INT(lit));
    return self;
}

#coreclause(i) ⇒ Object 



147
148
149
150
151
152
 
# File 'ext/ricosat/ricosat.c', line 147

static VALUE coreclause(VALUE self, VALUE i)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_coreclause(sat, NUM2INT(i)));
}

#corelit(lit) ⇒ Object 



140
141
142
143
144
145
 
# File 'ext/ricosat/ricosat.c', line 140

static VALUE corelit(VALUE self, VALUE lit)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_corelit(sat, NUM2INT(lit)));
}

#deref(lit) ⇒ Object 



71
72
73
74
75
76
77
78
79
80
81
82
83
 
# File 'ext/ricosat/ricosat.c', line 71

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 ⇒ Object 



122
123
124
125
126
127
 
# File 'ext/ricosat/ricosat.c', line 122

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(lit) ⇒ Object 



98
99
100
101
102
103
104
105
106
107
 
# File 'ext/ricosat/ricosat.c', line 98

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 ⇒ Object 



85
86
87
88
89
90
91
92
93
94
95
96
 
# File 'ext/ricosat/ricosat.c', line 85

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=(val) ⇒ Object 



161
162
163
164
165
166
167
 
# File 'ext/ricosat/ricosat.c', line 161

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 ⇒ Object 



53
54
55
56
57
 
# File 'ext/ricosat/ricosat.c', line 53

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(lit) ⇒ Object 



39
40
41
42
43
44
 
# File 'ext/ricosat/ricosat.c', line 39

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 ⇒ Object 



17
18
19
20
21
22
23
 
# File 'ext/ricosat/ricosat.c', line 17

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(lit) ⇒ Object 



32
33
34
35
36
37
 
# File 'ext/ricosat/ricosat.c', line 32

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 ⇒ Object 



169
170
171
172
173
174
175
 
# File 'ext/ricosat/ricosat.c', line 169

static VALUE reset_phases(VALUE self)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_reset_phases(sat);
    return self;
}

#reset_scores ⇒ Object 



177
178
179
180
181
182
183
 
# File 'ext/ricosat/ricosat.c', line 177

static VALUE reset_scores(VALUE self)
{
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    picosat_reset_scores(sat);
    return self;
}

#set_default_phase(lit, val) ⇒ Object 



46
47
48
49
50
51
 
# File 'ext/ricosat/ricosat.c', line 46

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(limit) ⇒ Object 



65
66
67
68
69
 
# File 'ext/ricosat/ricosat.c', line 65

static VALUE solve(VALUE self, VALUE limit) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_sat(sat, NUM2INT(limit)));
}

#variables ⇒ Object 



116
117
118
119
120
 
# File 'ext/ricosat/ricosat.c', line 116

static VALUE variables(VALUE self) {
    PicoSAT * sat;
    TypedData_Get_Struct(self, PicoSAT, &RicoSatType, sat);
    return INT2NUM(picosat_variables(sat));
}

#verbosity=(verbosity) ⇒ Object 



25
26
27
28
29
30
 
# File 'ext/ricosat/ricosat.c', line 25

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(io) ⇒ Object 



129
130
131
132
133
134
135
136
137
138
 
# File 'ext/ricosat/ricosat.c', line 129

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