CVC3::Trigger Class Reference

#include <theory_quant.h>

Collaboration diagram for CVC3::Trigger:

[legend]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 >
	)

Definition at line 45 of file theory_quant.cpp.

References bvs, hasRWOp, hasT2, hasTrans, head, isMulti, isSimple, isSuperSimple, multiId, multiIndex, null_expr, polarity, and trig.

---

Member Function Documentation

bool Trigger::isPos

(

)

Definition at line 61 of file theory_quant.cpp.

References polarity, CVC3::Pos, and CVC3::PosNeg.

bool Trigger::isNeg

(

)

Definition at line 65 of file theory_quant.cpp.

References CVC3::Neg, polarity, and CVC3::PosNeg.

Expr Trigger::getEx

(

)

Definition at line 73 of file theory_quant.cpp.

References trig.

Referenced by CVC3::TheoryQuant::registerTrig().

std::vector< Expr > Trigger::getBVs

(

)

Definition at line 69 of file theory_quant.cpp.

References bvs.

void Trigger::setHead

(

Expr

h

)

Definition at line 77 of file theory_quant.cpp.

References head.

Expr Trigger::getHead

(

)

Definition at line 81 of file theory_quant.cpp.

References head.

Referenced by CVC3::TheoryQuant::registerTrig().

void Trigger::setRWOp

(

bool

b

)

Definition at line 85 of file theory_quant.cpp.

References hasRWOp.

bool Trigger::hasRW

(

)

Definition at line 89 of file theory_quant.cpp.

References hasRWOp.

void Trigger::setTrans

(

bool

b

)

Definition at line 93 of file theory_quant.cpp.

References hasTrans.

bool Trigger::hasTr

(

)

Definition at line 97 of file theory_quant.cpp.

References hasTrans.

void Trigger::setTrans2

(

bool

b

)

Definition at line 101 of file theory_quant.cpp.

References hasT2.

bool Trigger::hasTr2

(

)

Definition at line 105 of file theory_quant.cpp.

References hasT2.

void Trigger::setSimp

(

)

Definition at line 109 of file theory_quant.cpp.

References isSimple.

bool Trigger::isSimp

(

)

Definition at line 113 of file theory_quant.cpp.

References isSimple.

void Trigger::setSuperSimp

(

)

Definition at line 117 of file theory_quant.cpp.

References isSuperSimple.

bool Trigger::isSuperSimp

(

)

Definition at line 121 of file theory_quant.cpp.

References isSuperSimple.

void Trigger::setMultiTrig

(

)

Definition at line 125 of file theory_quant.cpp.

References isMulti.

bool Trigger::isMultiTrig

(

)

Definition at line 129 of file theory_quant.cpp.

References isMulti.

---

Member Data Documentation

Expr CVC3::Trigger::trig

Definition at line 52 of file theory_quant.h.

Referenced by getEx(), and Trigger().

Polarity CVC3::Trigger::polarity

Definition at line 53 of file theory_quant.h.

Referenced by isNeg(), isPos(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), and Trigger().

std::vector<Expr> CVC3::Trigger::bvs

Definition at line 55 of file theory_quant.h.

Referenced by getBVs(), and Trigger().

Expr CVC3::Trigger::head

Definition at line 56 of file theory_quant.h.

Referenced by CVC3::TheoryQuant::arrayHeuristic(), getHead(), setHead(), and Trigger().

bool CVC3::Trigger::hasRWOp

Definition at line 57 of file theory_quant.h.

Referenced by hasRW(), CVC3::TheoryQuant::registerTrig(), setRWOp(), and Trigger().

bool CVC3::Trigger::hasTrans

Definition at line 58 of file theory_quant.h.

Referenced by hasTr(), setTrans(), and Trigger().

bool CVC3::Trigger::hasT2

Definition at line 59 of file theory_quant.h.

Referenced by hasTr2(), setTrans2(), and Trigger().

bool CVC3::Trigger::isSimple

Definition at line 60 of file theory_quant.h.

Referenced by isSimp(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), setSimp(), and Trigger().

bool CVC3::Trigger::isSuperSimple

Definition at line 61 of file theory_quant.h.

Referenced by isSuperSimp(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), setSuperSimp(), and Trigger().

bool CVC3::Trigger::isMulti

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::synNewInst(), and Trigger().

size_t CVC3::Trigger::multiId

Definition at line 64 of file theory_quant.h.

Referenced by CVC3::TheoryQuant::synNewInst(), and Trigger().

---

The documentation for this class was generated from the following files:

• theory_quant.h
• theory_quant.cpp

---