38 : d_val(vm->newVariableValue(e))
58 if(&l ==
this)
return *
this;
173 vector<Theorem> thms;
174 int size(lits.size());
176 for(
int i=0; i<size; ++i)
177 if(i!=idx) thms.push_back(lits[i].getVar().
deriveThmRec(
true));
186 || (e.isNot() && e[0] ==
getExpr()),
187 "Variable::deriveTheorem: bad theorem derived: expr ="
203 return os << (*l.
d_val);
221 os <<
", count=" << l.
count() <<
", score=" << l.
score();
264 for(
int i=0, iend=c.
size(); i!=iend; ++i) {
267 if(s > scope) scope = s;
269 "VariableValue::setValue(ante): literal has no value: "
285 || (val < 0 && l.isNot() && l[0] ==
getExpr()),
286 "VariableValue::setValue(val = " +
int2string(val)
289 +
"\n literal = " + l.toString());
315 "VariableValue::setValue(thm = "
360 if(i != iend)
return (*i);
363 d_varSet.insert(p_vv);
369 const string& mmFlag)
370 : d_cm(cm), d_rules(rules), d_disableGC(false), d_postponeGC(false) {
371 if(mmFlag ==
"chunks")
384 vector<VariableValue*> vars;
393 for(vector<VariableValue*>::iterator i=vars.begin(), iend=vars.end();
394 i!=iend; ++i)
delete *i;