CVC3::TheoryQuant::TheoryQuant::multTrigsInfo Struct Reference

Collaboration diagram for CVC3::TheoryQuant::TheoryQuant::multTrigsInfo:

[legend]

List of all members.

Public Attributes

• std::vector< std::vector
  < size_t > > common_pos
• std::vector< std::vector
  < size_t > > var_pos
• std::vector< CDMap< Expr, bool > * > var_binds_found
• std::vector< ExprMap< CDList
  < Expr > * > * > uncomm_list
• Theorem univThm
• size_t univ_id

---

Detailed Description

Definition at line 404 of file theory_quant.h.

---

Member Data Documentation

std::vector<std::vector<size_t> > CVC3::TheoryQuant::TheoryQuant::multTrigsInfo::common_pos

Definition at line 405 of file theory_quant.h.

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

std::vector<std::vector<size_t> > CVC3::TheoryQuant::TheoryQuant::multTrigsInfo::var_pos

Definition at line 406 of file theory_quant.h.

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

std::vector<CDMap<Expr, bool>* > CVC3::TheoryQuant::TheoryQuant::multTrigsInfo::var_binds_found

Definition at line 408 of file theory_quant.h.

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

std::vector<ExprMap<CDList<Expr>* >* > CVC3::TheoryQuant::TheoryQuant::multTrigsInfo::uncomm_list

Definition at line 410 of file theory_quant.h.

Referenced by CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::setupTriggers(), and CVC3::TheoryQuant::synNewInst().

Theorem CVC3::TheoryQuant::TheoryQuant::multTrigsInfo::univThm

Definition at line 411 of file theory_quant.h.

Referenced by CVC3::TheoryQuant::checkSat(), and CVC3::TheoryQuant::setupTriggers().

size_t CVC3::TheoryQuant::TheoryQuant::multTrigsInfo::univ_id

Definition at line 412 of file theory_quant.h.

Referenced by CVC3::TheoryQuant::checkSat(), and CVC3::TheoryQuant::setupTriggers().

---

The documentation for this struct was generated from the following file:

• theory_quant.h