Classes
class	Clasp::Asp::Preprocessor
	Preprocesses (i.e. simplifies) a logic program. More...

class	Clasp::Asp::Rule
	A rule of a logic program. More...

class	Clasp::Asp::RuleState
	Used during rule simplification. More...

class	Clasp::ProgramBuilder
	Interface for defining an input program. More...

class	Clasp::SatBuilder
	A class for defining a SAT-problem in CNF. More...

class	Clasp::PBBuilder
	A class for defining a PB-problem. More...

Typedefs
typedef SharedMinimizeData	Clasp::ProgramBuilder::SharedMinimize

typedef SingleOwnerPtr < SharedMinimize, ReleaseObject >	Clasp::ProgramBuilder::MinPtr

Enumerations
enum	Clasp::Asp::RuleType { Clasp::Asp::ENDRULE = 0, Clasp::Asp::BASICRULE = 1, Clasp::Asp::CONSTRAINTRULE = 2, Clasp::Asp::CHOICERULE = 3, Clasp::Asp::WEIGHTRULE = 5, Clasp::Asp::OPTIMIZERULE = 6, Clasp::Asp::DISJUNCTIVERULE = 8, Clasp::Asp::NUM_RULE_TYPES = 6 }
	Supported rule-types. More...

Functions
	Clasp::ProgramBuilder::ProgramBuilder ()

virtual	Clasp::ProgramBuilder::~ProgramBuilder ()

bool	Clasp::ProgramBuilder::startProgram (SharedContext &ctx)
	Starts the definition of a program. More...

bool	Clasp::ProgramBuilder::parseProgram (StreamSource &prg)
	Parses the given stream as a program of type() and adds it to this object. More...

bool	Clasp::ProgramBuilder::parseProgram (std::istream &prg)

bool	Clasp::ProgramBuilder::updateProgram ()
	Unfreezes a currently frozen program. More...

bool	Clasp::ProgramBuilder::endProgram ()
	Loads the program into the shared context passed to startProgram(). More...

void	Clasp::ProgramBuilder::getAssumptions (LitVec &out) const
	Returns any assumptions that shall hold during solving. More...

SharedMinimize *	Clasp::ProgramBuilder::getMinimizeConstraint (SumVec *softBound=0) const
	Returns an optimized representation of the program's minimize statements (if any). More...

void	Clasp::ProgramBuilder::disposeMinimizeConstraint ()
	Removes a previously created minimize constraint. More...

int	Clasp::ProgramBuilder::type () const
	Returns the type of program that is created by this builder. More...

bool	Clasp::ProgramBuilder::frozen () const
	Returns true if the program is currently frozen. More...

virtual bool	Clasp::ProgramBuilder::ok () const
	Returns true if the program is not conflicting. More...

SharedContext *	Clasp::ProgramBuilder::ctx () const
	Returns the stored context object. More...

void	Clasp::ProgramBuilder::addMinLit (WeightLiteral x)

void	Clasp::ProgramBuilder::addMinRule (const WeightLitVec &lits)

void	Clasp::ProgramBuilder::disposeMin ()

void	Clasp::ProgramBuilder::setFrozen (bool frozen)

void	Clasp::ProgramBuilder::setCtx (SharedContext *x)

	Clasp::SatBuilder::SatBuilder (bool maxSat=false)

void	Clasp::SatBuilder::prepareProblem (uint32 numVars, wsum_t hardClauseWeight=0, uint32 clauseHint=100)
	Creates necessary variables and prepares the problem. More...

Var	Clasp::SatBuilder::numVars () const
	Returns the number of variables in the problem. More...

bool	Clasp::SatBuilder::addClause (LitVec &clause, wsum_t cw=0)
	Adds the given clause to the problem. More...

	Clasp::PBBuilder::PBBuilder ()

void	Clasp::PBBuilder::prepareProblem (uint32 numVars, uint32 maxProduct, uint32 maxSoft, uint32 constraintHint=100)
	Creates necessary variables and prepares the problem. More...

