Gringo::Term Struct Reference

#include <term.hh>

Inheritance diagram for Gringo::Term:

Collaboration diagram for Gringo::Term:

Classes
struct	SimplifyRet

Public Types
enum	Invertibility { CONSTANT = 0, INVERTIBLE = 1, NOT_INVERTIBLE = 2 }
using	ProjectRet = std::tuple< UTerm, UTerm, UTerm >
	Return value of Term::project (replace, projected, project). More...
using	SVal = std::shared_ptr< Value >
using	VarSet = std::unordered_set< FWString >
using	RenameMap = std::unordered_map< FWString, std::pair< FWString, SVal >>
using	ReferenceMap = std::unordered_map< Term *, SGRef, value_hash< Term * >, value_equal_to< Term * >>
using	DotsMap = std::vector< std::tuple< UTerm, UTerm, UTerm >>
	Type that stores for each rewritten DotsTerm the associated variable and the lower and upper bound. More...
using	ScriptMap = std::vector< std::tuple< UTerm, FWString, UTermVec >>
using	ArithmeticsMap = std::vector< std::unordered_map< UTerm, UTerm, value_hash< UTerm >, value_equal_to< UTerm >>>

Public Member Functions
virtual bool	hasVar () const =0
	Whether the term contains a VarTerm. More...
virtual void	rename (FWString name)=0
virtual void	unpool (UTermVec &x) const =0
virtual SimplifyRet	simplify (DotsMap &dots, ScriptMap &scripts, unsigned &auxNum, bool positional, bool arithmetic)=0
virtual ProjectRet	project (bool rename, unsigned &auxNum)=0
virtual bool	isNotNumeric () const =0
virtual Invertibility	getInvertibility () const =0
virtual Value	eval () const =0
bool	isZero () const
virtual void	collect (VarTermBoundVec &vars, bool bound) const =0
virtual void	collect (VarTermSet &vars) const
virtual void	collect (VarSet &vars, unsigned minLevel=0, unsigned maxLevel=std::numeric_limits< unsigned >::max()) const =0
virtual void	collectIds (VarSet &vars) const =0
virtual unsigned	getLevel () const =0
virtual UTerm	rewriteArithmetics (ArithmeticsMap &arith, unsigned &auxNum)=0
virtual bool	match (Value const &val) const =0
bool	bind (VarSet &bound)
virtual FWSignature	getSig () const =0
virtual UTerm	renameVars (RenameMap &names) const =0
SGRef	_newRef (RenameMap &names, ReferenceMap &refs) const
UGTerm	gterm () const
virtual bool	hasPool () const =0
virtual UGTerm	gterm (RenameMap &names, ReferenceMap &refs) const =0
virtual UTerm	replace (Defines &defs, bool replace)=0
virtual double	estimate (double size, VarSet const &bound) const =0
virtual Value	isEDB () const =0
virtual	~Term ()
template<class T , class U , class V >
void	replace (std::unique_ptr< T > &dst, std::unique_ptr< U > &&src, std::unique_ptr< V > &&alt)
template<class It , class TermUnpool , class Callback >
void	unpool (It const &begin, It const &end, TermUnpool const &f, Callback const &g)
template<class Vec , class TermUnpool >
void	unpoolJoin (Vec &vec, TermUnpool const &f)
Public Member Functions inherited from Gringo::Printable
virtual void	print (std::ostream &out) const =0
virtual	~Printable ()
Public Member Functions inherited from Gringo::Hashable
virtual size_t	hash () const =0
virtual	~Hashable ()
Public Member Functions inherited from Gringo::Locatable
virtual Location const &	loc () const =0
virtual void	loc (Location const &loc)=0
virtual	~Locatable ()
Public Member Functions inherited from Gringo::Comparable< Term >
virtual bool	operator== (Termconst &other) const =0
virtual bool	operator!= (Termconst &other) const
virtual	~Comparable ()
Public Member Functions inherited from Gringo::Clonable< Term >
virtual Term *	clone () const =0
virtual	~Clonable ()

Static Public Member Functions
static FWString	uniqueName (unsigned &auxNum, char const *prefix="#X")
	Creates a unique variable name. More...
static UTerm	uniqueVar (Location const &loc, unsigned &auxNum, unsigned level=0, const char *prefix="#X")
	Creates a unique variable using #aux(auxNum) as name. More...
static UTerm	uniqueVal (Location const &loc, unsigned &auxNum, const char *prefix="#X")
static UTerm	insert (ArithmeticsMap &arith, unsigned &auxNum, UTerm &&term)
	Inserts a term into arith creating a new unique variable if necessary. More...
template<class T , class U >
static void	replace (std::unique_ptr< T > &dst, std::unique_ptr< U > &&src)
	Set dst to src if src is non-zero. More...
template<class A , class UnpoolA , class Callback >
static void	unpool (A const &a, UnpoolA const &fA, Callback const &g)
	Unpools a, calling g on each obtained element. More...
