26 #ifndef _cvc3__variable_h_
27 #define _cvc3__variable_h_
33 class VariableManager;
36 class SearchEngineRules;
57 bool isNull()
const {
return d_val == NULL; }
100 unsigned&
count(
bool neg);
102 int&
score(
bool neg);
103 bool&
added(
bool neg);
105 unsigned count(
bool neg)
const;
107 int score(
bool neg)
const;
108 bool added(
bool neg)
const;
110 std::vector<std::pair<Clause, int> >&
wp(
bool neg)
const;
127 : d_var(v), d_negative(!positive) { }
133 : d_var(vm, (e.isNot())? e[0] : e), d_negative(e.isNot()) { }
145 if(d_negative)
return -(d_var.
getValue());
176 std::vector<std::pair<Clause, int> >&
wp()
const
177 {
return d_var.
wp(d_negative); }
196 std::ostream&
operator<<(std::ostream& os,
const Literal& l);
231 std::vector<std::pair<Clause, int> >
d_wp;
246 : d_vm(vm), d_refcount(0), d_expr(e),
247 d_count(0), d_countPrev(0), d_score(0),
248 d_negCount(0), d_negCountPrev(0), d_negScore(0),
249 d_added(false), d_negAdded(false),
250 d_val(NULL), d_scope(NULL), d_thm(NULL),
251 d_ante(NULL), d_anteIdx(NULL), d_assump(NULL) { }
266 if(d_val==NULL)
return 0;
267 else return d_val->
get();
271 if(d_scope==NULL)
return 0;
272 else return d_scope->
get();
277 if(d_thm==NULL)
return null;
278 else return d_thm->
get();
283 if(d_ante==NULL)
return null;
284 else return d_ante->
get();
288 if(d_anteIdx==NULL)
return 0;
289 else return d_anteIdx->
get();
294 if(d_assump==NULL)
return null;
295 else return d_assump->
get();
327 return mm->newData(size);
330 mm->deleteData(pMem);
332 void operator delete(
void*) { }
354 inline std::vector<std::pair<Clause, int> >&
Variable::wp(
bool neg)
const {
402 const std::string& mmFlag);
void setValue(const Theorem &thm)
unsigned & count(bool neg)
std::vector< std::pair< Clause, int > > d_wp
int getAntecedentIdx() const
Literal(VariableManager *vm, const Expr &e)
Data structure of expressions in CVC3.
std::hash_set< VariableValue *, HashLV, EqLV > VariableValueSet
unsigned & countPrev(bool neg)
const Theorem & getTheorem() const
std::vector< std::pair< Clause, int > > & wp() const
friend bool operator==(const Variable &l1, const Variable &l2)
bool d_disableGC
Disable the garbage collection.
std::string toString() const
size_t operator()(VariableValue *v) const
std::vector< std::pair< Clause, int > > & wp(bool neg) const
Theorem deriveTheorem() const
ostream & operator<<(ostream &os, const Expr &e)
const Theorem & getTheorem() const
void gc(VariableValue *v)
Garbage collect VariableValue pointer.
SearchEngineRules * getRules() const
ContextManager * getCM() const
void setValue(int val, const Clause &c, int idx)
friend std::ostream & operator<<(std::ostream &os, const Variable &l)
VariableManagerNotifyObj(VariableManager *vm, Context *cxt)
Constructor.
VariableManagerNotifyObj * d_notifyObj
Literal operator!(const Variable &v)
friend std::ostream & operator<<(std::ostream &os, const Literal &l)
const Theorem & getAssumpThm() const
void setAssumpThm(const Theorem &a, int scope)
bool d_postponeGC
Postpone garbage collection.
void setValue(const Theorem &thm, int scope)
unsigned & countPrev(bool neg)
std::vector< std::pair< Clause, int > > d_negwp
friend bool operator==(const VariableValue &v1, const VariableValue &v2)
VariableValue * newVariableValue(const Expr &e)
Variable & operator=(const Variable &l)
Theorem deriveTheorem() const
A class representing a CNF clause (a smart pointer)
const Theorem & getTheorem() const
friend std::ostream & operator<<(std::ostream &os, const VariableValue &v)
const Expr & getExpr() const
const Expr & getExpr() const
const Theorem & getAssumpThm() const
unsigned & count(bool neg)
void resumeGC()
Resume garbage collection.
std::string toString() const
static size_t hash(const Expr &e)
const Expr & getNegExpr() const
friend bool operator==(const Literal &l1, const Literal &l2)
int getAntecedentIdx() const
bool operator()(const VariableValue *lv1, const VariableValue *lv2) const
std::vector< VariableValue * > d_deleted
Vector of variables to be deleted (postponed during pop())
const Variable & getVar() const
Definition of the API to expression package. See class Expr for details.
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)
Literal(const Variable &v, bool positive=true)
Notifies VariableManager before and after each pop()
const Expr & getNegExpr() const
CDO< Theorem > * d_assump
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
SearchEngineRules * d_rules
void setAssumpThm(const Theorem &a, int scope)
unsigned countPrev() const
void postponeGC()
Postpone garbage collection.
VariableValueSet d_varSet