#include <theory_quant.h>
Collaboration diagram for CVC3::Trigger:
Definition at line 50 of file theory_quant.h.
Trigger::Trigger | ( | TheoryCore * | core, | |
Expr | e, | |||
Polarity | pol, | |||
std::set< Expr > | ||||
) |
Definition at line 43 of file theory_quant.cpp.
References bvs, hasRWOp, hasT2, hasTrans, head, isMulti, isSimple, isSuperSimple, multiId, multiIndex, null_expr, polarity, and trig.
bool Trigger::isPos | ( | ) |
bool Trigger::isNeg | ( | ) |
Expr Trigger::getEx | ( | ) |
Definition at line 71 of file theory_quant.cpp.
References trig.
Referenced by CVC3::TheoryQuant::registerTrig().
std::vector< Expr > Trigger::getBVs | ( | ) |
void Trigger::setHead | ( | Expr | h | ) |
Definition at line 75 of file theory_quant.cpp.
References head.
Referenced by CVC3::TheoryQuant::setupTriggers().
Expr Trigger::getHead | ( | ) |
Definition at line 79 of file theory_quant.cpp.
References head.
Referenced by CVC3::TheoryQuant::registerTrig().
void Trigger::setRWOp | ( | bool | b | ) |
Definition at line 83 of file theory_quant.cpp.
References hasRWOp.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::hasRW | ( | ) |
void Trigger::setTrans | ( | bool | b | ) |
Definition at line 91 of file theory_quant.cpp.
References hasTrans.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::hasTr | ( | ) |
void Trigger::setTrans2 | ( | bool | b | ) |
Definition at line 99 of file theory_quant.cpp.
References hasT2.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::hasTr2 | ( | ) |
void Trigger::setSimp | ( | ) |
Definition at line 107 of file theory_quant.cpp.
References isSimple.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::isSimp | ( | ) |
void Trigger::setSuperSimp | ( | ) |
Definition at line 115 of file theory_quant.cpp.
References isSuperSimple.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::isSuperSimp | ( | ) |
void Trigger::setMultiTrig | ( | ) |
Definition at line 123 of file theory_quant.cpp.
References isMulti.
Referenced by CVC3::TheoryQuant::setupTriggers().
bool Trigger::isMultiTrig | ( | ) |
Definition at line 53 of file theory_quant.h.
Referenced by isNeg(), isPos(), CVC3::TheoryQuant::newTopMatch(), and Trigger().
std::vector<Expr> CVC3::Trigger::bvs |
Definition at line 56 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::arrayHeuristic(), getHead(), setHead(), and Trigger().
Definition at line 57 of file theory_quant.h.
Referenced by hasRW(), CVC3::TheoryQuant::registerTrig(), setRWOp(), and Trigger().
Definition at line 58 of file theory_quant.h.
Referenced by hasTr(), setTrans(), CVC3::TheoryQuant::synNewInst(), and Trigger().
bool CVC3::Trigger::hasT2 |
Definition at line 59 of file theory_quant.h.
Referenced by hasTr2(), setTrans2(), CVC3::TheoryQuant::synNewInst(), and Trigger().
Definition at line 60 of file theory_quant.h.
Referenced by isSimp(), CVC3::TheoryQuant::newTopMatch(), setSimp(), and Trigger().
Definition at line 61 of file theory_quant.h.
Referenced by isSuperSimp(), CVC3::TheoryQuant::newTopMatch(), setSuperSimp(), and Trigger().
Definition at line 62 of file theory_quant.h.
Referenced by isMultiTrig(), setMultiTrig(), CVC3::TheoryQuant::synNewInst(), and Trigger().
size_t CVC3::Trigger::multiIndex |
Definition at line 63 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::synNewInst(), and Trigger().
size_t CVC3::Trigger::multiId |
Definition at line 64 of file theory_quant.h.
Referenced by CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::synNewInst(), and Trigger().