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 = "
322 d_thm->set(thm, scope);
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;
int getAntecedentIdx() const
Data structure of expressions in CVC3.
std::string toString() const
const Theorem & getTheorem() const
bool d_disableGC
Disable the garbage collection.
std::string toString() const
ostream & operator<<(ostream &os, const Expr &e)
const Theorem & getTheorem() const
void set(const T &data, int scope=-1)
void gc(VariableValue *v)
Garbage collect VariableValue pointer.
SearchEngineRules * getRules() const
ContextManager * getCM() const
void setValue(int val, const Clause &c, int idx)
_hash_table::iterator iterator
VariableManagerNotifyObj * d_notifyObj
#define DebugAssert(cond, str)
virtual Theorem unitProp(const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0
Unit propagation rule: .
virtual Theorem conflictRule(const std::vector< Theorem > &thms, const Theorem &clause)=0
"Conflict" rule (all literals in a clause become FALSE)
const Theorem & getAssumpThm() const
void setAssumpThm(const Theorem &a, int scope)
bool d_postponeGC
Postpone garbage collection.
Context * getCurrentContext()
Abstract proof rules interface to the simple search engine.
const Theorem & getTheorem() const
std::string toString() const
VariableValue * newVariableValue(const Expr &e)
std::string toString() const
Print the expression to a string.
Variable & operator=(const Variable &l)
Theorem deriveTheorem() const
A class representing a CNF clause (a smart pointer)
std::string int2string(int n)
size_type erase(const key_type &key)
friend std::ostream & operator<<(std::ostream &os, const VariableValue &v)
const Expr & getExpr() const
iterator begin()
iterators
const Theorem & getAssumpThm() const
virtual void deleteData(void *d)=0
void resumeGC()
Resume garbage collection.
std::string toString() const
const Expr & getNegExpr() const
int getAntecedentIdx() const
std::vector< VariableValue * > d_deleted
Vector of variables to be deleted (postponed during pop())
VariableManager(ContextManager *cm, SearchEngineRules *rules, const std::string &mmFlag)
const Expr & getExpr() const
API to the proof rules for the Search Engines.
VariableValue(VariableManager *vm, const Expr &e)
Notifies VariableManager before and after each pop()
CDO< Theorem > * d_assump
const Expr & getNegExpr() const
Manager for multiple contexts. Also holds current context.
void setValue(int val, const Clause &c, int idx)
const Clause & getAntecedent() const
Theorem deriveThmRec(bool checkAssump) const
const Clause & getAntecedent() const
const std::vector< Literal > & getLiterals() const
void setAssumpThm(const Theorem &a, int scope)
VariableValueSet d_varSet