Lattice Land Powerdomains Library
Loading...
Searching...
No Matches
lala::BAB< A, B > Class Template Reference

#include <bab.hpp>

Classes

struct  tell_type
 

Public Types

using allocator_type = typename A::allocator_type
 
using sub_type = A
 
using sub_ptr = abstract_ptr<sub_type>
 
using best_type = B
 
using best_ptr = abstract_ptr<best_type>
 
using this_type = BAB<sub_type, best_type>
 
template<class Alloc2 >
using ask_type = typename sub_type::template ask_type<Alloc2>
 

Public Member Functions

CUDA BAB (AType atype, sub_ptr sub, best_ptr best)
 
template<class A2 , class B2 , class... Allocators>
CUDA NI BAB (const BAB< A2, B2 > &other, AbstractDeps< Allocators... > &deps)
 
CUDA AType aty () const
 
CUDA allocator_type get_allocator () const
 
CUDA local::B is_bot () const
 
CUDA local::B is_top () 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<bool diagnose = false, class F , class Env , class Alloc2 >
CUDA NI bool interpret_ask (const F &f, const Env &env, ask_type< Alloc2 > &ask, IDiagnostics &diagnostics) const
 
template<IKind kind, bool diagnose = false, class F , class Env , class I >
CUDA NI bool interpret (const F &f, Env &env, I &intermediate, IDiagnostics &diagnostics) const
 
template<class Alloc >
CUDA bool deduce (const tell_type< Alloc > &t)
 
template<class Alloc2 >
CUDA NI TFormula< Alloc2 > deinterpret_best_bound (const typename best_type::universe_type &best_bound, const Alloc2 &alloc=Alloc2{}) const
 
template<class Alloc2 >
CUDA TFormula< Alloc2 > deinterpret_best_bound (const Alloc2 &alloc=Alloc2{}) const
 
CUDA local::B deduce (const typename best_type::universe_type &best_bound)
 
template<class Store1 , class Store2 >
CUDA bool compare_bound (const Store1 &store1, const Store2 &store2) const
 
CUDA local::B deduce ()
 
CUDA int solutions_count () const
 
template<class ExtractionStrategy = NonAtomicExtraction>
CUDA bool is_extractable (const ExtractionStrategy &strategy=ExtractionStrategy()) const
 
template<class AbstractBest >
CUDA void extract (AbstractBest &ua) const
 
CUDA const best_typeoptimum () const
 
CUDA best_ptr optimum_ptr () const
 
CUDA bool is_satisfaction () const
 
CUDA bool is_optimization () const
 
CUDA bool is_minimization () const
 
CUDA bool is_maximization () const
 
CUDA AVar objective_var () const
 

Static Public Attributes

static constexpr const bool is_abstract_universe = false
 
static constexpr const bool sequential = sub_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 = sub_type::preserve_join
 
static constexpr const bool preserve_meet = sub_type::preserve_meet
 
static constexpr const bool injective_concretization = sub_type::injective_concretization
 
static constexpr const bool preserve_concrete_covers = sub_type::preserve_concrete_covers
 
static constexpr const char * name = "BAB"
 

Friends

template<class A2 , class B2 >
class BAB
 

Member Typedef Documentation

◆ allocator_type

template<class A , class B = A>
using lala::BAB< A, B >::allocator_type = typename A::allocator_type

◆ sub_type

template<class A , class B = A>
using lala::BAB< A, B >::sub_type = A

◆ sub_ptr

template<class A , class B = A>
using lala::BAB< A, B >::sub_ptr = abstract_ptr<sub_type>

◆ best_type

template<class A , class B = A>
using lala::BAB< A, B >::best_type = B

◆ best_ptr

template<class A , class B = A>
using lala::BAB< A, B >::best_ptr = abstract_ptr<best_type>

◆ this_type

template<class A , class B = A>
using lala::BAB< A, B >::this_type = BAB<sub_type, best_type>

◆ ask_type

template<class A , class B = A>
template<class Alloc2 >
using lala::BAB< A, B >::ask_type = typename sub_type::template ask_type<Alloc2>

Constructor & Destructor Documentation

◆ BAB() [1/2]

template<class A , class B = A>
CUDA lala::BAB< A, B >::BAB ( AType atype,
sub_ptr sub,
best_ptr best )
inline

◆ BAB() [2/2]

template<class A , class B = A>
template<class A2 , class B2 , class... Allocators>
CUDA NI lala::BAB< A, B >::BAB ( const BAB< A2, B2 > & other,
AbstractDeps< Allocators... > & deps )
inline

Construct BAB by copying other. The best solution is copied using a fresh AbstractDeps, and thus is not intended to be shared with other abstract domains. For instance, if best is a VStore, it shares the same AType than the VStore underlying sub. Hence, if we copy it using deps, both VStore will be shared which is not the intended behavior.

Member Function Documentation

◆ aty()

template<class A , class B = A>
CUDA AType lala::BAB< A, B >::aty ( ) const
inline

◆ get_allocator()

template<class A , class B = A>
CUDA allocator_type lala::BAB< A, B >::get_allocator ( ) const
inline

◆ is_bot()

template<class A , class B = A>
CUDA local::B lala::BAB< A, B >::is_bot ( ) const
inline

◆ is_top()

template<class A , class B = A>
CUDA local::B lala::BAB< A, B >::is_top ( ) const
inline

◆ interpret_tell()

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

◆ interpret_ask()

template<class A , class B = A>
template<bool diagnose = false, class F , class Env , class Alloc2 >
CUDA NI bool lala::BAB< A, B >::interpret_ask ( const F & f,
const Env & env,
ask_type< Alloc2 > & ask,
IDiagnostics & diagnostics ) const
inline

