A class for defining a logic program. More...

#include <logic_program.h>

Inheritance diagram for Clasp::Asp::LogicProgram:

Collaboration diagram for Clasp::Asp::LogicProgram:

Classes
struct	AspOptions
	Options for the Asp-Preprocessor. More...

Public Types
enum	ExtendedRuleMode { mode_native = 0, mode_transform = 1, mode_transform_choice = 2, mode_transform_card = 3, mode_transform_weight = 4, mode_transform_scc = 5, mode_transform_nhcf = 6, mode_transform_integ = 7, mode_transform_dynamic = 8 }
	Defines the possible modes for handling extended rules, i.e. choice, cardinality, and weight rules. More...

Public Types inherited from Clasp::ProgramBuilder
typedef SharedMinimizeData	SharedMinimize

typedef SingleOwnerPtr < SharedMinimize, ReleaseObject >	MinPtr

Public Member Functions
	LogicProgram ()

	~LogicProgram ()

Step control functions
LogicProgram &	start (SharedContext &ctx, const AspOptions &opts=AspOptions())
	Starts the definition of a logic program. More...

void	setExtendedRuleMode (ExtendedRuleMode m)
	Sets the mode for handling extended rules (default: mode_native). More...

void	setOptions (const AspOptions &opts)
	Sets preprocessing options. More...

void	setNonHcfConfiguration (Configuration *c)
	Sets the configuration to be used for checker solvers in disjunctive LP solving. More...

bool	update ()
	Unfreezes a currently frozen program and starts an incremental step. More...

bool	end ()
	Finishes the definition of the logic program (or its current increment). More...

void	write (std::ostream &os)
	Writes the (possibly simplified) program in lparse-format to the given stream. More...

void	dispose (bool forceFullDispose)
	Disposes (parts of) the internal representation of the logic program. More...

bool	clone (SharedContext &ctx, bool shareSymbols=false)
	Clones the program and adds it to the given ctx. More...

Program mutating functions
Functions in this group shall only be called if the program is currently not frozen. That is, only between the call to start() (resp. update() if in incremental setting) and end(). A std::logic_error is raised if this precondition is violated.
Var	newAtom ()
	Adds a new atom to the program. More...

LogicProgram &	setAtomName (Var atomId, const char *name)
	Sets the name of the given atom and adds it to the program's symbol table. More...

LogicProgram &	setCompute (Var atomId, bool value)
	Forces the atom's truth-value to value. More...

LogicProgram &	freeze (Var atomId, ValueRep value=value_false)
	Protects an otherwise undefined atom from preprocessing. More...

LogicProgram &	unfreeze (Var atomId)
	Removes any protection from the given atom. More...

LogicProgram &	addRule (const Rule &r)
	Adds the given rule to the program. More...

Rule creation functions
Functions in this group may be used to construct logic program rules. The construction of a rule must start with a call to startRule() and ends with a call to endRule(). Functions for adding elements to a rule shall only be called between calls to startRule()/endRule() and only one rule can be under construction at any one time.
LogicProgram &	startRule (RuleType t=BASICRULE, weight_t bound=-1)
	Starts the construction of a rule. More...

LogicProgram &	setBound (weight_t bound)
	Sets the bound (resp. min weight) of the currently active rule. More...

LogicProgram &	addHead (Var atomId)
	Adds the atom with the given id as a head to the currently active rule. More...

LogicProgram &	addToBody (Var atomId, bool pos, weight_t weight=1)
	Adds a subgoal to the currently active rule. More...

LogicProgram &	endRule ()
	Finishes the construction of the active rule and adds it to the program. 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...

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

Query functions
Functions in this group are useful to query important information once the program is frozen, i.e. after end() was called.
LpStats	stats

LpStats *	accu

bool	hasMinimize () const
	Returns whether the program contains any minimize statements. More...

uint32	numAtoms () const
	Returns the number of atoms in the logic program. More...

uint32	numBodies () const
	Returns the number of bodies in the current (slice of the) logic program. More...

