Functions to rewrite expressions. More...

Classes
struct	CppClingo::Input::IETerm
	A term of form coefficient times variable. More...

struct	CppClingo::Input::IE
	An inequality of form terms >= bound. More...

class	CppClingo::Input::IEInterval
	A interval of integers. More...

class	CppClingo::Input::IESolver
	A (partial) solver for inequalities. More...

class	CppClingo::Input::ProjectionMap
	Helper to gather projection related arguments. More...

class	CppClingo::Input::TheoryTermParser
	A parser for theory terms. More...

class	CppClingo::Input::TheoryAtomParser
	A parser for theory atoms. More...

class	CppClingo::Input::RewriteContext
	Helper to pass arguments to rewrite functions. More...

Typedefs
using	CppClingo::Input::IETermVec = std::vector< IETerm >
	A vector of terms representing a sum of terms.

using	CppClingo::Input::IEVec = std::vector< IE >
	A system of inequalities.

using	CppClingo::Input::IEDomain = Util::ordered_map< String, IEInterval >
	A map from variables to intervals.

using	CppClingo::Input::AuxTermVec = std::vector< std::pair< Term, Term > >
	A vector of term pairs where the second has been substituted by the first in some other term.

using	CppClingo::Input::ParamMap = Util::ordered_set< SharedString >
	Map from identifiers to constants.

template<class E >
using	CppClingo::Input::SimplifyResult = Util::ResultState< E, TruthValue >
	The result of a simplification.

using	CppClingo::Input::SimplifyTermResult = Util::ResultState< Term, bool >
	The result of a simplification.

Enumerations
enum class	CppClingo::Input::Arity : uint8_t { Arity::unary = 0 , Arity::binary = 1 }
	Enum for unary/binary operator arities. More...

enum class	CppClingo::Input::Associativity : uint8_t { Associativity::left = 0 , Associativity::right = 1 , Associativity::non_assoc = 2 }
	Enum for operator associativities. More...

enum class	CppClingo::Input::SimplifyTermFlags : uint8_t { SimplifyTermFlags::none = 0 , SimplifyTermFlags::matchable = 1 , SimplifyTermFlags::unfailable = 2 , SimplifyTermFlags::nested_matchable = 4 , SimplifyTermFlags::preserve_toplevel = 8 }
	Flags controlling simplification of terms. More...

enum class	CppClingo::Input::SimplifyLiteralFlags : uint8_t { SimplifyLiteralFlags::none = 0 , SimplifyLiteralFlags::matchable = 1 , SimplifyLiteralFlags::unfailable = 2 , SimplifyLiteralFlags::head = 4 }
	Flags controlling simplification of literals. More...

Functions
void	CppClingo::Input::rewrite (RewriteContext &ctx, Stm const &stm, StmVec &stms)
	Rewrite the given statement.

auto	CppClingo::Input::compute_bounds (RewriteContext &ctx, Stm const &stm) -> Util::ResultState< Stm >
	Compute bounds from comparisons and intervals.

auto	CppClingo::Input::analyze (SymbolStore &store, std::vector< Stm > const &stms) -> Components
	Analyze the given statements organizing them in components for grounding.

void	CppClingo::Input::analyze (Stm const &stm, SharedSigSet &provide, Util::ordered_map< SharedSig, Location > &depend)
	Analyze the given statement adding provided and dependent predicates.

auto	CppClingo::Input::unify (SymbolStore &store, Term const &a, Term const &b) -> bool
	Try to unify the two terms.

void	CppClingo::Input::visualize (Components const &comps, std::ostream &out)
	Output components in the dot language for visualization.

void	CppClingo::Input::add_term (IETermVec &terms, IETerm term)
	Add a term to a sum of terms.

auto	CppClingo::Input::simplify (IETermVec &terms) -> Number
	Simplify the given sum of terms.

auto	CppClingo::Input::project (Term const &term, ProjectionMap project) -> std::optional< Term >
	Project variables according to given projection mode.

auto	CppClingo::Input::project (Lit const &lit, ProjectionMap project) -> std::optional< Lit >
	Project variables according to given projection mode.

