Clause() | CVC3::Clause | [inline] |
Clause(TheoryCore *core, VariableManager *vm, const Theorem &clause, int scope, const std::string &file="", int line=0) | CVC3::Clause | [inline] |
Clause(const Clause &c) | CVC3::Clause | [inline] |
ClauseOwner class | CVC3::Clause | [friend] |
countOwner() | CVC3::Clause | [inline, private] |
d_clause | CVC3::Clause | [private] |
deleted() const | CVC3::Clause | [inline] |
dir(int i) const | CVC3::Clause | [inline] |
dir(int i, int d) const | CVC3::Clause | [inline] |
getLiteral(size_t i) const | CVC3::Clause | [inline] |
getLiterals() const | CVC3::Clause | [inline] |
getScope() const | CVC3::Clause | [inline] |
getTheorem() const | CVC3::Clause | [inline] |
id() const | CVC3::Clause | [inline] |
IF_DEBUG(bool wpCheck() const ;) IF_DEBUG(const std | CVC3::Clause | [inline] |
isNull() const | CVC3::Clause | [inline] |
markDeleted() const | CVC3::Clause | |
markSat() const | CVC3::Clause | [inline] |
operator<<(std::ostream &os, const Clause &c) | CVC3::Clause | [friend] |
operator=(const Clause &c) | CVC3::Clause | |
operator==(const Clause &c) const | CVC3::Clause | [inline] |
operator[](size_t i) const | CVC3::Clause | [inline] |
owners() const | CVC3::Clause | [inline] |
sat() const | CVC3::Clause | [inline] |
sat(bool ignored) const | CVC3::Clause | [inline] |
size() const | CVC3::Clause | [inline] |
toString() const | CVC3::Clause | |
watched(int i) const | CVC3::Clause | [inline] |
wp(int i) const | CVC3::Clause | [inline] |
wp(int i, size_t l) const | CVC3::Clause | [inline] |
~Clause() | CVC3::Clause |