uint32	numDisjunctions () const
	Returns the number of disjunctive heads. More...

Var	startAtom () const
	Returns the id of the first atom of the current step. More...

Literal	getLiteral (Var atomId) const
	Returns the internal literal that is associated with the given atom. More...

Implementation functions
Low-level implementation functions. Use with care and only if you know what you are doing!
typedef VarVec::const_iterator	VarIter

typedef PrgHead const	HeadIter

typedef std::pair < EdgeIterator, EdgeIterator >	EdgeRange

typedef std::pair< HeadIter, HeadIter >	HeadRange

const AspOptions &	options () const

bool	hasConflict () const

bool	ok () const
	Returns true if the program is not conflicting. More...

PrgAtom *	getAtom (Var atomId) const

PrgHead *	getHead (PrgEdge it) const

PrgNode *	getSupp (PrgEdge it) const

Var	getEqAtom (Var a) const

PrgBody *	getBody (Var bodyId) const

Var	getEqBody (Var b) const

PrgDisj *	getDisj (Var disjId) const

bool	isFact (PrgAtom *a) const

HeadIter	disj_begin () const

HeadIter	disj_end () const

HeadIter	atom_begin () const

HeadIter	atom_end () const

VarIter	unfreeze_begin () const

VarIter	unfreeze_end () const

const char *	getAtomName (Var id) const

RuleType	simplifyRule (const Rule &r, VarVec &head, BodyInfo &info)

VarVec &	getSupportedBodies (bool sorted)

uint32	update (PrgBody *b, uint32 oldHash, uint32 newHash)

bool	assignValue (PrgAtom *a, ValueRep v)

bool	assignValue (PrgHead *h, ValueRep v)

bool	propagate (bool backprop)

PrgAtom *	mergeEqAtoms (PrgAtom *a, Var rootAtom)

PrgBody *	mergeEqBodies (PrgBody *b, Var rootBody, bool hashEq, bool atomsAssigned)

bool	propagate ()

void	setConflict ()

RuleState &	ruleState ()

void	addMinimize ()

void	upRules (RuleType r, int i)

void	incTr (RuleType r, uint32 n)

void	incTrAux (uint32 n)

void	incEqs (VarType t)

Additional Inherited Members
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)

Detailed Description

A class for defining a logic program.

Use this class to specify a logic program. Once the program is completly defined, call endProgram() to load the logic program into a SharedContext object.

Member Typedef Documentation

typedef std::pair<EdgeIterator, EdgeIterator> Clasp::Asp::LogicProgram::EdgeRange

typedef PrgHead* const* Clasp::Asp::LogicProgram::HeadIter

typedef std::pair<HeadIter, HeadIter> Clasp::Asp::LogicProgram::HeadRange

typedef VarVec::const_iterator Clasp::Asp::LogicProgram::VarIter

Member Enumeration Documentation

enum Clasp::Asp::LogicProgram::ExtendedRuleMode

Defines the possible modes for handling extended rules, i.e. choice, cardinality, and weight rules.

Enumerator
mode_native	Handle extended rules natively.
mode_transform	Transform extended rules to normal rules.
mode_transform_choice	Transform only choice rules to normal rules.
mode_transform_card	Transform only cardinality rules to normal rules.
mode_transform_weight	Transform cardinality- and weight rules to normal rules.
mode_transform_scc	Transform recursive cardinality- and weight rules to normal rules.
mode_transform_nhcf	Transform cardinality- and weight rules in non-hcf components to normal rules.
mode_transform_integ	Transform cardinality-based integrity constraints.
mode_transform_dynamic	Heuristically decide whether or not to transform a particular extended rule.

Constructor & Destructor Documentation

Clasp::Asp::LogicProgram::LogicProgram ( )

Clasp::Asp::LogicProgram::~LogicProgram ( )

Here is the call graph for this function:

Member Function Documentation

LogicProgram& Clasp::Asp::LogicProgram::addHead ( Var atomId )

inline

