Logo Search packages:      
Sourcecode: undertaker version File versions  Download package

Classes | Public Types | Public Member Functions | Static Public Member Functions | Private Types | Private Member Functions | Private Attributes

SatChecker Class Reference

Collaboration diagram for SatChecker:
Collaboration graph

List of all members.


struct  AssignmentMap
 Representation of a variable selection. More...

Public Types

enum  Debug { DEBUG_NONE = 0, DEBUG_PARSER = 1, DEBUG_CNF = 2 }
typedef char const * iterator_t
typedef tree_match< iterator_t > parse_tree_match_t

Public Member Functions

const char * c_str ()
const AssignmentMapgetAssignment ()
bool operator() () throw (SatCheckerError)
std::string pprint ()
clock_t runtime ()
 SatChecker (const char *sat, int debug=0)
 SatChecker (const std::string sat, int debug=0)
const std::string str ()

Static Public Member Functions

static bool check (const std::string &sat) throw (SatCheckerError)
static int formatConfigItems (AssignmentMap solution, std::ostream &out, const MissingSet &missingSet)
 format solutions
static std::string pprinter (const char *sat)

Private Types

enum  state { no, yes, module }

Private Member Functions

void _debug_parser (std::string d="", bool newblock=true)
void addClause (int *clause)
int andClause (int A_clause, int B_clause)
void fillSatChecker (tree_parse_info<> &info)
void fillSatChecker (std::string expression) throw (SatCheckerError)
int newSymbol (void)
int notClause (int inner_clause)
int orClause (int A_clause, int B_clause)
int stringToSymbol (const std::string &key)
int transform_bool_rec (iter_t const &input)

Private Attributes

clock_t _runtime
const std::string _sat
AssignmentMap assignmentTable
std::string debug_cnf
int debug_flags
std::string debug_parser
int debug_parser_indent
std::map< std::string, int > symbolTable

Detailed Description

Definition at line 58 of file SatChecker.h.

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

Generated by  Doxygen 1.6.0   Back to index