CVC3 2.2
Public Member Functions | Private Member Functions | Private Attributes

LFSCPrinter Class Reference

List of all members.

Public Member Functions

Private Member Functions

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]
string LFSCPrinter::new_name ( ) [private]

Definition at line 1408 of file search_theorem_producer.cpp.

void LFSCPrinter::print_helper ( const Expr pf,
bool  definition = false 
) [private]
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)

Member Data Documentation

Definition at line 1394 of file search_theorem_producer.cpp.

Referenced by print_helper().

Definition at line 1395 of file search_theorem_producer.cpp.

Referenced by print_helper().

Definition at line 1396 of file search_theorem_producer.cpp.

Referenced by print(), and print_helper().

ExprMap<string> LFSCPrinter::d_let_map [private]

Definition at line 1397 of file search_theorem_producer.cpp.

Referenced by print(), and print_helper().

Definition at line 1398 of file search_theorem_producer.cpp.


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