#include <simplifier.hpp>

Classes
struct	light_copy_tag

struct	tell_type

Public Types
using	allocator_type = Allocator

using	sub_type = A

using	sub_allocator_type = typename sub_type::allocator_type

using	universe_type = typename sub_type::universe_type

using	memory_type = typename universe_type::memory_type

using	this_type = Simplifier< sub_type, allocator_type >

using	formula_sequence = battery::vector< TFormula< allocator_type >, allocator_type >

Public Member Functions
CUDA	Simplifier (AType atype, AType store_aty, abstract_ptr< sub_type > sub, const allocator_type &alloc=allocator_type())

CUDA	Simplifier (this_type &&other)

template<class A2 , class Alloc2 >
CUDA	Simplifier (const Simplifier< A2, Alloc2 > &other, light_copy_tag tag, abstract_ptr< sub_type > sub, const allocator_type &alloc=allocator_type())

CUDA allocator_type	get_allocator () const

CUDA AType	aty () const

CUDA local::B	is_bot () const

CUDA size_t	vars () const

template<bool diagnose = false, class F , class Env , class Alloc2 >
CUDA NI bool	interpret_tell (const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const

template<IKind kind, bool diagnose = false, class F , class Env , class Alloc2 >
CUDA bool	interpret (const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const

CUDA void	initialize (int num_vars, int num_cons)

template<class Seq >
CUDA void	initialize_tnf (int num_vars, const Seq &tnf)

template<class Alloc2 >
CUDA bool	deduce (tell_type< Alloc2 > &&t)

CUDA AVar	var_of (const TFormula< allocator_type > &f) const

template<class Alloc , class Abs , class Env >
CUDA void	print_variable (const LVar< Alloc > &vname, const Env &benv, const Abs &b) const

CUDA local::B	cons_deduce (int i)

CUDA size_t	num_deductions () const

CUDA local::B	deduce (size_t i)

template<class Env >
CUDA void	init_env (const Env &env)

template<class Seq >
CUDA bool	i_cse (const Seq &tnf, SimplifierStats &stats)

template<class Seq >
CUDA bool	algebraic_simplify (Seq &tnf, SimplifierStats &stats)

CUDA void	meet_equivalence_classes ()

template<class B , class Seq >
CUDA void	eliminate_entailed_constraints (const B &b, const Seq &tnf, SimplifierStats &stats)

template<class Seq >
CUDA void	eliminate_useless_variables (const Seq &tnf, size_t &num_eliminated_variables)

template<class F >
CUDA void	substitute (F &f) const

CUDA size_t	num_vars_after_elimination () const

template<class Seq >
CUDA NI TFormula< allocator_type >	deinterpret (const Seq &source, bool substitute)

CUDA NI TFormula< allocator_type >	deinterpret ()

Static Public Attributes
static constexpr const bool	is_abstract_universe = false

static constexpr const bool	sequential = universe_type::sequential

static constexpr const bool	is_totally_ordered = false

static constexpr const bool	preserve_bot = true

static constexpr const bool	preserve_top = true

static constexpr const bool	preserve_join = true

static constexpr const bool	preserve_meet = true

static constexpr const bool	injective_concretization = true

static constexpr const bool	preserve_concrete_covers = true

static constexpr const char *	name = "Simplifier"

Friends
template<class A2 , class Alloc2 >
class	Simplifier

Detailed Description

template<class A, class Allocator>
class lala::Simplifier< A, Allocator >

This abstract domain works at the level of logical formulas. It deduces the formula by performing a number of simplifications w.r.t. an underlying abstract domain including:

Removing assigned variables.
Removing unused variables.
Removing entailed formulas.
Removing variable equality by tracking equivalence classes.

The simplified formula can be obtained by calling deinterpret(). Given a solution to the simplified formula, the value of the variables deleted can be obtained by calling print_variable().

Member Typedef Documentation

◆ allocator_type

template<class A , class Allocator >

using lala::Simplifier< A, Allocator >::allocator_type = Allocator

◆ sub_type

template<class A , class Allocator >

using lala::Simplifier< A, Allocator >::sub_type = A

◆ sub_allocator_type

template<class A , class Allocator >

using lala::Simplifier< A, Allocator >::sub_allocator_type = typename sub_type::allocator_type

◆ universe_type

template<class A , class Allocator >

using lala::Simplifier< A, Allocator >::universe_type = typename sub_type::universe_type

◆ memory_type

template<class A , class Allocator >

using lala::Simplifier< A, Allocator >::memory_type = typename universe_type::memory_type

◆ this_type

template<class A , class Allocator >

using lala::Simplifier< A, Allocator >::this_type = Simplifier<sub_type, allocator_type>

◆ formula_sequence

template<class A , class Allocator >

using lala::Simplifier< A, Allocator >::formula_sequence = battery::vector<TFormula<allocator_type>, allocator_type>

Constructor & Destructor Documentation

◆ Simplifier() [1/3]

template<class A , class Allocator >

CUDA lala::Simplifier< A, Allocator >::Simplifier	(	AType	atype,
		AType	store_aty,
		abstract_ptr< sub_type >	sub,
		const allocator_type &	alloc = `allocator_type()`
	)

inline

◆ Simplifier() [2/3]

template<class A , class Allocator >

CUDA lala::Simplifier< A, Allocator >::Simplifier ( this_type && other )

inline

◆ Simplifier() [3/3]

template<class A , class Allocator >

template<class A2 , class Alloc2 >

CUDA lala::Simplifier< A, Allocator >::Simplifier	(	const Simplifier< A2, Alloc2 > &	other,
		light_copy_tag	tag,
		abstract_ptr< sub_type >	sub,
		const allocator_type &	alloc = `allocator_type()`
	)

inline

Member Function Documentation

◆ get_allocator()

template<class A , class Allocator >

CUDA allocator_type lala::Simplifier< A, Allocator >::get_allocator ( ) const

inline

◆ aty()

template<class A , class Allocator >

CUDA AType lala::Simplifier< A, Allocator >::aty ( ) const

inline

◆ is_bot()

template<class A , class Allocator >

CUDA local::B lala::Simplifier< A, Allocator >::is_bot ( ) const

inline

@parallel @order-preserving @increasing

◆ vars()

template<class A , class Allocator >

CUDA size_t lala::Simplifier< A, Allocator >::vars ( ) const

inline

Returns the number of variables currently represented by this abstract element.

◆ interpret_tell()

template<class A , class Allocator >

template<bool diagnose = false, class F , class Env , class Alloc2 >

CUDA NI bool lala::Simplifier< A, Allocator >::interpret_tell	(	const F &	f,
		Env &	env,
		tell_type< Alloc2 > &	tell,
		IDiagnostics &	diagnostics
	)		const

inline

◆ interpret()

template<class A , class Allocator >

template<IKind kind, bool diagnose = false, class F , class Env , class Alloc2 >

CUDA bool lala::Simplifier< A, Allocator >::interpret	(	const F &	f,
		Env &	env,
		tell_type< Alloc2 > &	tell,
		IDiagnostics &	diagnostics
	)		const

inline

◆ initialize()

template<class A , class Allocator >

CUDA void lala::Simplifier< A, Allocator >::initialize	(	int	num_vars,
		int	num_cons
	)

inline

◆ initialize_tnf()

template<class A , class Allocator >

template<class Seq >

CUDA void lala::Simplifier< A, Allocator >::initialize_tnf	(	int	num_vars,
		const Seq &	tnf
	)

inline

We initialize the equivalence classes and var/cons elimination masks. Further, we eliminate all constraints in tnf that are not in TNF. (It is the existential quantifiers and unary constraints that are re-generated from the underlying store later.)

◆ deduce() [1/2]

template<class A , class Allocator >

template<class Alloc2 >

CUDA bool lala::Simplifier< A, Allocator >::deduce ( tell_type< Alloc2 > && t )

inline

@sequential

◆ var_of()

template<class A , class Allocator >

CUDA AVar lala::Simplifier< A, Allocator >::var_of ( const TFormula< allocator_type > & f ) const

inline

◆ print_variable()

template<class A , class Allocator >

template<class Alloc , class Abs , class Env >

CUDA void lala::Simplifier< A, Allocator >::print_variable	(	const LVar< Alloc > &	vname,
		const Env &	benv,
		const Abs &	b
	)		const

inline

Print the abstract universe of vname taking into account simplifications (representative variable and constant).

◆ cons_deduce()

template<class A , class Allocator >

CUDA local::B lala::Simplifier< A, Allocator >::cons_deduce ( int i )

inline

◆ num_deductions()

template<class A , class Allocator >

CUDA size_t lala::Simplifier< A, Allocator >::num_deductions ( ) const

inline

We have one deduction operator per variable and one per constraint in the interpreted formula.

◆ deduce() [2/2]

template<class A , class Allocator >

CUDA local::B lala::Simplifier< A, Allocator >::deduce ( size_t i )

inline

◆ init_env()

template<class A , class Allocator >

template<class Env >

CUDA void lala::Simplifier< A, Allocator >::init_env ( const Env & env )

inline

◆ i_cse()

template<class A , class Allocator >

template<class Seq >

CUDA bool lala::Simplifier< A, Allocator >::i_cse	(	const Seq &	tnf,
		SimplifierStats &	stats
	)

inline

I-CSE algorithm. For each pair of TNF constraints x <=> y op z and ‘x’ <=> y' op' z', whenever[y'] = [y],op = op'and[z] = [z'], we add the equivalencex = x'and eliminate the second constraint. Note that [x] represents the equivalence class ofx. To avoid an algorithm running in O(n^2), we use a hash map to detect syntactical equivalence betweeny op zandy' op z'`. Further, for commutative operators, we redefine the equality function.