uint32	Clasp::PBBuilder::numVars () const
	Returns the number of variables in the problem. More...

bool	Clasp::PBBuilder::addConstraint (WeightLitVec &lits, weight_t bound, bool eq=false, weight_t cw=0)
	Adds the given PB-constraint to the problem. More...

Literal	Clasp::PBBuilder::addProduct (LitVec &lits)
	Adds the given product to the problem. More...

bool	Clasp::PBBuilder::addObjective (const WeightLitVec &min)
	Adds min as an objective function to the problem. More...

bool	Clasp::PBBuilder::setSoftBound (wsum_t bound)
	Only allow solutions where the sum of violated soft constraint is less than bound. More...

Detailed Description

Classes and functions for defining input programs.

Typedef Documentation

typedef SingleOwnerPtr<SharedMinimize, ReleaseObject> Clasp::ProgramBuilder::MinPtr

typedef SharedMinimizeData Clasp::ProgramBuilder::SharedMinimize

Enumeration Type Documentation

enum Clasp::Asp::RuleType

Supported rule-types.

Enumerator
ENDRULE	Not a valid rule, used as sentinel
BASICRULE	A normal rule, i.e: A0 :- A1,...,Am, not Am+1,...,not An
CONSTRAINTRULE	A cardinality constraint, i.e. A0 :- L{A1,...,Am,not Am+1,...,not An}
CHOICERULE	A choice rule, i.e. {A0,...,An} :- BODY
WEIGHTRULE	A weight constraint, i.e. A0 :- L[A1=W1,...,Am=Wm,not Am+1=Wm+1,...,not An=Wn]
OPTIMIZERULE	A minimize statement
DISJUNCTIVERULE	A disjunctive rule, i.e. A0 \| ... \| An :- BODY
NUM_RULE_TYPES	Number of different rule types

Function Documentation

bool Clasp::SatBuilder::addClause	(	LitVec &	clause,
		wsum_t	cw = `0`
	)

Adds the given clause to the problem.

The SatBuilder supports the creation of (weighted) MaxSAT problems via the creation of "soft clauses". For this, clauses added to this object have an associated weight cw. If cw does not equal hardClauseWeight (typically 0), the clause is a soft clause and not satisfying it results in a penalty of cw.

Precondition: v <= numVars(), for all variables v occuring in clause.; cw >= 0.

Parameters

clause	The clause to add.
cw	The weight associated with the clause.

Here is the call graph for this function:

bool Clasp::PBBuilder::addConstraint	(	WeightLitVec &	lits,
		weight_t	bound,
		bool	eq = `false`,
		weight_t	cw = `0`
	)

Adds the given PB-constraint to the problem.

A PB-constraint onsists of a list of weighted Boolean literals (lhs), a comparison operator (either >= or =), and an integer bound (rhs).

Precondition: v <= numVars(), for all variables v occuring in lits.; bound >= 0 && cw >= 0.

Parameters

lits	The lhs of the PB-constraint.
bound	The rhs of the PB-constraint.
eq	If true, use '=' instead of '>=' as comparison operator.
cw	If > 0, treat constraint as soft constraint with weight cw.

Here is the call graph for this function:

void Clasp::ProgramBuilder::addMinLit ( WeightLiteral x )

protected

Here is the call graph for this function:

void Clasp::ProgramBuilder::addMinRule ( const WeightLitVec & lits )

protected

Here is the call graph for this function:

bool Clasp::PBBuilder::addObjective ( const WeightLitVec & min )

Adds min as an objective function to the problem.

Here is the call graph for this function:

Literal Clasp::PBBuilder::addProduct ( LitVec & lits )

Adds the given product to the problem.

The function creates the equality x == l1 && ... && ln, where x is a new literal and each li is a literal in lits.

Precondition: The number of products added so far is < maxProduct that was given in prepareProblem().

