Lattice Land Core Library
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Static Public Attributes | Friends | List of all members
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::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
 
template<class Alloc2 >
CUDA bool deduce (tell_type< Alloc2 > &&t)
 
template<class Alloc , class Abs , class Env >
CUDA void print_variable (const LVar< Alloc > &vname, const Env &benv, const Abs &b) const
 
CUDA size_t num_deductions () const
 
CUDA local::B deduce (size_t i)
 
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 deduces 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_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

◆ deduce() [1/2]

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

@sequential

◆ 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).

◆ 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

◆ 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 >
const bool lala::Simplifier< A, Allocator >::is_abstract_universe = false
staticconstexpr

◆ sequential

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::sequential = universe_type::sequential
staticconstexpr

◆ is_totally_ordered

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::is_totally_ordered = false
staticconstexpr

◆ preserve_bot

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::preserve_bot = true
staticconstexpr

◆ preserve_top

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::preserve_top = true
staticconstexpr

◆ preserve_join

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::preserve_join = true
staticconstexpr

◆ preserve_meet

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::preserve_meet = true
staticconstexpr

◆ injective_concretization

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::injective_concretization = true
staticconstexpr

◆ preserve_concrete_covers

template<class A , class Allocator >
const bool lala::Simplifier< A, Allocator >::preserve_concrete_covers = true
staticconstexpr

◆ name

template<class A , class Allocator >
const char* lala::Simplifier< A, Allocator >::name = "Simplifier"
staticconstexpr
The documentation for this class was generated from the following file: