recCompleteInster Class Reference

Collaboration diagram for recCompleteInster:

[legend]

List of all members.

Public Member Functions

• recCompleteInster (const Expr &, const std::vector< Expr > &, std::set< Expr > &, Expr)
• Expr inst ()

Private Member Functions

• void inst_helper (int num_vars)

Private Attributes

• const Expr & d_body
• const std::vector< Expr > & d_bvs
• std::vector< Expr > d_buff
• const std::set< Expr > & d_all_index
• Expr d_result

---

Detailed Description

Definition at line 2140 of file theory_quant.cpp.

---

Constructor & Destructor Documentation

recCompleteInster::recCompleteInster	(	const Expr &	body,
		const std::vector< Expr > &	bvs,
		std::set< Expr > &	all_index,
		Expr	res
	)

Definition at line 2152 of file theory_quant.cpp.

---

Member Function Documentation

void recCompleteInster::inst_helper

(

int

num_vars

)

[private]

Definition at line 2161 of file theory_quant.cpp.

References CVC3::Expr::andExpr(), d_all_index, d_body, d_buff, d_bvs, d_result, and CVC3::Expr::substExpr().

Referenced by inst().

Expr recCompleteInster::inst

(

)

Definition at line 2154 of file theory_quant.cpp.

References d_buff, d_bvs, d_result, and inst_helper().

Referenced by CVC3::CompleteInstPreProcessor::inst().

---

Member Data Documentation

const Expr& recCompleteInster::d_body [private]

Definition at line 2141 of file theory_quant.cpp.

Referenced by inst_helper().

const std::vector<Expr>& recCompleteInster::d_bvs [private]

Definition at line 2142 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

std::vector<Expr> recCompleteInster::d_buff [private]

Definition at line 2143 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

const std::set<Expr>& recCompleteInster::d_all_index [private]

Definition at line 2144 of file theory_quant.cpp.

Referenced by inst_helper().

Expr recCompleteInster::d_result [private]

Definition at line 2145 of file theory_quant.cpp.

Referenced by inst(), and inst_helper().

---

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

• theory_quant.cpp