CVC3::Trigger Class Reference

#include <theory_quant.h>

Collaboration diagram for CVC3::Trigger:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Public Attributes


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:
Generated on Wed Nov 18 16:16:58 2009 for CVC3 by  doxygen 1.5.2