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