template<class A , class B , class UnpoolA , class UnpoolB , class Callback >
static void	unpool (A const &a, B const &b, UnpoolA const &fA, UnpoolB const &fB, Callback const &g)
	Unpools a and b, calculates cross product, calling g on each obtained tuple. More...
template<class It , class Unpool , class Callback >
static void	unpool (It const &begin, It const &end, Unpool const &f, Callback const &g)
	Iterates of [begin, end] unpooling with f, calculates cross product, calling g on each obtained tuple. More...
template<class Vec , class Unpool >
static void	unpoolJoin (Vec &vec, Unpool const &f)
	Unpools each element of vec using f, and move the union of all pools back to f. More...

Member Typedef Documentation

using Gringo::Term::ArithmeticsMap = std::vector<std::unordered_map<UTerm, UTerm, value_hash<UTerm>, value_equal_to<UTerm>>>

Type that stores for each rewritten arithmetic term (UnopTerm, BinopTerm, LuaTerm) the associated variable and the term itself. The indices of the vector correspond to the level of the term.

using Gringo::Term::DotsMap = std::vector<std::tuple<UTerm, UTerm, UTerm>>

Type that stores for each rewritten DotsTerm the associated variable and the lower and upper bound.

using Gringo::Term::ProjectRet = std::tuple<UTerm, UTerm, UTerm>

Return value of Term::project (replace, projected, project).

using Gringo::Term::ReferenceMap = std::unordered_map<Term*, SGRef, value_hash<Term*>, value_equal_to<Term*>>

using Gringo::Term::RenameMap = std::unordered_map<FWString, std::pair<FWString, SVal>>

using Gringo::Term::ScriptMap = std::vector<std::tuple<UTerm, FWString, UTermVec>>

using Gringo::Term::SVal = std::shared_ptr<Value>

using Gringo::Term::VarSet = std::unordered_set<FWString>

Member Enumeration Documentation

enum Gringo::Term::Invertibility

The invertibility of a term. This may either be

• CONSTANT for terms that do not contain variables,
• INVERTIBLE for invertible terms (e.g. -X, 1+X, f(X,Y+Z))
• NOT_INVERTIBLE for terms that are not invertible (e.g. arithmetic operations with two unknowns)

Enumerator
CONSTANT
INVERTIBLE
NOT_INVERTIBLE

Constructor & Destructor Documentation

virtual Gringo::Term::~Term ( )

inlinevirtual

Member Function Documentation

SGRef Gringo::Term::_newRef	(	RenameMap &	names,
		Term::ReferenceMap &	refs
	)		const

Here is the call graph for this function:

bool Gringo::Term::bind

(

VarSet &

bound

)

Here is the call graph for this function:

virtual void Gringo::Term::collect ( VarTermBoundVec &  vars, bool  bound  ) const

pure virtual

Collects variables in Terms.

Precondition

Must be called after simplify and project to properly account for bound variables.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

void Gringo::Term::collect ( VarTermSet &  vars ) const

virtual

Here is the call graph for this function:

