Analyze

Functions to analyze expressions. More...

Classes
struct	CppClingo::Input::CheckTypeResult
	Extract additional information while checking the type of a term. More...
class	CppClingo::Input::LinearTerm
	Helper to access elements of linear terms. More...

Enumerations
enum class	CppClingo::Input::TermCheckType : uint8_t {   TermCheckType::atom , TermCheckType::sig , TermCheckType::identifier , TermCheckType::signed_identifier ,   TermCheckType::pos_number }
	Enumeration for Term::check_type(). More...

Functions
auto	CppClingo::Input::check_type (Term const &term, TermCheckType type, CheckTypeResult *res=nullptr) -> bool
	Query information about the structure of the given term.
auto	CppClingo::Input::is_linear (Term const &term) -> bool
	Check if the given term is a linear term.
auto	CppClingo::Input::is_linear (TermBinary const &term) -> bool
	See is_linear().
auto	CppClingo::Input::check_linear (TermBinary const &term) -> std::optional< LinearTerm >
	Check if the given term is a linear term and return an object to access its elements.
auto	CppClingo::Input::check_linear (Term const &term) -> std::optional< LinearTerm >
	See check_linear().
auto	CppClingo::Input::is_interval (Term const &term) -> bool
	Returns true if the term has form t..u.
auto	CppClingo::Input::is_external (Term const &term) -> bool
	Returns true if the term has form @f(...).
auto	CppClingo::Input::is_interval (TermBinary const &term) -> bool
	See is_interval().
auto	CppClingo::Input::always_numeric (Term const &term) -> bool
	Check if the term always evaluates to a number.
auto	CppClingo::Input::never_numeric (Term const &term) -> bool
	Check if the term never evaluates to a number.
auto	CppClingo::Input::is_symbol (Term const &term) -> bool
	Check if the term is a symbol.
auto	CppClingo::Input::is_variable (Term const &term) -> bool
	Check if the term is a variable.
auto	CppClingo::Input::is_fixed (Lit const &lit) -> std::optional< bool >
	Get the truth value of a literal, in case it is a Boolean constant.
auto	CppClingo::Input::is_atom (Term const &term) -> bool
	Check whether the term can represent an atom.
auto	CppClingo::Input::is_atom (Lit const &lit) -> bool
	Check whether the literal is an atom.
auto	CppClingo::Input::is_atom (HdLit const &lit) -> bool
	Check if the literal is a symbolic atom.
auto	CppClingo::Input::is_atom (BdLit const &lit) -> bool
	Check if the literal is a symbolic atom.
auto	CppClingo::Input::is_boolean (Lit const &lit) -> std::optional< bool >
	Check if a literal is a boolean constant.
auto	CppClingo::Input::is_test (BdLit const &lit) -> bool
	Check if the literal is a test.
auto	CppClingo::Input::is_classical (HdLit const &lit) -> bool
	Check if the literal is classical.
auto	CppClingo::Input::is_fact (SymbolStore &store, StmRule const &rule) -> std::optional< Symbol >
	Check if a rule is a fact.
auto	CppClingo::Input::is_fact (SymbolStore &store, Stm const &stm) -> std::optional< Symbol >
	Check if a statement is a fact.
auto	CppClingo::Input::check_global (Logger &log, VariableSet const &global, Stm const &stm) -> bool
	Check that none of the given variables are local in the statement.
auto	CppClingo::Input::is_theory_operator (std::string_view name) -> bool
	Check if the given string is a theory operator.
auto	CppClingo::Input::signature (Term const &term) -> std::optional< std::tuple< String, size_t, bool > >
	Get the signature of a term.
auto	CppClingo::Input::is_matchable (Term const &term) -> bool
	Check if a term is matchable.
void	CppClingo::Input::extract_can_fail (Term const &term, std::vector< Term > &result)
	Extract terms whose evaluation can fail.

Detailed Description

Functions to analyze expressions.

Enumeration Type Documentation

TermCheckType

enum class CppClingo::Input::TermCheckType : uint8_t

strong

Enumeration for Term::check_type().

Enumerator
atom	Check if term is an atom.
sig	Check if term is a signature.
identifier	Check if term is an identifier.
signed_identifier	Check if term is a signed identifier.
pos_number	Check if term is a positive number.

Function Documentation

always_numeric()

auto CppClingo::Input::always_numeric

(

Term const &

term

)

-> bool

Check if the term always evaluates to a number.

For example, X+Y but not X because it can also evaluate to other symbols.

is_atom() [1/3]

auto CppClingo::Input::is_atom

(

BdLit const &

lit

)

-> bool

Check if the literal is a symbolic atom.

This extends the test to conjunctions with exactly one element corresponding to an atom.

is_atom() [2/3]

auto CppClingo::Input::is_atom

(

HdLit const &

lit

)

-> bool

Check if the literal is a symbolic atom.

This extends the test to disjunctions with exactly one element corresponding to an atom.

is_atom() [3/3]

auto CppClingo::Input::is_atom

(

Lit const &

lit

)

-> bool

Check whether the literal is an atom.

A literal is an atom if it is a symbolic literal without a sign.

is_classical()

auto CppClingo::Input::is_classical

(

HdLit const &

lit

)

-> bool

Check if the literal is classical.

This function is used to enable additional projection in rule bodies whenever it can be statically determined that the head does not derive anything.

Note that this function could also be extended to aggregates that do not derive atoms.

is_fact() [1/2]

auto CppClingo::Input::is_fact	(	SymbolStore &	store,
		Stm const &	stm
	)		-> std::optional< Symbol >

Check if a statement is a fact.

Returns the symbol representing the fact. This function evaluates arithmetic expressions as long as they evaluate to one-elementary pools.

is_fact() [2/2]

auto CppClingo::Input::is_fact	(	SymbolStore &	store,
		StmRule const &	rule
	)		-> std::optional< Symbol >

Check if a rule is a fact.

Returns the symbol representing the fact. This function evaluates arithmetic expressions as long as they evaluate to one-elementary pools.

is_matchable()

auto CppClingo::Input::is_matchable

(

Term const &

term

)

-> bool

Check if a term is matchable.

Matchable terms only contain (non-external) functions, tuples, constants, variables, linear terms, and negated terms.

For example, the following terms is matchable: f(1,c,X,X+1,-X,(X,Y)).

is_test()

auto CppClingo::Input::is_test

(

BdLit const &

lit

)

-> bool

Check if the literal is a test.

This is used to prevent projection in projection-like rules. For example, variable Y in p(X) :- p(X,Y), X>10 is not projected because X>10 is classified as a test.

never_numeric()

auto CppClingo::Input::never_numeric

(

Term const &

term

)

-> bool

Check if the term never evaluates to a number.

This is true for tuples, functions, #sup, and #inf.