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

Detailed Description

Definition at line 1393 of file search_theorem_producer.cpp.

Constructor & Destructor Documentation

LFSCPrinter::LFSCPrinter	(	const Expr	b_str,
		const Expr	a_str
	)

Definition at line 1443 of file search_theorem_producer.cpp.

Member Function Documentation

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

Definition at line 1421 of file search_theorem_producer.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::ExprMap< Data >::count(), d_assump_map, d_assump_str, d_let_map, CVC3::Expr::end(), 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 & clause ) [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