This algorithm is applied until a fixpoint is reached.

Returns: The number of formulas eliminated.

◆ algebraic_simplify()

template<class A , class Allocator >

template<class Seq >

CUDA bool lala::Simplifier< A, Allocator >::algebraic_simplify	(	Seq &	tnf,
		SimplifierStats &	stats
	)

inline

Perform algebraic simplification on the TNF. The non-eliminated constraints are assumed to be in TNF.

◆ meet_equivalence_classes()

template<class A , class Allocator >

CUDA void lala::Simplifier< A, Allocator >::meet_equivalence_classes ( )

inline

◆ eliminate_entailed_constraints()

template<class A , class Allocator >

template<class B , class Seq >

CUDA void lala::Simplifier< A, Allocator >::eliminate_entailed_constraints	(	const B &	b,
		const Seq &	tnf,
		SimplifierStats &	stats
	)

inline

◆ eliminate_useless_variables()

template<class A , class Allocator >

template<class Seq >

CUDA void lala::Simplifier< A, Allocator >::eliminate_useless_variables	(	const Seq &	tnf,
		size_t &	num_eliminated_variables
	)

inline

◆ substitute()

template<class A , class Allocator >

template<class F >

CUDA void lala::Simplifier< A, Allocator >::substitute ( F & f ) const