auto	CppClingo::Input::project (HdLit const &lit, ProjectionMap project) -> std::optional< HdLit >
	Project variables according to given projection mode.

auto	CppClingo::Input::project (BdLit const &lit, ProjectionMap project, bool in_classical_scope) -> std::optional< BdLit >
	Project variables according to given projection mode and scope.

auto	CppClingo::Input::project (RewriteOptions const &opts, Stm const &stm) -> std::optional< Stm >
	Project variables according to given projection mode.

auto	CppClingo::Input::project_anonymous (Term const &term) -> std::optional< Term >
	Project positional anonymous variables in the term.

auto	CppClingo::Input::project_anonymous (Lit const &lit) -> std::optional< Lit >
	Project anonymous variables in negated symbolic literals.

auto	CppClingo::Input::project_anonymous (HdLit const &lit) -> std::optional< HdLit >
	Project anonymous variables in (nested) negated symbolic literals.

auto	CppClingo::Input::project_anonymous (BdLit const &lit) -> std::optional< BdLit >
	Project anonymous variables in (nested) negated symbolic literals.

auto	CppClingo::Input::project_anonymous (Stm const &stm) -> std::optional< Stm >
	Project anonymous variables in (nested) negated symbolic literals.

auto	CppClingo::Input::rewrite_anonymous (Term const &term, NameGen &gen) -> std::optional< Term >
	Give anonymous variables a unique name.

auto	CppClingo::Input::rewrite_anonymous (TheoryTerm const &term, NameGen &gen) -> std::optional< TheoryTerm >
	Give anonymous variables a unique name.

auto	CppClingo::Input::rewrite_anonymous (Lit const &lit, NameGen &gen) -> std::optional< Lit >
	Give anonymous variables a unique name.

auto	CppClingo::Input::rewrite_anonymous (HdLit const &lit, NameGen &gen) -> std::optional< HdLit >
	Give anonymous variables a unique name.

auto	CppClingo::Input::rewrite_anonymous (BdLit const &lit, NameGen &gen) -> std::optional< BdLit >
	Give anonymous variables a unique name.

auto	CppClingo::Input::rewrite_anonymous (SymbolStore &store, Stm const &stm) -> std::optional< Stm >
	Give anonymous variables a unique name.

auto	CppClingo::Input::rewrite_theory (RewriteContext &ctx, Stm const &stm) -> std::optional< Stm >
	Parse theory atoms in the given statement with the given parser.

auto	CppClingo::Input::check_safety (Logger &log, Stm const &stm) -> Util::ResultState< Stm >
	Check whether the given statement is safe.

	CppClingo::Input::CLINGO_ENABLE_BITSET_ENUM (SimplifyTermFlags)
	Indicate that the enum is a bitset.

	CppClingo::Input::CLINGO_ENABLE_BITSET_ENUM (SimplifyLiteralFlags)
	Indicate that the enum is a bitset.

auto	CppClingo::Input::simplify (SimplifyTermFlags flags, RewriteContext &ctx, Term const &term) -> SimplifyTermResult
	Simplifies the given term.

auto	CppClingo::Input::simplify (SimplifyLiteralFlags flags, RewriteContext &ctx, Lit const &lit) -> SimplifyResult< Lit >
	Simplifies the given literal.

auto	CppClingo::Input::simplify (RewriteContext &ctx, HdLit const &lit) -> SimplifyResult< HdLit >
	Simplifies the given head literal.

auto	CppClingo::Input::simplify (RewriteContext &ctx, BdLit const &lit) -> SimplifyResult< BdLit >
	Simplifies the given body literal.

auto	CppClingo::Input::simplify (RewriteContext &ctx, Stm const &stm) -> SimplifyResult< Stm >
	Simplifies the given statement.

auto	CppClingo::Input::map_params (RewriteContext &ctx, Location const &loc, Symbol const &sym) -> std::variant< Symbol, Stm >
	Replace all parameters in the given fact.

auto	CppClingo::Input::map_params (RewriteContext &ctx, Term const &term) -> std::optional< Term >
	Replace all parameters in the given term.