Adds the atom with the given id as a head to the currently active rule.

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::addMinimize ( )

Here is the call graph for this function:

LogicProgram & Clasp::Asp::LogicProgram::addRule ( const Rule & r )

Adds the given rule to the program.

Precondition: The head of the rule does not contain an atom defined in a previous incremental step.

Simplifies the given rule and adds it to the program if it is neither tautological (e.g. a :- a) nor contradictory (e.g. a :- b, not b). Atoms in the simplified rule that are not yet known are implicitly created.

Exceptions

RedefinitionError if the precondition is violated.

Note: If the head of the simplified rule mentions an atom from a previous step, that atom shall either be frozen or false. In the former case, unfreeze() is implicitly called. In the latter case, the rule is interpreted as an integrity constraint.

Here is the call graph for this function:

LogicProgram& Clasp::Asp::LogicProgram::addToBody	(	Var	atomId,
		bool	pos,
		weight_t	weight = `1`
	)

inline

Adds a subgoal to the currently active rule.

Precondition: atomId > 0 && weight >= 0

Parameters

atomId	The id of the atom to be added to the rule.
pos	true if the atom is positive. Fals otherwise
weight	The weight the new predecessor should have in the rule.

Note: The weight parameter is only used if the active rule is a weight or optimize rule.

Here is the call graph for this function:

bool Clasp::Asp::LogicProgram::assignValue	(	PrgAtom *	a,
		ValueRep	v
	)

Here is the call graph for this function:

bool Clasp::Asp::LogicProgram::assignValue	(	PrgHead *	h,
		ValueRep	v
	)

Here is the call graph for this function:

HeadIter Clasp::Asp::LogicProgram::atom_begin ( ) const

inline

HeadIter Clasp::Asp::LogicProgram::atom_end ( ) const

inline

Here is the call graph for this function:

bool Clasp::Asp::LogicProgram::clone	(	SharedContext &	ctx,
		bool	shareSymbols = `false`
	)

Clones the program and adds it to the given ctx.

Here is the call graph for this function:

HeadIter Clasp::Asp::LogicProgram::disj_begin ( ) const

inline

HeadIter Clasp::Asp::LogicProgram::disj_end ( ) const

inline

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::dispose ( bool forceFullDispose )

Disposes (parts of) the internal representation of the logic program.

Parameters

forceFullDispose If set to true, the whole program is disposed. Otherwise, only the rules (of the current step) are disposed but atoms and any incremental control data remain.

Here is the call graph for this function:

bool Clasp::Asp::LogicProgram::end ( )

inline

Finishes the definition of the logic program (or its current increment).

Applies program mutating operations issued in the current step and transforms the new program into the solver's internal representation.

Returns: false if the program is conflicting, true otherwise.

Postcondition

If true is returned, the program is considered to be "frozen" and calling program mutating functions is invalid until the next call to update().
If false is returned, the state of the object is undefined and start() and dispose() are the only remaining valid operations.

Note: The function is an alias for ProgramBuilder::endProgram().

Here is the call graph for this function:

LogicProgram& Clasp::Asp::LogicProgram::endRule ( )

inline

Finishes the construction of the active rule and adds it to the program.

See also: LogicProgram::addRule(Rule&);

Here is the call graph for this function:

LogicProgram & Clasp::Asp::LogicProgram::freeze	(	Var	atomId,
		ValueRep	value = `value_false`
	)

Protects an otherwise undefined atom from preprocessing.

If the atom is defined in this or a previous step, the operation has no effect.

Note: If atomId is not yet known, an atom with the given id is implicitly created.; The second parameter defines the value that is assumed for the given atom while it is frozen. It shall be either value_false or value_true.

Here is the call graph for this function:

PrgAtom* Clasp::Asp::LogicProgram::getAtom ( Var atomId ) const

inline

const char * Clasp::Asp::LogicProgram::getAtomName ( Var id ) const

Here is the call graph for this function:

PrgBody* Clasp::Asp::LogicProgram::getBody ( Var bodyId ) const

inline

