#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 |
Detailed Description
Definition at line 50 of file theory_quant.h.
Constructor & Destructor Documentation
| Trigger::Trigger | ( | TheoryCore * | core, |
| Expr | e, | ||
| Polarity | pol, | ||
| std::set< Expr > | boundVars | ||
| ) |
Definition at line 45 of file theory_quant.cpp.
References null_expr.
Member Function Documentation
| 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.
Member Data Documentation
| 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().
The documentation for this class was generated from the following files:
