3#ifndef LALA_POWER_BAB_HPP
4#define LALA_POWER_BAB_HPP
6#include "battery/vector.hpp"
7#include "battery/shared_ptr.hpp"
8#include "lala/logic/logic.hpp"
9#include "lala/universes/arith_bound.hpp"
10#include "lala/abstract_deps.hpp"
11#include "lala/vstore.hpp"
14template <
class A,
class B>
class BAB;
18 static constexpr bool value =
false;
20 template<
class A,
class B>
21 struct is_bab_like<
BAB<A, B>> {
22 static constexpr bool value =
true;
26template <
class A,
class B = A>
37 constexpr static const bool sequential = sub_type::sequential;
46 constexpr static const char*
name =
"BAB";
48 template <
class Alloc>
58 CUDA NI
tell_type(AVar
x,
bool opt,
const Alloc& alloc = Alloc{}):
61 template <
class BABTellType>
62 CUDA NI
tell_type(
const BABTellType& other,
const Alloc& alloc = Alloc{}):
72 template <
class Alloc2>
76 template <
class Alloc2>
79 template <
class A2,
class B2>
87 bool optimization_mode;
92 : atype(atype), sub(std::move(sub)), best(std::move(best)), x(),
104 template<
class A2,
class B2,
class... Allocators>
107 , sub(deps.template clone<
sub_type>(other.sub))
109 , optimization_mode(other.optimization_mode)
120 return sub->get_allocator();
124 return sub->is_bot();
128 return x.is_untyped() && sub->is_top();
132 template <
bool diagnose = false,
class F,
class Env,
class Alloc2>
134 if(
f.is_untyped() ||
f.type() ==
aty()) {
136 if(
f.seq(0).is_variable()) {
151 RETURN_INTERPRETATION_ERROR(
"Optimization predicates expect a variable to optimize (not an expression). Instead, you can create a new variable with the expression to optimize.");
154 else if(
f.type() ==
aty()) {
161 template <
bool diagnose = false,
class F,
class Env,
class Alloc2>
166 template <IKind kind,
bool diagnose = false,
class F,
class Env,
class I>
168 if constexpr(
kind == IKind::TELL) {
176 template <
class Alloc>
179 if(!
t.x.is_untyped()) {
182 optimization_mode =
t.optimization_mode;
188 template <
class Alloc2>
194 return F::make_true();
203 template <
class Alloc2>
217 return sub->deduce(
t);
224 template <
class Store1,
class Store2>
227 using Univ1 =
typename Store1::local_universe;
228 using Univ2 =
typename Store2::local_universe;
255 return solutions_found;
259 template <
class ExtractionStrategy = NonAtomicExtraction>
261 return solutions_found > 0 && sub->is_bot() && best->is_extractable(
strategy);
266 template <
class AbstractBest>
268 if constexpr(impl::is_bab_like<AbstractBest>::value) {
269 best->extract(*(
ua.best));
270 ua.solutions_found = solutions_found;
272 ua.optimization_mode = optimization_mode;
275 return best->extract(
ua);
290 return x.is_untyped();
CUDA NI bool interpret_tell(const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const
Definition bab.hpp:133
CUDA TFormula< Alloc2 > deinterpret_best_bound(const Alloc2 &alloc=Alloc2{}) const
Definition bab.hpp:204
CUDA int solutions_count() const
Definition bab.hpp:254
CUDA bool is_minimization() const
Definition bab.hpp:297
CUDA bool is_optimization() const
Definition bab.hpp:293
static constexpr const bool preserve_meet
Definition bab.hpp:43
static constexpr const bool preserve_bot
Definition bab.hpp:39
typename sub_type::template ask_type< Alloc2 > ask_type
Definition bab.hpp:77
abstract_ptr< sub_type > sub_ptr
Definition bab.hpp:31
CUDA allocator_type get_allocator() const
Definition bab.hpp:119
CUDA bool deduce(const tell_type< Alloc > &t)
Definition bab.hpp:177
CUDA bool is_maximization() const
Definition bab.hpp:301
CUDA local::B is_bot() const
Definition bab.hpp:123
static constexpr const bool is_abstract_universe
Definition bab.hpp:36
A sub_type
Definition bab.hpp:30
B best_type
Definition bab.hpp:32
CUDA AVar objective_var() const
Definition bab.hpp:305
typename A::allocator_type allocator_type
Definition bab.hpp:29
static constexpr const bool is_totally_ordered
Definition bab.hpp:38
static constexpr const bool preserve_join
Definition bab.hpp:42
static constexpr const bool preserve_concrete_covers
Definition bab.hpp:45
abstract_ptr< best_type > best_ptr
Definition bab.hpp:33
CUDA local::B deduce()
Definition bab.hpp:245
CUDA best_ptr optimum_ptr() const
Definition bab.hpp:285
CUDA const best_type & optimum() const
Definition bab.hpp:281
CUDA NI BAB(const BAB< A2, B2 > &other, AbstractDeps< Allocators... > &deps)
Definition bab.hpp:105
CUDA void extract(AbstractBest &ua) const
Definition bab.hpp:267
CUDA AType aty() const
Definition bab.hpp:115
CUDA bool compare_bound(const Store1 &store1, const Store2 &store2) const
Definition bab.hpp:225
CUDA BAB(AType atype, sub_ptr sub, best_ptr best)
Definition bab.hpp:91
static constexpr const bool preserve_top
Definition bab.hpp:40
static constexpr const char * name
Definition bab.hpp:46
static constexpr const bool injective_concretization
Definition bab.hpp:44
static constexpr const bool sequential
Definition bab.hpp:37
CUDA bool is_satisfaction() const
Definition bab.hpp:289
CUDA local::B is_top() const
Definition bab.hpp:127
CUDA local::B deduce(const typename best_type::universe_type &best_bound)
Definition bab.hpp:209
CUDA NI bool interpret_ask(const F &f, const Env &env, ask_type< Alloc2 > &ask, IDiagnostics &diagnostics) const
Definition bab.hpp:162
CUDA NI bool interpret(const F &f, Env &env, I &intermediate, IDiagnostics &diagnostics) const
Definition bab.hpp:167
CUDA bool is_extractable(const ExtractionStrategy &strategy=ExtractionStrategy()) const
Definition bab.hpp:260
CUDA NI TFormula< Alloc2 > deinterpret_best_bound(const typename best_type::universe_type &best_bound, const Alloc2 &alloc=Alloc2{}) const
Definition bab.hpp:189
bool optimization_mode
Definition bab.hpp:52
tell_type(const Alloc &alloc=Alloc{})
Definition bab.hpp:54
tell_type(const tell_type< Alloc > &)=default
CUDA NI tell_type(AVar x, bool opt, const Alloc &alloc=Alloc{})
Definition bab.hpp:58
sub_tell_type sub_tell
Definition bab.hpp:53
Alloc allocator_type
Definition bab.hpp:67
sub_type::template tell_type< Alloc > sub_tell_type
Definition bab.hpp:50
CUDA allocator_type get_allocator() const
Definition bab.hpp:68
CUDA NI tell_type(const BABTellType &other, const Alloc &alloc=Alloc{})
Definition bab.hpp:62
AVar x
Definition bab.hpp:51
tell_type & operator=(tell_type< Alloc > &&)=default
tell_type(tell_type< Alloc > &&)=default