A class for defining a SAT-problem in CNF. More...
#include <program_builder.h>
Inheritance diagram for Clasp::SatBuilder:
Public Member Functions | |
| bool | addClause (LitVec &clause, wsum_t cw=0) |
| Adds the given clause to the problem. | |
| Var | numVars () const |
| Returns the number of variables in the problem. | |
| void | prepareProblem (uint32 numVars, wsum_t hardClauseWeight=0, uint32 clauseHint=100) |
| Creates necessary variables and prepares the problem. | |
| SatBuilder (bool maxSat=false) | |
Private Types | |
| typedef PodVector< uint8 >::type | VarState |
Private Member Functions | |
| bool | doEndProgram () |
| void | doGetAssumptions (LitVec &) const |
| bool | doParse (StreamSource &prg) |
| Parses prg as a SAT-problem in DIMACS-format. | |
| bool | doStartProgram () |
| int | doType () const |
| bool | doUpdateProgram () |
| bool | markAssigned () |
| void | markLit (Literal x) |
| bool | satisfied (LitVec &clause) |
Private Attributes | |
| wsum_t | hardWeight_ |
| bool | maxSat_ |
| uint32 | pos_ |
| LitVec | softClauses_ |
| Var | vars_ |
| VarState | varState_ |
Detailed Description
A class for defining a SAT-problem in CNF.
Definition at line 109 of file program_builder.h.
The documentation for this class was generated from the following files: