lala::Simplifier< A, Allocator > Class Template Reference

#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, 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::BInc	is_top () 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
template<class Alloc2 , class Mem >
CUDA this_type &	tell (tell_type< Alloc2 > &&t, BInc< Mem > &has_changed)
template<class Alloc2 >
CUDA this_type &	tell (tell_type< Alloc2 > &&t)
template<class Alloc , class B , class Env >
CUDA void	print_variable (const LVar< Alloc > &vname, const Env &benv, const B &b) const
CUDA size_t	num_refinements () const
template<class Mem >
CUDA void	refine (size_t i, BInc< Mem > &has_changed)
CUDA size_t	num_eliminated_variables () const
CUDA size_t	num_eliminated_formulas () const
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 refines the formula by performing a number of simplifications w.r.t. an underlying abstract domain including:

1. Removing assigned variables.
2. Removing unused variables.
3. Removing entailed formulas.
4. Removing variable equality by tracking equivalence classes.

The simplified formula can be obtained by calling deinterpret(). Given a solution to the simplified formula, the extended model (with the variables deleted) can be obtained by calling representative() to obtain the representative variable of each equivalence class.

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, 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_top()

template<class A , class Allocator >

CUDA local::BInc lala::Simplifier< A, Allocator >::is_top ( ) const

inline

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

tell() [1/2]

template<class A , class Allocator >

template<class Alloc2 , class Mem >

CUDA this_type & lala::Simplifier< A, Allocator >::tell ( tell_type< Alloc2 > && t, BInc< Mem > & has_changed )

inline

tell() [2/2]

template<class A , class Allocator >

template<class Alloc2 >

CUDA this_type & lala::Simplifier< A, Allocator >::tell ( tell_type< Alloc2 > && t )

inline

print_variable()

template<class A , class Allocator >

template<class Alloc , class B , class Env >

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

inline

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

num_refinements()

template<class A , class Allocator >

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

inline

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

refine()

template<class A , class Allocator >

template<class Mem >

CUDA void lala::Simplifier< A, Allocator >::refine ( size_t i, BInc< Mem > & has_changed )

inline

num_eliminated_variables()

template<class A , class Allocator >

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

inline

num_eliminated_formulas()

template<class A , class Allocator >

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

inline

deinterpret()

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