CVC3  2.4.1
Public Member Functions | Public Attributes | List of all members
CVC3::Trigger Class Reference

#include <theory_quant.h>

Public Member Functions

 Trigger (TheoryCore *core, Expr e, Polarity pol, std::set< Expr >)
 
bool isPos ()
 
bool isNeg ()
 
Expr getEx ()
 
std::vector< ExprgetBVs ()
 
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< Exprbvs
 
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
Polarity CVC3::Trigger::polarity
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
bool CVC3::Trigger::hasT2

Definition at line 59 of file theory_quant.h.

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

bool CVC3::Trigger::isSimple
bool CVC3::Trigger::isSuperSimple
bool CVC3::Trigger::isMulti
size_t CVC3::Trigger::multiIndex
size_t CVC3::Trigger::multiId

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