Classes
class	Clasp::PBBuilder
	A class for defining a PB-problem. More...
class	Clasp::Asp::Preprocessor
	Preprocesses (i.e. simplifies) a logic program. More...
class	Clasp::ProgramBuilder
	Interface for defining an input program. More...
class	Clasp::Asp::Rule
	A rule of a logic program. More...
class	Clasp::Asp::RuleState
	Used during rule simplification. More...
class	Clasp::SatBuilder
	A class for defining a SAT-problem in CNF. More...
Typedefs
typedef SingleOwnerPtr < MinimizeBuilder >	Clasp::ProgramBuilder::MinBuildPtr
typedef SingleOwnerPtr < SharedMinimize, ReleaseObject >	Clasp::ProgramBuilder::MinPtr
typedef std::map< LitVec, Literal >	Clasp::PBBuilder::ProductIndex
typedef SharedMinimizeData	Clasp::ProgramBuilder::SharedMinimize
typedef PodVector< uint8 >::type	Clasp::SatBuilder::VarState
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
bool	Clasp::SatBuilder::addClause (LitVec &clause, wsum_t cw=0)
	Adds the given clause to the problem.
bool	Clasp::PBBuilder::addConstraint (WeightLitVec &lits, weight_t bound, bool eq=false, weight_t cw=0)
	Adds the given PB-constraint to the problem.
void	Clasp::ProgramBuilder::addMinLit (WeightLiteral x)
void	Clasp::ProgramBuilder::addMinRule (const WeightLitVec &lits)
bool	Clasp::PBBuilder::addObjective (const WeightLitVec &min)
	Adds min as an objective function to the problem.
Literal	Clasp::PBBuilder::addProduct (LitVec &lits)
	Adds the given product to the problem.
void	Clasp::PBBuilder::addProductConstraints (Literal eqLit, LitVec &lits)
SharedContext *	Clasp::ProgramBuilder::ctx () const
	Returns the stored context object.
void	Clasp::ProgramBuilder::disposeMin ()
void	Clasp::ProgramBuilder::disposeMinimizeConstraint ()
	Removes a previously created minimize constraint.
virtual bool	Clasp::ProgramBuilder::doEndProgram ()=0
bool	Clasp::SatBuilder::doEndProgram ()
bool	Clasp::PBBuilder::doEndProgram ()
virtual void	Clasp::ProgramBuilder::doGetAssumptions (LitVec &out) const =0
void	Clasp::SatBuilder::doGetAssumptions (LitVec &) const
void	Clasp::PBBuilder::doGetAssumptions (LitVec &) const
virtual bool	Clasp::ProgramBuilder::doParse (StreamSource &prg)=0
bool	Clasp::SatBuilder::doParse (StreamSource &prg)
	Parses prg as a SAT-problem in DIMACS-format.
bool	Clasp::PBBuilder::doParse (StreamSource &prg)
	Parses prg as a PB-problem in OPB-format.
virtual bool	Clasp::ProgramBuilder::doStartProgram ()=0
bool	Clasp::SatBuilder::doStartProgram ()
bool	Clasp::PBBuilder::doStartProgram ()
virtual int	Clasp::ProgramBuilder::doType () const =0
int	Clasp::SatBuilder::doType () const
int	Clasp::PBBuilder::doType () const
virtual bool	Clasp::ProgramBuilder::doUpdateProgram ()=0
bool	Clasp::SatBuilder::doUpdateProgram ()
bool	Clasp::PBBuilder::doUpdateProgram ()
bool	Clasp::ProgramBuilder::endProgram ()
	Loads the program into the shared context passed to startProgram().
bool	Clasp::ProgramBuilder::frozen () const
	Returns true if the program is currently frozen.
void	Clasp::ProgramBuilder::getAssumptions (LitVec &out) const
	Returns any assumptions that shall hold during solving.
virtual void	Clasp::ProgramBuilder::getMinBound (SumVec &out) const
void	Clasp::PBBuilder::getMinBound (SumVec &out) const
SharedMinimize *	Clasp::ProgramBuilder::getMinimizeConstraint (SumVec *softBound=0) const
	Returns an optimized representation of the program's minimize statements (if any).
Var	Clasp::PBBuilder::getNextVar ()
bool	Clasp::SatBuilder::markAssigned ()
void	Clasp::SatBuilder::markLit (Literal x)
Var	Clasp::SatBuilder::numVars () const
	Returns the number of variables in the problem.
uint32	Clasp::PBBuilder::numVars () const
	Returns the number of variables in the problem.
virtual bool	Clasp::ProgramBuilder::ok () const
	Returns true if the program is not conflicting.