virtual void Gringo::Term::collect ( VarSet &  vars, unsigned  minLevel = 0, unsigned  maxLevel = std::numeric_limits< unsigned >::max()  ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual void Gringo::Term::collectIds ( VarSet &  vars ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual double Gringo::Term::estimate ( double  size, VarSet const &  bound  ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual Value Gringo::Term::eval ( ) const

pure virtual

Evaluates the term to a value.

Precondition

Must be called after simplify.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual Invertibility Gringo::Term::getInvertibility ( ) const

pure virtual

Obtain the invertibility of a term.

Precondition

Must be called after simplify.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual unsigned Gringo::Term::getLevel ( ) const

pure virtual

Returns the nesting level of a term. That is the largest level of a nested variable or zero for ground terms.

Precondition

Must be called after assignLevel.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual FWSignature Gringo::Term::getSig ( ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

UGTerm Gringo::Term::gterm

(

)

const

virtual UGTerm Gringo::Term::gterm ( RenameMap &  names, ReferenceMap &  refs  ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual bool Gringo::Term::hasPool ( ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual bool Gringo::Term::hasVar ( ) const

pure virtual

Whether the term contains a VarTerm.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

UTerm Gringo::Term::insert ( ArithmeticsMap &  arith, unsigned &  auxNum, UTerm &&  term  )

static

Inserts a term into arith creating a new unique variable if necessary.

Here is the call graph for this function:

virtual Value Gringo::Term::isEDB ( ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual bool Gringo::Term::isNotNumeric ( ) const

pure virtual

Obtain the type of a term.

Precondition

Must be called after simplify. Whether evaluation of a term is guaranteed to not produce numeric values. Basically, this means that the term is either a non-numeric constant or a function symbol.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

bool Gringo::Term::isZero

(

)

const

Returns true if the term evaluates to zero.

Precondition

Must be called after simplify.

Term is ground or

Here is the call graph for this function:

virtual bool Gringo::Term::match ( Value const &  val ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual ProjectRet Gringo::Term::project ( bool  rename, unsigned &  auxNum  )

pure virtual

Removes anonymous variables in projectable positions (in outermost function symbols) from a term. The first element of the return value is a replacement term for the current term, which might be null if the term does not have to be replace.. The second and third can be used to create a projection rule where the second is the head and the third is the body element.

Precondition

Must be called after simplify.

num = 0; sig = base; lit = q(X,_)
(lit', projected, project) = lit.project(&sig, num)
assert(lit'      == #p_q(base,X,#p))
assert(projected == #p_q(base,#X1,#p))
assert(project   == #p_q(base,#X1,#Y2))

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual void Gringo::Term::rename ( FWString  name )

pure virtual

Rename the outermost term.

Precondition

the term must either be a function term or value term holding an identifier.

Note

unnecessary; can be deleted

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual UTerm Gringo::Term::renameVars ( RenameMap &  names ) const

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual UTerm Gringo::Term::replace ( Defines &  defs, bool  replace  )

pure virtual

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

template<class T , class U >

void Gringo::Term::replace ( std::unique_ptr< T > &  dst, std::unique_ptr< U > &&  src  )

static

Set dst to src if src is non-zero.

template<class T , class U , class V >

void Gringo::Term::replace	(	std::unique_ptr< T > &	dst,
		std::unique_ptr< U > &&	src,
		std::unique_ptr< V > &&	alt
	)

virtual UTerm Gringo::Term::rewriteArithmetics ( ArithmeticsMap &  arith, unsigned &  auxNum  )

pure virtual

Removes non-invertible arithmetics.

Note

The term is unusable if the method returned a non-zero replacement term.

Precondition

Must be called after assignLevel.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

virtual SimplifyRet Gringo::Term::simplify ( DotsMap &  dots, ScriptMap &  scripts, unsigned &  auxNum, bool  positional, bool  arithmetic  )

pure virtual

Removes all occurrences of DotsTerm instances, simplifies the term and sets the invertibility. To reduce the number of cases in later algorithms moves invertible terms to the left:

• 1+X -> X+1
• (1+(1-X)) -> ((-X)+1)+1 Replaces undefined arithmetic operations with 0:
• f(X)+0 -> 0

  Note

  The term is unusable if the method returned a non-zero replacement term.

  Precondition

  Must be called after unpool.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

FWString Gringo::Term::uniqueName ( unsigned &  auxNum, char const *  prefix = "#X"  )

static

Creates a unique variable name.

Here is the call graph for this function:

UTerm Gringo::Term::uniqueVal ( Location const &  loc, unsigned &  auxNum, const char *  prefix = "#X"  )

static

Here is the call graph for this function:

UTerm Gringo::Term::uniqueVar ( Location const &  loc, unsigned &  auxNum, unsigned  level = 0, const char *  prefix = "#X"  )

static

Creates a unique variable using #aux(auxNum) as name.

Here is the call graph for this function:

virtual void Gringo::Term::unpool ( UTermVec &  x ) const

pure virtual

Removes all occurrences of PoolTerm instances. Returns all unpooled incarnations of the term.

Note

The term becomes unusable after the method returns.

Postcondition

The pool does not contain PoolTerm instances.

Implemented in Gringo::LinearTerm, Gringo::FunctionTerm, Gringo::LuaTerm, Gringo::DotsTerm, Gringo::BinOpTerm, Gringo::UnOpTerm, Gringo::VarTerm, Gringo::ValTerm, and Gringo::PoolTerm.

template<class A , class UnpoolA , class Callback >

void Gringo::Term::unpool ( A const &  a, UnpoolA const &  fA, Callback const &  g  )

static

Unpools a, calling g on each obtained element.

template<class A , class B , class UnpoolA , class UnpoolB , class Callback >

void Gringo::Term::unpool ( A const &  a, B const &  b, UnpoolA const &  fA, UnpoolB const &  fB, Callback const &  g  )

static

Unpools a and b, calculates cross product, calling g on each obtained tuple.

Here is the call graph for this function:

template<class It , class Unpool , class Callback >

static void Gringo::Term::unpool ( It const &  begin, It const &  end, Unpool const &  f, Callback const &  g  )

static

Iterates of [begin, end] unpooling with f, calculates cross product, calling g on each obtained tuple.

template<class It , class TermUnpool , class Callback >

void Gringo::Term::unpool	(	It const &	begin,
		It const &	end,
		TermUnpool const &	f,
		Callback const &	g
	)

Here is the call graph for this function:

template<class Vec , class Unpool >

static void Gringo::Term::unpoolJoin ( Vec &  vec, Unpool const &  f  )

static

Unpools each element of vec using f, and move the union of all pools back to f.

template<class Vec , class TermUnpool >

void Gringo::Term::unpoolJoin	(	Vec &	vec,
		TermUnpool const &	f
	)

Here is the call graph for this function:

---

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

• /Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libgringo/gringo/term.hh
• /Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libgringo/src/term.cc