|
clingo
|
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Groups
|
clingo
|
A class for defining a SAT-problem in CNF. More...
#include <program_builder.h>
Public Member Functions | |
| SatBuilder (bool maxSat=false) | |
| void | prepareProblem (uint32 numVars, wsum_t hardClauseWeight=0, uint32 clauseHint=100) |
| Creates necessary variables and prepares the problem. More... | |
| Var | numVars () const |
| Returns the number of variables in the problem. More... | |
| bool | addClause (LitVec &clause, wsum_t cw=0) |
| Adds the given clause to the problem. More... | |
 Public Member Functions inherited from Clasp::ProgramBuilder | |
| ProgramBuilder () | |
| virtual | ~ProgramBuilder () |
| bool | startProgram (SharedContext &ctx) |
| Starts the definition of a program. More... | |
| bool | parseProgram (StreamSource &prg) |
| Parses the given stream as a program of type() and adds it to this object. More... | |
| bool | parseProgram (std::istream &prg) |
| bool | updateProgram () |
| Unfreezes a currently frozen program. More... | |
| bool | endProgram () |
| Loads the program into the shared context passed to startProgram(). More... | |
| void | getAssumptions (LitVec &out) const |
| Returns any assumptions that shall hold during solving. More... | |
| SharedMinimize * | getMinimizeConstraint (SumVec *softBound=0) const |
| Returns an optimized representation of the program's minimize statements (if any). More... | |
| void | disposeMinimizeConstraint () |
| Removes a previously created minimize constraint. More... | |
| int | type () const |
| Returns the type of program that is created by this builder. More... | |
| bool | frozen () const |
| Returns true if the program is currently frozen. More... | |
| virtual bool | ok () const |
| Returns true if the program is not conflicting. More... | |
| SharedContext * | ctx () const |
| Returns the stored context object. More... | |
Additional Inherited Members | |
| Public Types inherited from Clasp::ProgramBuilder | |
| typedef SharedMinimizeData | SharedMinimize |
| typedef SingleOwnerPtr < SharedMinimize, ReleaseObject > | MinPtr |
| Protected Member Functions inherited from Clasp::ProgramBuilder | |
| void | addMinLit (WeightLiteral x) |
| void | addMinRule (const WeightLitVec &lits) |
| void | disposeMin () |
| void | setFrozen (bool frozen) |
| void | setCtx (SharedContext *x) |
A class for defining a SAT-problem in CNF.
1.8.7