ProgramBuilder &	Clasp::ProgramBuilder::operator= (ProgramBuilder &)
bool	Clasp::ProgramBuilder::parseProgram (StreamSource &prg)
	Parses the given stream as a program of type() and adds it to this object.
bool	Clasp::ProgramBuilder::parseProgram (std::istream &prg)
	Clasp::PBBuilder::PBBuilder ()
void	Clasp::SatBuilder::prepareProblem (uint32 numVars, wsum_t hardClauseWeight=0, uint32 clauseHint=100)
	Creates necessary variables and prepares the problem.
void	Clasp::PBBuilder::prepareProblem (uint32 numVars, uint32 maxProduct, uint32 maxSoft, uint32 constraintHint=100)
	Creates necessary variables and prepares the problem.
bool	Clasp::PBBuilder::productSubsumed (LitVec &lits, Literal &subLit)
	Clasp::ProgramBuilder::ProgramBuilder ()
	Clasp::ProgramBuilder::ProgramBuilder (const ProgramBuilder &)
	Clasp::SatBuilder::SatBuilder (bool maxSat=false)
bool	Clasp::SatBuilder::satisfied (LitVec &clause)
void	Clasp::ProgramBuilder::setCtx (SharedContext *x)
void	Clasp::ProgramBuilder::setFrozen (bool frozen)
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.
int	Clasp::ProgramBuilder::type () const
	Returns the type of program that is created by this builder.
bool	Clasp::ProgramBuilder::updateProgram ()
	Unfreezes a currently frozen program.
virtual	Clasp::ProgramBuilder::~ProgramBuilder ()
Variables
SharedContext *	Clasp::ProgramBuilder::ctx_
bool	Clasp::ProgramBuilder::frozen_
wsum_t	Clasp::SatBuilder::hardWeight_
bool	Clasp::SatBuilder::maxSat_
uint32	Clasp::PBBuilder::maxVar_
MinBuildPtr	Clasp::ProgramBuilder::min_
MinPtr	Clasp::ProgramBuilder::minCon_
uint32	Clasp::PBBuilder::nextVar_
uint32	Clasp::SatBuilder::pos_
ProductIndex	Clasp::PBBuilder::products_
wsum_t	Clasp::PBBuilder::soft_
LitVec	Clasp::SatBuilder::softClauses_
Var	Clasp::SatBuilder::vars_
VarState	Clasp::SatBuilder::varState_

Detailed Description

Classes and functions for defining input programs.

Typedef Documentation

typedef SingleOwnerPtr<MinimizeBuilder> Clasp::ProgramBuilder::MinBuildPtr [private]

Definition at line 92 of file program_builder.h.

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

Definition at line 46 of file program_builder.h.

typedef std::map<LitVec, Literal> Clasp::PBBuilder::ProductIndex [private]

Definition at line 200 of file program_builder.h.

typedef SharedMinimizeData Clasp::ProgramBuilder::SharedMinimize

Definition at line 45 of file program_builder.h.

typedef PodVector<uint8>::type Clasp::SatBuilder::VarState [private]

Definition at line 140 of file program_builder.h.

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

Definition at line 43 of file logic_program_types.h.

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.

Definition at line 115 of file program_builder.cpp.

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.

Definition at line 202 of file program_builder.cpp.

void Clasp::ProgramBuilder::addMinLit ( WeightLiteral x ) [protected]

Definition at line 79 of file program_builder.cpp.

void Clasp::ProgramBuilder::addMinRule ( const WeightLitVec & lits ) [protected]

Definition at line 80 of file program_builder.cpp.

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

Adds min as an objective function to the problem.

Definition at line 220 of file program_builder.cpp.

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().

Definition at line 237 of file program_builder.cpp.

void Clasp::PBBuilder::addProductConstraints	(	Literal	eqLit,
		LitVec &	lits
	)		`[private]`

Definition at line 271 of file program_builder.cpp.

SharedContext* Clasp::ProgramBuilder::ctx ( ) const [inline]

Returns the stored context object.

Definition at line 84 of file program_builder.h.

void Clasp::ProgramBuilder::disposeMin ( ) [protected]

Definition at line 81 of file program_builder.cpp.

void Clasp::ProgramBuilder::disposeMinimizeConstraint ( )

Removes a previously created minimize constraint.

Definition at line 82 of file program_builder.cpp.

virtual bool Clasp::ProgramBuilder::doEndProgram ( ) [private, pure virtual]

Implemented in Clasp::Asp::LogicProgram, Clasp::PBBuilder, and Clasp::SatBuilder.