auto	CppClingo::Input::map_params (RewriteContext &ctx, Lit const &lit) -> std::optional< Lit >
	Replace all parameters in the given literal.

auto	CppClingo::Input::map_params (RewriteContext &ctx, HdLit const &lit) -> std::optional< HdLit >
	Replace all parameters in the given head literal.

auto	CppClingo::Input::map_params (RewriteContext &ctx, BdLit const &lit) -> std::optional< BdLit >
	Replace all parameters in the given body literal.

auto	CppClingo::Input::map_params (RewriteContext &ctx, Stm const &stm) -> std::optional< Stm >
	Replace all parameters in the given statement.

auto	CppClingo::Input::unmap_params (SymbolStore &store, ParamUnmap const &map, Stm const &stm) -> std::optional< Stm >
	Replace all variables with the given names in the statement.

void	CppClingo::Input::collect_ids (Symbol const &sym, StringSet &ids)
	Collect all ids appearing in the symbol.

void	CppClingo::Input::collect_ids (Stm const &stm, StringSet &ids)
	Collect all ids appearing in the statement.

auto	CppClingo::Input::substitute (RewriteContext &ctx, Stm const &stm) -> Util::ResultState< Stm, TruthValue >
	Substitute variables in terms of form `X=term` in the statement.

auto	CppClingo::Input::unpool (RewriteContext &ctx, Term const &term) -> std::optional< std::vector< Term > >
	Remove all pooled arguments from the term.

auto	CppClingo::Input::unpool (RewriteContext &ctx, Lit const &lit) -> std::optional< std::vector< Lit > >
	Remove all pooled arguments from the literal.

auto	CppClingo::Input::unpool (RewriteContext &ctx, HdLit const &lit) -> std::optional< std::vector< HdLit > >
	Remove all pooled arguments from the literal.

auto	CppClingo::Input::unpool (RewriteContext &ctx, BdLit const &lit) -> std::optional< std::vector< BdLit > >
	Remove all pooled arguments from the literal.

auto	CppClingo::Input::unpool (RewriteContext &ctx, Stm const &stm) -> std::optional< StmVec >
	Remove all pooled arguments from the statement.

auto	CppClingo::Input::negate (Lit const &lit) -> Lit
	Negate the given literal.

auto	CppClingo::Input::unpool_relations (Lit const &lit, bool conjunctive) -> std::optional< LitArray >
	Unpool non-binary relation literals.

auto	CppClingo::Input::unpool_relations (RewriteContext &ctx, Stm const &stm) -> std::optional< StmVec >
	Unpool all non-binary relation in the statement.

Detailed Description

Functions to rewrite expressions.

Enumeration Type Documentation

◆ Arity

enum class CppClingo::Input::Arity : uint8_t

strong

Enum for unary/binary operator arities.

Enumerator
unary	unary arity
binary	binary arity

◆ Associativity

enum class CppClingo::Input::Associativity : uint8_t

strong

Enum for operator associativities.

Enumerator
left	left associative
right	right associative
non_assoc	no associativity

◆ SimplifyLiteralFlags

enum class CppClingo::Input::SimplifyLiteralFlags : uint8_t

strong

Flags controlling simplification of literals.

Enumerator
none	No flags are set.
matchable	Ensure that literals are matchable.
unfailable	Ensure that terms in literals do not evaluate to empty pools.
head	Indicate literals occurring in rule heads.

◆ SimplifyTermFlags

enum class CppClingo::Input::SimplifyTermFlags : uint8_t

strong

Flags controlling simplification of terms.

Enumerator
none	No flags are set.
matchable	Ensure that terms are matchable.
unfailable	Ensure that terms do not evaluate to empty pools (should be used together with matchable).
nested_matchable	Do not make roots of terms matchable (should be used together with matchable).
preserve_toplevel	Preserve toplevel terms terms like u..t or @f.

Function Documentation

◆ check_safety()

auto CppClingo::Input::check_safety	(	Logger &	log,
		Stm const &	stm
	)		-> Util::ResultState< Stm >

Check whether the given statement is safe.

Literals in bodies and conditions are brought into a groundable order. The function returns the rewritten statement if this leads to changes.

◆ project() [1/2]