Here is the call graph for this function:

SharedContext* Clasp::ProgramBuilder::ctx ( ) const

inline

Returns the stored context object.

void Clasp::ProgramBuilder::disposeMin ( )

protected

void Clasp::ProgramBuilder::disposeMinimizeConstraint ( )

Removes a previously created minimize constraint.

bool Clasp::ProgramBuilder::endProgram ( )

Loads the program into the shared context passed to startProgram().

Here is the call graph for this function:

bool Clasp::ProgramBuilder::frozen ( ) const

inline

Returns true if the program is currently frozen.

void Clasp::ProgramBuilder::getAssumptions ( LitVec & out ) const

Returns any assumptions that shall hold during solving.

Precondition: frozen()

Here is the call graph for this function:

SharedMinimizeData * Clasp::ProgramBuilder::getMinimizeConstraint ( SumVec * softBound = 0 ) const

Returns an optimized representation of the program's minimize statements (if any).

Note: The returned object is owned by the program, hence callers have to call share() if the minimize constraint is to be used independently from it.

Here is the call graph for this function:

Var Clasp::SatBuilder::numVars ( ) const

inline

Returns the number of variables in the problem.

uint32 Clasp::PBBuilder::numVars ( ) const

inline

Returns the number of variables in the problem.

bool Clasp::ProgramBuilder::ok ( ) const

virtual

Returns true if the program is not conflicting.

Reimplemented in Clasp::Asp::LogicProgram.

Here is the call graph for this function:

bool Clasp::ProgramBuilder::parseProgram ( StreamSource & prg )

Parses the given stream as a program of type() and adds it to this object.

Here is the call graph for this function:

bool Clasp::ProgramBuilder::parseProgram ( std::istream & prg )

Here is the call graph for this function:

Clasp::PBBuilder::PBBuilder ( )

void Clasp::SatBuilder::prepareProblem	(	uint32	numVars,
		wsum_t	hardClauseWeight = `0`,
		uint32	clauseHint = `100`
	)

Creates necessary variables and prepares the problem.

Parameters

numVars	Number of variables to create.
hardClauseWeight	Weight identifying hard clauses (0 means no weight). Clauses added with a weight != hardClauseWeight are considered soft clauses (see addClause()).
clauseHint	A hint on how many clauses will be added.

Here is the call graph for this function:

void Clasp::PBBuilder::prepareProblem	(	uint32	numVars,
		uint32	maxProduct,
		uint32	maxSoft,
		uint32	constraintHint = `100`
	)

Creates necessary variables and prepares the problem.

Parameters

numVars	Number of problem variables to create.
maxProduct	Max number of products in the problem.
maxSoft	Max number of soft constraints in the problem.
constraintHint	A hint on how many clauses will be added.

Here is the call graph for this function:

Clasp::ProgramBuilder::ProgramBuilder ( )

Clasp::SatBuilder::SatBuilder ( bool maxSat = false )

explicit

void Clasp::ProgramBuilder::setCtx ( SharedContext * x )

inlineprotected

void Clasp::ProgramBuilder::setFrozen ( bool frozen )

inlineprotected

Here is the call graph for this function:

bool Clasp::PBBuilder::setSoftBound ( wsum_t bound )

Only allow solutions where the sum of violated soft constraint is less than bound.

bool Clasp::ProgramBuilder::startProgram ( SharedContext & ctx )

Starts the definition of a program.

This function shall be called exactly once before a new program is defined. It discards any previously added program.

Parameters

ctx	The context object in which the program should be stored.

Here is the call graph for this function:

int Clasp::ProgramBuilder::type ( ) const

inline

Returns the type of program that is created by this builder.

bool Clasp::ProgramBuilder::updateProgram ( )

Unfreezes a currently frozen program.

Here is the call graph for this function:

Clasp::ProgramBuilder::~ProgramBuilder ( )

virtual

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

Enumeration Type Documentation

Function Documentation