PrgDisj* Clasp::Asp::LogicProgram::getDisj ( Var disjId ) const

inline

Var Clasp::Asp::LogicProgram::getEqAtom ( Var a ) const

inline

Var Clasp::Asp::LogicProgram::getEqBody ( Var b ) const

inline

PrgHead* Clasp::Asp::LogicProgram::getHead ( PrgEdge it ) const

inline

Here is the call graph for this function:

Literal Clasp::Asp::LogicProgram::getLiteral ( Var atomId ) const

Returns the internal literal that is associated with the given atom.

Precondition: atomId is a known atom

Returns: A literal that is valid in the current solving context.

Note: Untill end() is called, atoms from the current step are associated with the always-false literal negLit(0).

Exceptions

std::logic_error if precondition is violated.

Here is the call graph for this function:

PrgNode* Clasp::Asp::LogicProgram::getSupp ( PrgEdge it ) const

inline

Here is the call graph for this function:

VarVec & Clasp::Asp::LogicProgram::getSupportedBodies ( bool sorted )

bool Clasp::Asp::LogicProgram::hasConflict ( ) const

inline

Here is the call graph for this function:

bool Clasp::Asp::LogicProgram::hasMinimize ( ) const

inline

Returns whether the program contains any minimize statements.

void Clasp::Asp::LogicProgram::incEqs ( VarType t )

inline

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::incTr	(	RuleType	r,
		uint32	n
	)

inline

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::incTrAux ( uint32 n )

inline

bool Clasp::Asp::LogicProgram::isFact ( PrgAtom * a ) const

inline

Here is the call graph for this function:

PrgAtom * Clasp::Asp::LogicProgram::mergeEqAtoms	(	PrgAtom *	a,
		Var	rootAtom
	)

Here is the call graph for this function:

PrgBody * Clasp::Asp::LogicProgram::mergeEqBodies	(	PrgBody *	b,
		Var	rootBody,
		bool	hashEq,
		bool	atomsAssigned
	)

Here is the call graph for this function:

Var Clasp::Asp::LogicProgram::newAtom ( )

Adds a new atom to the program.

Returns: The new atom's id.

uint32 Clasp::Asp::LogicProgram::numAtoms ( ) const

inline

Returns the number of atoms in the logic program.

uint32 Clasp::Asp::LogicProgram::numBodies ( ) const

inline

Returns the number of bodies in the current (slice of the) logic program.

uint32 Clasp::Asp::LogicProgram::numDisjunctions ( ) const

inline

Returns the number of disjunctive heads.

bool Clasp::Asp::LogicProgram::ok ( ) const

inlinevirtual

Returns true if the program is not conflicting.

Reimplemented from Clasp::ProgramBuilder.

Here is the call graph for this function:

const AspOptions& Clasp::Asp::LogicProgram::options ( ) const

inline

bool Clasp::Asp::LogicProgram::propagate ( bool backprop )

Here is the call graph for this function:

bool Clasp::Asp::LogicProgram::propagate ( )

inline

Here is the call graph for this function:

RuleState& Clasp::Asp::LogicProgram::ruleState ( )

inline

LogicProgram & Clasp::Asp::LogicProgram::setAtomName	(	Var	atomId,
		const char *	name
	)

Sets the name of the given atom and adds it to the program's symbol table.

Precondition

The atom is either not yet known or was added in the current step (atomId >= startAtom()).
The atom was not yet added to the symbol table, i.e. setAtomName() is called at most once for an atom.

Parameters

atomId	The id of the atom for which a name should be set
name	The new name of the atom with the given id.

Note: If atomId is not yet known, an atom with the given id is implicitly created.

Exceptions

RedefinitionError	precondition is violated.
std::logic_error	program is frozen.

Here is the call graph for this function:

LogicProgram& Clasp::Asp::LogicProgram::setBound ( weight_t bound )

inline

Sets the bound (resp. min weight) of the currently active rule.

Parameters

bound The lower bound (resp. min weight) of the rule to be created.

