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 >	boundVars
	)

Definition at line 45 of file theory_quant.cpp.

References bvs, hasRWOp, hasT2, hasTrans, head, isMulti, isSimple, isSuperSimple, multiId, multiIndex, 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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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.

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

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(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), 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(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), 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().

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::matchListNew(), CVC3::TheoryQuant::matchListOld(), 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(), CVC3::TheoryQuant::matchListOld(), 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().

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