auto CppClingo::Input::project	(	BdLit const &	lit,
		ProjectionMap	project,
		bool	in_classical_scope
	)		-> std::optional< BdLit >

Project variables according to given projection mode and scope.

Some literal occurrences cannot be projected preserving equivalence. For example, variables in nonmonotone aggregates are only projected in classical scope.

◆ project() [2/2]

auto CppClingo::Input::project	(	RewriteOptions const &	opts,
		Stm const &	stm
	)		-> std::optional< Stm >

Project variables according to given projection mode.

Optionally, project anonymous variables in negative scope (deprecated).

◆ rewrite()

void CppClingo::Input::rewrite	(	RewriteContext &	ctx,
		Stm const &	stm,
		StmVec &	stms
	)

Rewrite the given statement.

This functions pulls together all the different rewriting steps. There are some optional rewriting steps that can be configured via options.

◆ simplify() [1/6]

auto CppClingo::Input::simplify ( IETermVec & terms ) -> Number

Simplify the given sum of terms.

Returns the sum constants and removes them from the sum.

◆ simplify() [2/6]

auto CppClingo::Input::simplify	(	RewriteContext &	ctx,
		BdLit const &	lit
	)		-> SimplifyResult< BdLit >

Simplifies the given body literal.

The result consists of a truth value and an optional literal in case of change. The literal is simplified to #true/#false for truth values true/false.

Terms that are replaced during simplification by auxiliary variables are added to the given context.

◆ simplify() [3/6]

auto CppClingo::Input::simplify	(	RewriteContext &	ctx,
		HdLit const &	lit
	)		-> SimplifyResult< HdLit >

Simplifies the given head literal.

The result consists of a truth value and an optional literal in case of change. The literal is simplified to #true/#false for truth values true/false.

Terms that are replaced during simplification by auxiliary variables are added to the given context.

◆ simplify() [4/6]

auto CppClingo::Input::simplify	(	RewriteContext &	ctx,
		Stm const &	stm
	)		-> SimplifyResult< Stm >

Simplifies the given statement.

The result consists of a truth value and an optional statement in case of change. The statement is simplified to #true/#false for truth values true/false.

◆ simplify() [5/6]

auto CppClingo::Input::simplify	(	SimplifyLiteralFlags	flags,
		RewriteContext &	ctx,
		Lit const &	lit
	)		-> SimplifyResult< Lit >

Simplifies the given literal.

The result consists of a truth value and an optional literal in case of change. The literal is simplified to #true/#false for truth values true/false.

Terms that are replaced during simplification by auxiliary variables are added to the given context.

Only the matchable and head flags apply to literals. The remaining ones are simply cleared.

◆ simplify() [6/6]

auto CppClingo::Input::simplify	(	SimplifyTermFlags	flags,
		RewriteContext &	ctx,
		Term const &	term
	)		-> SimplifyTermResult

Simplifies the given term.

The truth value of the result is false if the term failed to simplify, i.e., it evaluated to an empty pool.

Terms that are replaced during simplification by auxiliary variables are added to the given context.

◆ unify()

auto CppClingo::Input::unify	(	SymbolStore &	store,
		Term const &	a,
		Term const &	b
	)		-> bool

Try to unify the two terms.

The function also accepts terms with arithmetic terms, which except for special cases are assumed to unify with anything that is not a function or tuple. The store object is required to add auxiliary symbols during unification.

◆ visualize()

void CppClingo::Input::visualize	(	Components const &	comps,
		std::ostream &	out
	)

Output components in the dot language for visualization.

This function is intended for debugging.

Classes

Typedefs

Enumerations

Functions

Detailed Description

Enumeration Type Documentation

◆ Arity

◆ Associativity

◆ SimplifyLiteralFlags

◆ SimplifyTermFlags

Function Documentation

◆ check_safety()

◆ project() [1/2]

◆ project() [2/2]

◆ rewrite()

◆ simplify() [1/6]

◆ simplify() [2/6]

◆ simplify() [3/6]

◆ simplify() [4/6]

◆ simplify() [5/6]

◆ simplify() [6/6]

◆ unify()

◆ visualize()