bool Clasp::SatBuilder::doEndProgram ( ) [private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 154 of file program_builder.cpp.

bool Clasp::PBBuilder::doEndProgram ( ) [private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 289 of file program_builder.cpp.

virtual void Clasp::ProgramBuilder::doGetAssumptions ( LitVec & out ) const [private, pure virtual]

Implemented in Clasp::PBBuilder.

void Clasp::SatBuilder::doGetAssumptions ( LitVec & ) const [inline, private]

Definition at line 146 of file program_builder.h.

void Clasp::PBBuilder::doGetAssumptions ( LitVec & ) const [inline, private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 205 of file program_builder.h.

virtual bool Clasp::ProgramBuilder::doParse ( StreamSource & prg ) [private, pure virtual]

Implemented in Clasp::Asp::LogicProgram, Clasp::PBBuilder, and Clasp::SatBuilder.

bool Clasp::SatBuilder::doParse ( StreamSource & prg ) [private, virtual]

Parses prg as a SAT-problem in DIMACS-format.

Implements Clasp::ProgramBuilder.

Definition at line 153 of file program_builder.cpp.

bool Clasp::PBBuilder::doParse ( StreamSource & prg ) [private, virtual]

Parses prg as a PB-problem in OPB-format.

Implements Clasp::ProgramBuilder.

Definition at line 295 of file program_builder.cpp.

virtual bool Clasp::ProgramBuilder::doStartProgram ( ) [private, pure virtual]

Implemented in Clasp::Asp::LogicProgram, Clasp::PBBuilder, and Clasp::SatBuilder.

bool Clasp::SatBuilder::doStartProgram ( ) [private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 148 of file program_builder.cpp.

bool Clasp::PBBuilder::doStartProgram ( ) [private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 284 of file program_builder.cpp.

virtual int Clasp::ProgramBuilder::doType ( ) const [private, pure virtual]

Implemented in Clasp::Asp::LogicProgram, Clasp::PBBuilder, and Clasp::SatBuilder.

int Clasp::SatBuilder::doType ( ) const [inline, private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 144 of file program_builder.h.

int Clasp::PBBuilder::doType ( ) const [inline, private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 203 of file program_builder.h.

virtual bool Clasp::ProgramBuilder::doUpdateProgram ( ) [private, pure virtual]

Implemented in Clasp::Asp::LogicProgram, Clasp::PBBuilder, and Clasp::SatBuilder.

bool Clasp::SatBuilder::doUpdateProgram ( ) [inline, private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 145 of file program_builder.h.

bool Clasp::PBBuilder::doUpdateProgram ( ) [inline, private, virtual]

Implements Clasp::ProgramBuilder.

Definition at line 204 of file program_builder.h.

bool Clasp::ProgramBuilder::endProgram ( )

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

Definition at line 54 of file program_builder.cpp.

bool Clasp::ProgramBuilder::frozen ( ) const [inline]

Returns true if the program is currently frozen.

Definition at line 80 of file program_builder.h.

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

Returns any assumptions that shall hold during solving.

Precondition:: frozen()

Definition at line 64 of file program_builder.cpp.

void Clasp::ProgramBuilder::getMinBound ( SumVec & out ) const [private, virtual]

Definition at line 83 of file program_builder.cpp.

void Clasp::PBBuilder::getMinBound ( SumVec & out ) const [private]

Definition at line 230 of file program_builder.cpp.

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.

Definition at line 84 of file program_builder.cpp.

uint32 Clasp::PBBuilder::getNextVar ( ) [private]

Definition at line 198 of file program_builder.cpp.

bool Clasp::SatBuilder::markAssigned ( ) [private]

Definition at line 96 of file program_builder.cpp.

void Clasp::SatBuilder::markLit ( Literal x ) [inline, private]

Definition at line 150 of file program_builder.h.

Var Clasp::SatBuilder::numVars ( ) const [inline]

Returns the number of variables in the problem.

Definition at line 124 of file program_builder.h.

uint32 Clasp::PBBuilder::numVars ( ) const [inline]

Returns the number of variables in the problem.

Definition at line 173 of file program_builder.h.

bool Clasp::ProgramBuilder::ok ( ) const [virtual]

Returns true if the program is not conflicting.

Reimplemented in Clasp::Asp::LogicProgram.

Definition at line 35 of file program_builder.cpp.

ProgramBuilder& Clasp::ProgramBuilder::operator= ( ProgramBuilder & ) [private]

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

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

Definition at line 71 of file program_builder.cpp.

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

Definition at line 75 of file program_builder.cpp.

Clasp::PBBuilder::PBBuilder ( )

Definition at line 187 of file program_builder.cpp.

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.

Definition at line 104 of file program_builder.cpp.

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.

Definition at line 188 of file program_builder.cpp.