CVC3::SearchImplBase Class Reference
[Search Engine]

API to to a generic proof search engine (a.k.a. SAT solver). More...

#include <search_impl_base.h>

Inheritance diagram for CVC3::SearchImplBase:

Inheritance graph
[legend]
Collaboration diagram for CVC3::SearchImplBase:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Protected Member Functions

Protected Attributes

CNF Caches
These caches are for subexpressions of the translated formula phi, to avoid expanding phi into a tree. We cannot use d_cnfCache for that, since it is effectively non-backtracking, and we do not know if a subexpression of phi was translated at the current level, or at some other (inactive) branch of the decision tree.

Private Member Functions

Friends

Classes


Detailed Description

API to to a generic proof search engine (a.k.a. SAT solver).

Definition at line 37 of file search_impl_base.h.


Friends And Related Function Documentation

friend class DecisionEngine [friend]

Definition at line 38 of file search_impl_base.h.


The documentation for this class was generated from the following files:
Generated on Wed Nov 18 16:15:47 2009 for CVC3 by  doxygen 1.5.2