LFSCPrinter Class Reference

Collaboration diagram for LFSCPrinter:

[legend]List of all members.

Public Member Functions

• LFSCPrinter (const Expr, const Expr)
• void print (const Expr &pf)

Private Member Functions

• void collect_assumps (const Expr &pf, ExprMap< bool > &)
• string new_name ()
• void print_helper (const Expr &pf, bool definition=false)
• void print_clause (const Expr &)

Private Attributes

• const Expr d_bool_res_str
• const Expr d_assump_str
• ExprMap< string > d_assump_map
• ExprMap< string > d_let_map
• ExprMap< bool > d_visited

---

Detailed Description

Definition at line 1393 of file search_theorem_producer.cpp.

---

Constructor & Destructor Documentation

LFSCPrinter::LFSCPrinter	(	const	Expr,
		const	Expr
	)

Definition at line 1443 of file search_theorem_producer.cpp.

---

Member Function Documentation

void LFSCPrinter::collect_assumps	(	const Expr &	pf,
		ExprMap< bool > &
	)			[private]

Definition at line 1421 of file search_theorem_producer.cpp.

References CVC3::Expr::begin(), CVC3::ExprMap< Data >::count(), d_assump_map, d_assump_str, d_let_map, is_leaf(), and new_name().

Referenced by print().

string LFSCPrinter::new_name

(

)

[private]

Definition at line 1408 of file search_theorem_producer.cpp.

Referenced by collect_assumps().

void LFSCPrinter::print_helper	(	const Expr &	pf,
		bool	definition = false
	)			[private]

Definition at line 1507 of file search_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::ExprMap< Data >::count(), d_assump_map, d_assump_str, d_bool_res_str, d_let_map, std::endl(), and CVC3::Expr::isNot().

Referenced by print().

void LFSCPrinter::print_clause

(

const Expr &

)

[private]

Definition at line 1447 of file search_theorem_producer.cpp.

References CVC3::Expr::arity(), std::endl(), and CVC3::Expr::isOr().

Referenced by print().

void LFSCPrinter::print

(

const Expr &

pf

)

Definition at line 1472 of file search_theorem_producer.cpp.

References CVC3::ExprMap< Data >::begin(), collect_assumps(), d_assump_map, d_let_map, CVC3::ExprMap< Data >::end(), std::endl(), print_clause(), and print_helper().

Referenced by CVC3::SearchEngineTheoremProducer::satProof().

---

Member Data Documentation

const Expr LFSCPrinter::d_bool_res_str [private]

Definition at line 1394 of file search_theorem_producer.cpp.

Referenced by print_helper().

const Expr LFSCPrinter::d_assump_str [private]

Definition at line 1395 of file search_theorem_producer.cpp.

Referenced by collect_assumps(), and print_helper().

ExprMap<string> LFSCPrinter::d_assump_map [private]

Definition at line 1396 of file search_theorem_producer.cpp.

Referenced by collect_assumps(), print(), and print_helper().

ExprMap<string> LFSCPrinter::d_let_map [private]

Definition at line 1397 of file search_theorem_producer.cpp.

Referenced by collect_assumps(), print(), and print_helper().

ExprMap<bool> LFSCPrinter::d_visited [private]

Definition at line 1398 of file search_theorem_producer.cpp.

---

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

• search_theorem_producer.cpp

---