Precondition: The rule under construction is either a constraint or weight rule.

Here is the call graph for this function:

LogicProgram & Clasp::Asp::LogicProgram::setCompute	(	Var	atomId,
		bool	value
	)

Forces the atom's truth-value to value.

Precondition: The atom is either not yet known, false, or an atom from the current step.

Parameters

atomId	Id of the Atom for which a truth-value should be set.
pos	If true, atom is set to true (forced to be in every answer set). Otherwise atom is set to false (not part of any answer set).

Note: If atomId is not yet known, an atom with the given id is implicitly created.

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::setConflict ( )

inline

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::setExtendedRuleMode ( ExtendedRuleMode m )

inline

Sets the mode for handling extended rules (default: mode_native).

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::setNonHcfConfiguration ( Configuration * c )

inline

Sets the configuration to be used for checker solvers in disjunctive LP solving.

void Clasp::Asp::LogicProgram::setOptions ( const AspOptions & opts )

Sets preprocessing options.

Here is the call graph for this function:

RuleType Clasp::Asp::LogicProgram::simplifyRule	(	const Rule &	r,
		VarVec &	head,
		BodyInfo &	info
	)

Here is the call graph for this function:

LogicProgram& Clasp::Asp::LogicProgram::start	(	SharedContext &	ctx,
		const AspOptions &	opts = `AspOptions()`
	)

inline

Starts the definition of a logic program.

Here is the call graph for this function:

Var Clasp::Asp::LogicProgram::startAtom ( ) const

inline

Returns the id of the first atom of the current step.

LogicProgram& Clasp::Asp::LogicProgram::startRule	(	RuleType	t = `BASICRULE`,
		weight_t	bound = `-1`
	)

inline

Starts the construction of a rule.

Parameters

t	The type of the new rule.
bound	The lower bound (resp. min weight) of the rule to be created.

Note: the bound-parameter is only interpreted if the rule to be created is either a constraint- or a weight-rule.

Here is the call graph for this function:

LogicProgram & Clasp::Asp::LogicProgram::unfreeze ( Var atomId )

Removes any protection from the given atom.

If the atom is defined in this or a previous step, the operation has no effect.

Note

The effect is logically equivalent to adding a rule atomId :- false.
A call to unfreeze() always overwrites a call to freeze() even if the latter comes after the former

Here is the call graph for this function:

VarIter Clasp::Asp::LogicProgram::unfreeze_begin ( ) const

inline

VarIter Clasp::Asp::LogicProgram::unfreeze_end ( ) const

inline

bool Clasp::Asp::LogicProgram::update ( )

inline

Unfreezes a currently frozen program and starts an incremental step.

If a program is to be defined incrementally, this function must be called exactly once for each step before any new rules or atoms are added.

Note

Program update only works correctly under the following assumptions:

Atoms introduced in step i are either:
- solely defined in step i OR,
- marked as frozen in step i and solely defined in step i+k OR,
- forced to false by a acompute statement in step 0

Precondition: The program is either frozen or at step 0.

Postcondition: The program is no longer frozen and calling program mutating functions is valid again.

Exceptions

std::logic_error precondition is violated.

Note: The function is an alias for ProgramBuilder::updateProgram().

Here is the call graph for this function:

uint32 Clasp::Asp::LogicProgram::update	(	PrgBody *	b,
		uint32	oldHash,
		uint32	newHash
	)

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::upRules	(	RuleType	r,
		int	i
	)

inline

Here is the call graph for this function:

void Clasp::Asp::LogicProgram::write ( std::ostream & os )

Writes the (possibly simplified) program in lparse-format to the given stream.

Here is the call graph for this function:

Member Data Documentation

LpStats* Clasp::Asp::LogicProgram::accu

LpStats Clasp::Asp::LogicProgram::stats

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

/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/logic_program.h
/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/logic_program.cpp

Classes

Public Types

Public Member Functions

Query functions

Implementation functions

Additional Inherited Members

Detailed Description

Member Typedef Documentation

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation