Lattice Land Core Library
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, 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

constexpr static const bool is_abstract_universe = false
 
constexpr static const bool sequential = universe_type::sequential
 
constexpr static const bool is_totally_ordered = false
 
constexpr static const bool preserve_bot = true
 
constexpr static const bool preserve_top = true
 
constexpr static const bool preserve_join = true
 
constexpr static const bool preserve_meet = true
 
constexpr static const bool injective_concretization = true
 
constexpr static const bool preserve_concrete_covers = true
 
constexpr static 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 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 Function 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 static const bool lala::Simplifier< A, Allocator >::is_abstract_universe = false
staticconstexpr

◆ sequential

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

◆ is_totally_ordered

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

◆ preserve_bot

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

◆ preserve_top

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

◆ preserve_join

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

◆ preserve_meet

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

◆ injective_concretization

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

◆ preserve_concrete_covers

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

◆ name

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