inline

Given any formula (not necessarily in TNF), we substitute each variable with its representative variable or a constant if it got eliminated.

◆ num_vars_after_elimination()

template<class A , class Allocator >

CUDA size_t lala::Simplifier< A, Allocator >::num_vars_after_elimination ( ) const

inline

◆ deinterpret() [1/2]

template<class A , class Allocator >

template<class Seq >

CUDA NI TFormula< allocator_type > lala::Simplifier< A, Allocator >::deinterpret	(	const Seq &	source,
		bool	substitute
	)

inline

◆ deinterpret() [2/2]

template<class A , class Allocator >

CUDA NI TFormula< allocator_type > lala::Simplifier< A, Allocator >::deinterpret ( )

inline

Friends And Related Symbol Documentation

◆ Simplifier

template<class A , class Allocator >

template<class A2 , class Alloc2 >

friend class Simplifier

friend

Member Data Documentation

◆ is_abstract_universe

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::is_abstract_universe = false

staticconstexpr

◆ sequential

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::sequential = universe_type::sequential

staticconstexpr

◆ is_totally_ordered

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::is_totally_ordered = false

staticconstexpr

◆ preserve_bot

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::preserve_bot = true

staticconstexpr

◆ preserve_top

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::preserve_top = true

staticconstexpr

◆ preserve_join

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::preserve_join = true

staticconstexpr

◆ preserve_meet

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::preserve_meet = true

staticconstexpr

◆ injective_concretization

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::injective_concretization = true

staticconstexpr

◆ preserve_concrete_covers

template<class A , class Allocator >

constexpr const bool lala::Simplifier< A, Allocator >::preserve_concrete_covers = true

staticconstexpr

◆ name

template<class A , class Allocator >

constexpr const char* lala::Simplifier< A, Allocator >::name = "Simplifier"

staticconstexpr

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

include/lala/simplifier.hpp

Classes

Public Types

Public Member Functions

Static Public Attributes

Friends

Detailed Description

Member Typedef Documentation

◆ allocator_type

◆ sub_type

◆ sub_allocator_type

◆ universe_type

◆ memory_type

◆ this_type

◆ formula_sequence

Constructor & Destructor Documentation

◆ Simplifier() [1/3]

◆ Simplifier() [2/3]

◆ Simplifier() [3/3]

Member Function Documentation

◆ get_allocator()

◆ aty()

◆ is_bot()

◆ vars()

◆ interpret_tell()

◆ interpret()

◆ initialize()

◆ initialize_tnf()

◆ deduce() [1/2]

◆ var_of()

◆ print_variable()

◆ cons_deduce()

◆ num_deductions()

◆ deduce() [2/2]

◆ init_env()

◆ i_cse()

◆ algebraic_simplify()

◆ meet_equivalence_classes()

◆ eliminate_entailed_constraints()

◆ eliminate_useless_variables()

◆ substitute()

◆ num_vars_after_elimination()

◆ deinterpret() [1/2]

◆ deinterpret() [2/2]

Friends And Related Symbol Documentation

◆ Simplifier

Member Data Documentation

◆ is_abstract_universe

◆ sequential

◆ is_totally_ordered

◆ preserve_bot

◆ preserve_top

◆ preserve_join

◆ preserve_meet

◆ injective_concretization

◆ preserve_concrete_covers

◆ name