◆ interpret()

template<class A , class B = A>
template<IKind kind, bool diagnose = false, class F , class Env , class I >
CUDA NI bool lala::BAB< A, B >::interpret ( const F & f,
Env & env,
I & intermediate,
IDiagnostics & diagnostics ) const
inline

◆ deduce() [1/3]

template<class A , class B = A>
template<class Alloc >
CUDA bool lala::BAB< A, B >::deduce ( const tell_type< Alloc > & t)
inline

◆ deinterpret_best_bound() [1/2]

template<class A , class B = A>
template<class Alloc2 >
CUDA NI TFormula< Alloc2 > lala::BAB< A, B >::deinterpret_best_bound ( const typename best_type::universe_type & best_bound,
const Alloc2 & alloc = Alloc2{} ) const
inline

◆ deinterpret_best_bound() [2/2]

template<class A , class B = A>
template<class Alloc2 >
CUDA TFormula< Alloc2 > lala::BAB< A, B >::deinterpret_best_bound ( const Alloc2 & alloc = Alloc2{}) const
inline

◆ deduce() [2/3]

template<class A , class B = A>
CUDA local::B lala::BAB< A, B >::deduce ( const typename best_type::universe_type & best_bound)
inline

Update the variable to optimize objective_var() with a new bound.

◆ compare_bound()

template<class A , class B = A>
template<class Store1 , class Store2 >
CUDA bool lala::BAB< A, B >::compare_bound ( const Store1 & store1,
const Store2 & store2 ) const
inline

Compare the best bound of two stores on the objective variable represented in this BAB abstract element.

Precondition
is_optimization() must be true.
Returns
true if store1 is strictly better than store2, false otherwise.

◆ deduce() [3/3]

template<class A , class B = A>
CUDA local::B lala::BAB< A, B >::deduce ( )
inline

This deduction operator performs "branch-and-bound" by adding a constraint to the root node of the search tree to ensure the next solution is better than the current one, and store the best solution found.

Precondition
The current subelement must be extractable, and if it is an optimization problem, have a better bound than best (this is not checked here). Beware this deduction operator is not idempotent (it must only be called once on each new solution).

◆ solutions_count()

template<class A , class B = A>
CUDA int lala::BAB< A, B >::solutions_count ( ) const
inline

◆ is_extractable()

template<class A , class B = A>
template<class ExtractionStrategy = NonAtomicExtraction>
CUDA bool lala::BAB< A, B >::is_extractable ( const ExtractionStrategy & strategy = ExtractionStrategy()) const
inline

Given an optimization problem, it is extractable only when we have explored the whole state space (indicated by the subdomain being equal to top), we have found one solution, and that solution is extractable.

◆ extract()

template<class A , class B = A>
template<class AbstractBest >
CUDA void lala::BAB< A, B >::extract ( AbstractBest & ua) const
inline

Extract the best solution found in ua.

Precondition
is_extractable() must return true.

◆ optimum()

template<class A , class B = A>
CUDA const best_type & lala::BAB< A, B >::optimum ( ) const
inline

If is_extractable() is not true, the returned element might not be an optimum, and should be seen as the best optimum found so far.

◆ optimum_ptr()

template<class A , class B = A>
CUDA best_ptr lala::BAB< A, B >::optimum_ptr ( ) const
inline

◆ is_satisfaction()

template<class A , class B = A>
CUDA bool lala::BAB< A, B >::is_satisfaction ( ) const
inline

◆ is_optimization()

template<class A , class B = A>
CUDA bool lala::BAB< A, B >::is_optimization ( ) const
inline

◆ is_minimization()

template<class A , class B = A>
CUDA bool lala::BAB< A, B >::is_minimization ( ) const
inline

◆ is_maximization()

template<class A , class B = A>
CUDA bool lala::BAB< A, B >::is_maximization ( ) const
inline

◆ objective_var()

template<class A , class B = A>
CUDA AVar lala::BAB< A, B >::objective_var ( ) const
inline

Friends And Related Symbol Documentation

◆ BAB

template<class A , class B = A>
template<class A2 , class B2 >
friend class BAB
friend

Member Data Documentation

◆ is_abstract_universe

template<class A , class B = A>
const bool lala::BAB< A, B >::is_abstract_universe = false
staticconstexpr

◆ sequential

template<class A , class B = A>
const bool lala::BAB< A, B >::sequential = sub_type::sequential
staticconstexpr

◆ is_totally_ordered

template<class A , class B = A>
const bool lala::BAB< A, B >::is_totally_ordered = false
staticconstexpr

◆ preserve_bot

template<class A , class B = A>
const bool lala::BAB< A, B >::preserve_bot = true
staticconstexpr

◆ preserve_top

template<class A , class B = A>
const bool lala::BAB< A, B >::preserve_top = true
staticconstexpr

◆ preserve_join

template<class A , class B = A>
const bool lala::BAB< A, B >::preserve_join = sub_type::preserve_join
staticconstexpr

◆ preserve_meet

template<class A , class B = A>
const bool lala::BAB< A, B >::preserve_meet = sub_type::preserve_meet
staticconstexpr

◆ injective_concretization

template<class A , class B = A>
const bool lala::BAB< A, B >::injective_concretization = sub_type::injective_concretization
staticconstexpr

◆ preserve_concrete_covers

template<class A , class B = A>
const bool lala::BAB< A, B >::preserve_concrete_covers = sub_type::preserve_concrete_covers
staticconstexpr

◆ name

template<class A , class B = A>
const char* lala::BAB< A, B >::name = "BAB"
staticconstexpr

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