Class: RicoSAT

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

Constant Summary collapse

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

Instance Method Summary collapse

Instance Method Details

#add(lit) ⇒ Object 



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

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 



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

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 



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

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 



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

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 



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

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 



64
65
66
67
68
69
70
71
72
73
74
75
76
 
# File 'ext/ricosat/ricosat.c', line 64

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 



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

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 



91
92
93
94
95
96
97
98
99
100
 
# File 'ext/ricosat/ricosat.c', line 91

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 



78
79
80
81
82
83
84
85
86
87
88
89
 
# File 'ext/ricosat/ricosat.c', line 78

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 



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

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 



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

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

#solve(limit) ⇒ Object 



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

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 



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

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 



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

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