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 43 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 59 of file theory_quant.cpp.

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

bool Trigger::isNeg (  ) 

Definition at line 63 of file theory_quant.cpp.

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

Expr Trigger::getEx (  ) 

Definition at line 71 of file theory_quant.cpp.

References trig.

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

std::vector< Expr > Trigger::getBVs (  ) 

Definition at line 67 of file theory_quant.cpp.

References bvs.

void Trigger::setHead ( Expr  h  ) 

Definition at line 75 of file theory_quant.cpp.

References head.

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

Expr Trigger::getHead (  ) 

Definition at line 79 of file theory_quant.cpp.

References head.

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

void Trigger::setRWOp ( bool  b  ) 

Definition at line 83 of file theory_quant.cpp.

References hasRWOp.

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

bool Trigger::hasRW (  ) 

Definition at line 87 of file theory_quant.cpp.

References hasRWOp.

void Trigger::setTrans ( bool  b  ) 

Definition at line 91 of file theory_quant.cpp.

References hasTrans.

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

bool Trigger::hasTr (  ) 

Definition at line 95 of file theory_quant.cpp.

References hasTrans.

void Trigger::setTrans2 ( bool  b  ) 

Definition at line 99 of file theory_quant.cpp.

References hasT2.

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

bool Trigger::hasTr2 (  ) 

Definition at line 103 of file theory_quant.cpp.

References hasT2.

void Trigger::setSimp (  ) 

Definition at line 107 of file theory_quant.cpp.

References isSimple.

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

bool Trigger::isSimp (  ) 

Definition at line 111 of file theory_quant.cpp.

References isSimple.

void Trigger::setSuperSimp (  ) 

Definition at line 115 of file theory_quant.cpp.

References isSuperSimple.

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

bool Trigger::isSuperSimp (  ) 

Definition at line 119 of file theory_quant.cpp.

References isSuperSimple.

void Trigger::setMultiTrig (  ) 

Definition at line 123 of file theory_quant.cpp.

References isMulti.

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

bool Trigger::isMultiTrig (  ) 

Definition at line 127 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::newTopMatch(), 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(), 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::newTopMatch(), setSimp(), and Trigger().

bool CVC3::Trigger::isSuperSimple

Definition at line 61 of file theory_quant.h.

Referenced by isSuperSimp(), CVC3::TheoryQuant::newTopMatch(), 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::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:
Generated on Tue Jul 3 14:39:09 2007 for CVC3 by  doxygen 1.5.1