CVC3
2.4.1
|
#include <theory_quant.h>
Public Member Functions | |
Trigger (TheoryCore *core, Expr e, Polarity pol, std::set< Expr >) | |
bool | isPos () |
bool | isNeg () |
Expr | getEx () |
std::vector< Expr > | getBVs () |
void | setHead (Expr h) |
Expr | getHead () |
void | setRWOp (bool b) |
bool | hasRW () |
void | setTrans (bool b) |
bool | hasTr () |
void | setTrans2 (bool b) |
bool | hasTr2 () |
void | setSimp () |
bool | isSimp () |
void | setSuperSimp () |
bool | isSuperSimp () |
void | setMultiTrig () |
bool | isMultiTrig () |
Public Attributes | |
Expr | trig |
Polarity | polarity |
std::vector< Expr > | bvs |
Expr | head |
bool | hasRWOp |
bool | hasTrans |
bool | hasT2 |
bool | isSimple |
bool | isSuperSimple |
bool | isMulti |
size_t | multiIndex |
size_t | multiId |
Definition at line 50 of file theory_quant.h.
Trigger::Trigger | ( | TheoryCore * | core, |
Expr | e, | ||
Polarity | pol, | ||
std::set< Expr > | boundVars | ||
) |
Definition at line 45 of file theory_quant.cpp.
References null_expr.
bool Trigger::isPos | ( | ) |
Definition at line 61 of file theory_quant.cpp.
References CVC3::Pos, and CVC3::PosNeg.
bool Trigger::isNeg | ( | ) |
Definition at line 65 of file theory_quant.cpp.
References CVC3::Neg, and CVC3::PosNeg.
Expr Trigger::getEx | ( | ) |
Definition at line 73 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::registerTrig().
std::vector< Expr > Trigger::getBVs | ( | ) |
Definition at line 69 of file theory_quant.cpp.
void Trigger::setHead | ( | Expr | h | ) |
Definition at line 77 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::setupTriggers().
Expr Trigger::getHead | ( | ) |
Definition at line 81 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::registerTrig().
void Trigger::setRWOp | ( | bool | b | ) |
Definition at line 85 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::hasRW | ( | ) |
Definition at line 89 of file theory_quant.cpp.
void Trigger::setTrans | ( | bool | b | ) |
Definition at line 93 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::hasTr | ( | ) |
Definition at line 97 of file theory_quant.cpp.
void Trigger::setTrans2 | ( | bool | b | ) |
Definition at line 101 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::hasTr2 | ( | ) |
Definition at line 105 of file theory_quant.cpp.
void Trigger::setSimp | ( | ) |
Definition at line 109 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::isSimp | ( | ) |
Definition at line 113 of file theory_quant.cpp.
void Trigger::setSuperSimp | ( | ) |
Definition at line 117 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::isSuperSimp | ( | ) |
Definition at line 121 of file theory_quant.cpp.
void Trigger::setMultiTrig | ( | ) |
Definition at line 125 of file theory_quant.cpp.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::isMultiTrig | ( | ) |
Definition at line 129 of file theory_quant.cpp.
Expr CVC3::Trigger::trig |
Definition at line 52 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::matchListNew(), and CVC3::TheoryQuant::matchListOld().
Polarity CVC3::Trigger::polarity |
Definition at line 53 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().
std::vector<Expr> CVC3::Trigger::bvs |
Definition at line 55 of file theory_quant.h.
Expr CVC3::Trigger::head |
Definition at line 56 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::arrayHeuristic().
bool CVC3::Trigger::hasRWOp |
Definition at line 57 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::registerTrig().
bool CVC3::Trigger::hasTrans |
Definition at line 58 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), and CVC3::TheoryQuant::synNewInst().
bool CVC3::Trigger::hasT2 |
Definition at line 59 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::synNewInst().
bool CVC3::Trigger::isSimple |
Definition at line 60 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().
bool CVC3::Trigger::isSuperSimple |
Definition at line 61 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().
bool CVC3::Trigger::isMulti |
Definition at line 62 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::matchListOld(), and CVC3::TheoryQuant::synNewInst().
size_t CVC3::Trigger::multiIndex |
Definition at line 63 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::synNewInst().
size_t CVC3::Trigger::multiId |
Definition at line 64 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::synNewInst().