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:
CVC3::SearchEngine CVC3::SearchEngineFast CVC3::SearchSimple

List of all members.

Classes

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


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 4 Mar 2010 for CVC3 by  doxygen 1.6.1