Class: MiniSat::Variable

Inherits:
Object
  • Object
show all
Defined in:
ext/minisat/minisat.c

Instance Method Summary collapse

Instance Method Details

#+ ⇒ Literal

Returns positive literal of variable.

Returns:



99
100
101
102
103
104
105
106
107
108
109
110
111
 
# File 'ext/minisat/minisat.c', line 99

static VALUE variable_pos(VALUE rvar)
{
    cvariable *cvar, *clit;
    VALUE rlit;

    Data_Get_Struct(rvar, cvariable, cvar);
    rlit = Data_Make_Struct(rb_cLiteral, cvariable, value_mark, value_free, clit);
    clit->value = wrap_lit_pos_var(cvar->value);
    clit->solver = cvar->solver;
    if(OBJ_TAINTED(rvar)) OBJ_TAINT(rlit);

    return rlit;
}

#- ⇒ Literal

Returns negative literal of variable.

Returns:



120
121
122
123
124
125
126
127
128
129
130
131
132
 
# File 'ext/minisat/minisat.c', line 120

static VALUE variable_neg(VALUE rvar)
{
    cvariable *cvar, *clit;
    VALUE rlit;

    Data_Get_Struct(rvar, cvariable, cvar);
    rlit = Data_Make_Struct(rb_cLiteral, cvariable, value_mark, value_free, clit);
    clit->value = wrap_lit_neg_var(cvar->value);
    clit->solver = cvar->solver;
    if(OBJ_TAINTED(rvar)) OBJ_TAINT(rlit);

    return rlit;
}

#value ⇒ Boolean

Returns an assignment if the SAT is satisfiable. Raises an exception when the SAT is not satisfied.

Returns:

  • (Boolean) 


142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
 
# File 'ext/minisat/minisat.c', line 142

static VALUE variable_value(VALUE rvar)
{
    cvariable *cvar;
    csolver *cslv;

    Data_Get_Struct(rvar, cvariable, cvar);
    Data_Get_Struct(cvar->solver, csolver, cslv);
    check_model_available(cslv->result, 0);
    switch(wrap_solver_ref_var(cslv->solver, cvar->value)) {
        case 0: return Qfalse;
        case 1: return Qtrue;
    }

    return Qnil;
}