CVC3::Trigger Class Reference

#include <theory_quant.h>

Collaboration diagram for CVC3::Trigger:

List of all members.

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:

• theory_quant.h
• theory_quant.cpp