3#ifndef LALA_CORE_SIMPLIFIER_HPP
4#define LALA_CORE_SIMPLIFIER_HPP
9#include "battery/dynamic_bitset.hpp"
20 template <
class StatPr
inter>
21 CUDA
void print(StatPrinter& stats,
size_t fp_iter) {
29 template <
class StatPr
inter>
30 CUDA
void print(StatPrinter& stats) {
57template<
class A,
class Allocator>
68 constexpr static const bool sequential = universe_type::sequential;
77 constexpr static const char*
name =
"Simplifier";
79 template<
class A2,
class Alloc2>
96 battery::dynamic_bitset<memory_type, allocator_type> eliminated_variables;
98 battery::dynamic_bitset<memory_type, allocator_type> eliminated_formulas;
100 battery::vector<ZUB<int, memory_type>,
allocator_type> equivalence_classes;
102 battery::vector<universe_type, allocator_type> constants;
109 : atype(atype), store_aty(store_aty), sub(sub), env(alloc)
110 , formulas(alloc), simplified_formulas(alloc)
111 , eliminated_variables(alloc), eliminated_formulas(alloc)
112 , equivalence_classes(alloc), constants(alloc)
116 : atype(other.atype), store_aty(other.store_aty), sub(std::move(other.sub)), env(other.env)
117 , formulas(std::move(other.formulas)), simplified_formulas(std::move(other.simplified_formulas))
118 , eliminated_variables(std::move(other.eliminated_variables)), eliminated_formulas(std::move(other.eliminated_formulas))
119 , equivalence_classes(std::move(other.equivalence_classes)), constants(std::move(other.constants))
125 template<
class A2,
class Alloc2>
128 , store_aty(other.store_aty)
130 , env(other.env, alloc)
131 , equivalence_classes(other.equivalence_classes, alloc)
132 , constants(other.constants, alloc)
136 return formulas.get_allocator();
145 return sub->is_bot();
150 return equivalence_classes.size();
153 template <
class Alloc>
164 template <
bool diagnose = false,
class F,
class Env,
class Alloc2>
177 template <IKind kind,
bool diagnose = false,
class F,
class Env,
class Alloc2>
179 return interpret_tell<diagnose>(f, env, tell, diagnostics);
183 eliminated_variables.resize(
num_vars);
184 eliminated_variables.reset();
185 eliminated_formulas.resize(num_cons);
186 eliminated_formulas.reset();
188 for(
int i = 0; i < constants.size(); ++i) {
189 constants[i].join_top();
191 equivalence_classes.resize(
num_vars);
192 for(
int i = 0; i < equivalence_classes.size(); ++i) {
193 equivalence_classes[i] = i;
205 for(
int i = 0; i < tnf.size(); ++i) {
208 eliminate(eliminated_formulas, i);
215 template <
class Alloc2>
217 if(t.env !=
nullptr) {
220 formulas = std::move(t.formulas);
221 simplified_formulas.resize(formulas.size());
232 assert(env.
variable_of(f.
lv())->get().avar_of(store_aty).has_value());
233 return env.
variable_of(f.
lv())->get().avar_of(store_aty).value();
237 assert(env[f.
v()].avar_of(store_aty).has_value());
238 return env[f.
v()].avar_of(store_aty).value();
245 template <
class Alloc,
class Abs,
class Env>
248 const auto& local_var = env.
variable_of(vname)->get();
249 assert(local_var.avar_of(store_aty).has_value());
250 int rep = equivalence_classes[local_var.avar_of(store_aty)->vid()];
251 const auto& rep_name = env.
name_of(
AVar{store_aty, rep});
252 auto benv_variable = benv.variable_of(rep_name);
253 if(benv_variable.has_value()) {
254 benv_variable->get().sort.print_value(b.project(benv_variable->get().avars[0]));
257 local_var.sort.print_value(constants[rep]);
263 CUDA
local::B eliminate(battery::dynamic_bitset<memory_type, allocator_type>& mask,
size_t i) {
271 CUDA
local::B eliminate(battery::dynamic_bitset<memory_type, allocator_type>& mask,
size_t i,
size_t& eliminated_constraints) {
272 if(eliminate(mask, i)) {
273 ++eliminated_constraints;
281 const auto& u = sub->project(AVar{store_aty, i});
283 local::B has_changed = constants[j].meet(u);
284 if(!constants[j].
is_bot() && constants[j].lb().value() == constants[j].ub().value()) {
285 has_changed |= eliminate(eliminated_variables, j);
297 return replace_by_equivalence(
var_of(formulas[i].seq(0)),
var_of(formulas[i].seq(1)), i, s);
302 typename sub_type::template ask_type<allocator_type> ask;
304 if(sub->interpret_ask(formulas[i], env, ask, diagnostics))
306 if(sub->template interpret_ask(formulas[i], env, ask, diagnostics))
310 return eliminate(eliminated_formulas, i);
316 auto f = formulas[i].map([&](
const F& f,
const F& parent) {
317 if(f.is_variable()) {
319 if(eliminated_variables.test(x.vid())) {
320 auto k = constants[x.vid()].template deinterpret<F>();
321 if(env[x].sort.is_bool() && k.is(F::Z) && parent.is_logical()) {
322 return k.z() == 0 ? F::make_false() : F::make_true();
326 else if(equivalence_classes[x.vid()] != x.vid()) {
327 return F::make_lvar(UNTYPED, env.name_of(AVar{store_aty, equivalence_classes[x.vid()]}));
335 return eliminate(eliminated_formulas, i);
337 if(f != simplified_formulas[i]) {
338 simplified_formulas[i] = f;
347 return constants.size() + formulas.size();
351 assert(i < num_deductions());
352 if(i < constants.size()) {
356 return cons_deduce(i - constants.size());
366 CUDA
local::B replace_by_equivalence(
AVar x,
AVar y,
int i,
size_t& eliminated_constraints) {
367 return replace_by_equivalence(x.
vid(), y.
vid(), i, eliminated_constraints);
370 CUDA local::B replace_by_equivalence(
int x,
int y,
int i,
size_t& eliminated_constraints) {
372 return eliminate(eliminated_formulas, i, eliminated_constraints);
387 auto hash = [](
const std::tuple<int,Sig,int> &right_tnf) {
388 return static_cast<size_t>(std::get<0>(right_tnf))
389 *
static_cast<size_t>(std::get<1>(right_tnf))
390 *
static_cast<size_t>(std::get<2>(right_tnf));
393 auto equal = [](
const std::tuple<int,Sig,int> &l,
const std::tuple<int,Sig,int> &r){
394 return std::get<1>(l) == std::get<1>(r)
395 && ((std::get<0>(l) == std::get<0>(r) && std::get<2>(l) == std::get<2>(r)));
398 std::unordered_map<std::tuple<int,Sig,int>, int,
decltype(hash),
decltype(equal)> cs(tnf.size(), hash, equal);
399 bool has_changed =
false;
400 bool local_has_changed =
true;
401 while(local_has_changed) {
403 local_has_changed =
false;
405 for(
int i = 0; i < tnf.size(); ++i) {
406 if(!eliminated_formulas.test(i)) {
407 int x = find(var_of(tnf[i].seq(0)).vid());
408 int y = find(var_of(tnf[i].seq(1).seq(0)).vid());
409 int z = find(var_of(tnf[i].seq(1).seq(1)).vid());
410 Sig op = tnf[i].seq(1).sig();
411 auto p = cs.insert(std::make_pair(std::make_tuple(y, op, z), x));
414 if(local_has_changed) {
429 using F =
typename Seq::value_type;
435 bool has_changed =
false;
436 for(
int i = 0; i < tnf.size(); ++i) {
437 if(!eliminated_formulas.test(i)) {
438 int x = find(var_of(tnf[i].seq(0)).vid());
439 int y = find(var_of(tnf[i].seq(1).seq(0)).vid());
440 int z = find(var_of(tnf[i].seq(1).seq(1)).vid());
441 Sig sig = tnf[i].seq(1).sig();
442 bool x_is_c = vstore[x].lb() == vstore[x].ub();
443 bool y_is_c = vstore[y].lb() == vstore[y].ub();
444 bool z_is_c = vstore[z].lb() == vstore[z].ub();
452 if(x == y || x == z) {
453 int y2 = x == y ? z : y;
454 vstore[y2].meet(ZERO);
458 else if(vstore[z] == ZERO) {
463 tnf[i].seq(1) = F::make_binary(
472 if(x == y && z_is_c) {
473 if(vstore[z] != ONE) {
474 has_changed |= vstore[x].meet(ZERO);
481 else if(x_is_c && y == z) {
482 auto n = battery::iroots_up(vstore[x].lb().value(), 2);
483 if(n * n == vstore[x].lb()) {
487 vstore[y].meet_bot();
491 else if(vstore[z] == ONE) {
495 else if(x == y && y == z) {
503 if(vstore[y] == ONE && x == z) {
506 else if(vstore[y] == ZERO && x == z) {
507 vstore[x].meet_bot();
509 else if(x_is_c && y == z) {
510 if(vstore[x] != ONE) {
511 vstore[y].meet_bot();
515 else if(vstore[z] == ONE) {
518 else if(x == y && y == z) {
526 if(x == y && y == z) {
527 vstore[x].meet(ZERO);
531 else if(x == y && z_is_c) {
532 vstore[x].meet(
universe_type(0, std::abs(vstore[z].lb()) - 1));
536 else if(x == z && y_is_c) {
537 vstore[x].meet_bot();
540 else if(y == z && vstore[x] == ZERO) {
553 else if(x == y || x == z) {
554 int y2 = x == y ? z : y;
560 tnf[i].seq(1) = F::make_binary(
569 if(vstore[x] == ONE) {
573 else if(x == y && z_is_c) {
574 if(vstore[z] == ZERO) {
575 vstore[x].meet_bot();
577 else if(vstore[z] == ONE) {
581 vstore[x].meet(ZERO);
593 if(x == y && z_is_c) {
594 int k = vstore[z].lb();
596 vstore[x].meet(ZERO);
602 vstore[x].meet_bot();
607 else if(x == z && y_is_c) {
608 int k = vstore[y].lb();
610 vstore[x].meet(ZERO);
625 printf(
"Unsupported operator %s in TNF algebraic simplification.\n",
string_of_sig(sig));
638 CUDA
int find(
int x) {
640 while(equivalence_classes[root] != root) {
641 root = equivalence_classes[root];
643 while(equivalence_classes[x] != root) {
644 int parent = equivalence_classes[x];
645 sub->embed(AVar{store_aty, parent}, (*sub)[x]);
646 equivalence_classes[x] = root;
653 CUDA
void merge(
int x,
int y) {
658 if(rx < ry) battery::swap(rx, ry);
659 equivalence_classes[rx] = ry;
660 sub->embed(AVar{store_aty, ry}, (*sub)[rx]);
666 for(
int i = 0; i < equivalence_classes.size(); ++i) {
668 sub->embed(
AVar{store_aty, root}, (*sub)[i]);
670 for(
int i = 0; i < equivalence_classes.size(); ++i) {
672 sub->embed(
AVar{store_aty, i}, (*sub)[root]);
676 template <
class B,
class Seq>
678 for(
int i = 0; i < tnf.size(); ++i) {
679 if(!
is_tnf(tnf[i]) || eliminated_formulas.test(i)) {
683 typename sub_type::template ask_type<allocator_type> ask_value;
684 bool ask_success = b.interpret_ask(tnf[i], env, ask_value, diagnostics);
686 if(b.ask(ask_value)) {
695 eliminated_variables.set();
696 for(
int i = 0; i < tnf.size(); ++i) {
697 if(!eliminated_formulas.test(i)) {
698 eliminated_variables.set(find(var_of(tnf[i].seq(0)).vid()),
false);
699 eliminated_variables.set(find(var_of(tnf[i].seq(1).seq(0)).vid()),
false);
700 eliminated_variables.set(find(var_of(tnf[i].seq(1).seq(1)).vid()),
false);
703 num_eliminated_variables = eliminated_variables.count();
706 for(
int i = 0; i < sub->vars(); ++i) {
708 constants[i] = sub->project(
AVar{store_aty, root});
714 void substitute_var(F& f)
const {
715 if(f.is_variable()) {
718 int root = equivalence_classes[x.
vid()];
719 if(x.
vid() != root) {
720 x =
AVar{store_aty, root};
721 f = F::make_lvar(store_aty, env.
name_of(x));
724 if(eliminated_variables.test(x.
vid())) {
725 auto k = (*sub)[x.
vid()].template deinterpret<F>();
726 if(env[x].sort.is_bool() && k.is(F::Z)) {
727 f = k.z() == 0 ? F::make_false() : F::make_true();
740 f.inplace_map([
this](F& leaf,
const F&) { substitute_var(leaf); });
745 for(
int i = 0; i < equivalence_classes.size(); ++i) {
746 if(equivalence_classes[i] == i && !eliminated_variables.test(i)) {
756 CUDA
void deinterpret_vars(Seq& seq) {
758 for(
int i = 0; i < equivalence_classes.size(); ++i) {
759 if(equivalence_classes[i] == i && !eliminated_variables.test(i)) {
760 const auto& x = env[
AVar{store_aty, i}];
761 seq.push_back(F::make_exists(
UNTYPED, x.name, x.sort));
762 auto domain_constraint = constants[i].deinterpret(AVar{store_aty, i}, env, get_allocator());
764 seq.push_back(domain_constraint);
769 template <
class Seq1,
class Seq2>
770 CUDA
void deinterpret_constraints(Seq1& seq,
const Seq2& formulas,
bool enable_substitute =
false) {
772 for(
int i = 0; i < formulas.size(); ++i) {
773 if(!eliminated_formulas.test(i)) {
774 seq.push_back(formulas[i]);
775 if(enable_substitute) {
776 substitute(seq.back());
786 typename F::Sequence seq(get_allocator());
788 return F::make_false();
790 if(eliminated_variables.all() || eliminated_formulas.all()) {
791 return F::make_true();
793 deinterpret_vars(seq);
794 deinterpret_constraints(seq, source, substitute);
795 return seq.size() == 0 ? F::make_true() : F::make_nary(
AND, std::move(seq));
799 return deinterpret(simplified_formulas,
false);
CUDA constexpr int vid() const
Definition ast.hpp:69
Definition diagnostics.hpp:19
Definition simplifier.hpp:58
CUDA allocator_type get_allocator() const
Definition simplifier.hpp:135
static constexpr const bool preserve_bot
Definition simplifier.hpp:71
CUDA local::B deduce(size_t i)
Definition simplifier.hpp:350
CUDA Simplifier(this_type &&other)
Definition simplifier.hpp:115
CUDA bool deduce(tell_type< Alloc2 > &&t)
Definition simplifier.hpp:216
Allocator allocator_type
Definition simplifier.hpp:60
A sub_type
Definition simplifier.hpp:61
CUDA size_t vars() const
Definition simplifier.hpp:149
static constexpr const bool preserve_join
Definition simplifier.hpp:73
CUDA void init_env(const Env &env)
Definition simplifier.hpp:361
CUDA local::B is_bot() const
Definition simplifier.hpp:144
static constexpr const bool injective_concretization
Definition simplifier.hpp:75
CUDA local::B cons_deduce(int i)
Definition simplifier.hpp:291
CUDA void eliminate_entailed_constraints(const B &b, const Seq &tnf, SimplifierStats &stats)
Definition simplifier.hpp:677
CUDA AVar var_of(const TFormula< allocator_type > &f) const
Definition simplifier.hpp:228
CUDA NI bool interpret_tell(const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const
Definition simplifier.hpp:165
CUDA NI TFormula< allocator_type > deinterpret(const Seq &source, bool substitute)
Definition simplifier.hpp:784
battery::vector< TFormula< allocator_type >, allocator_type > formula_sequence
Definition simplifier.hpp:82
CUDA bool interpret(const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const
Definition simplifier.hpp:178
CUDA bool algebraic_simplify(Seq &tnf, SimplifierStats &stats)
Definition simplifier.hpp:428
CUDA bool i_cse(const Seq &tnf, SimplifierStats &stats)
Definition simplifier.hpp:386
CUDA size_t num_vars_after_elimination() const
Definition simplifier.hpp:743
CUDA AType aty() const
Definition simplifier.hpp:139
static constexpr const bool preserve_top
Definition simplifier.hpp:72
CUDA void eliminate_useless_variables(const Seq &tnf, size_t &num_eliminated_variables)
Definition simplifier.hpp:693
static constexpr const char * name
Definition simplifier.hpp:77
static constexpr const bool is_abstract_universe
Definition simplifier.hpp:67
static constexpr const bool is_totally_ordered
Definition simplifier.hpp:69
CUDA Simplifier(AType atype, AType store_aty, abstract_ptr< sub_type > sub, const allocator_type &alloc=allocator_type())
Definition simplifier.hpp:105
CUDA size_t num_deductions() const
Definition simplifier.hpp:346
typename sub_type::allocator_type sub_allocator_type
Definition simplifier.hpp:62
typename universe_type::memory_type memory_type
Definition simplifier.hpp:64
CUDA void substitute(F &f) const
Definition simplifier.hpp:739
CUDA NI TFormula< allocator_type > deinterpret()
Definition simplifier.hpp:798
CUDA void initialize(int num_vars, int num_cons)
Definition simplifier.hpp:182
CUDA void initialize_tnf(int num_vars, const Seq &tnf)
Definition simplifier.hpp:202
CUDA void print_variable(const LVar< Alloc > &vname, const Env &benv, const Abs &b) const
Definition simplifier.hpp:246
CUDA Simplifier(const Simplifier< A2, Alloc2 > &other, light_copy_tag tag, abstract_ptr< sub_type > sub, const allocator_type &alloc=allocator_type())
Definition simplifier.hpp:126
static constexpr const bool sequential
Definition simplifier.hpp:68
typename sub_type::universe_type universe_type
Definition simplifier.hpp:63
CUDA void meet_equivalence_classes()
Definition simplifier.hpp:665
static constexpr const bool preserve_concrete_covers
Definition simplifier.hpp:76
static constexpr const bool preserve_meet
Definition simplifier.hpp:74
CUDA NI std::optional< std::reference_wrapper< const variable_type > > variable_of(const char *lv) const
Definition env.hpp:478
CUDA const bstring & name_of(AVar av) const
Definition env.hpp:517
::lala::B<::battery::local_memory > B
Definition b.hpp:12
Definition abstract_deps.hpp:14
CUDA NI constexpr bool is_commutative(Sig sig)
Definition ast.hpp:243
CUDA NI void map_avar_to_lvar(F &f, const Env &env, bool erase_type=false)
Definition algorithm.hpp:438
@ LEQ
Unary arithmetic function symbols.
Definition ast.hpp:113
@ EQ
Unary arithmetic function symbols.
Definition ast.hpp:112
@ ADD
Unary arithmetic function symbols.
Definition ast.hpp:97
@ MIN
Unary arithmetic function symbols.
Definition ast.hpp:97
@ EDIV
Unary arithmetic function symbols.
Definition ast.hpp:105
@ MAX
Binary arithmetic function symbols.
Definition ast.hpp:97
@ AND
Unary arithmetic function symbols.
Definition ast.hpp:114
@ EQUIV
Unary arithmetic function symbols.
Definition ast.hpp:114
@ MUL
Unary arithmetic function symbols.
Definition ast.hpp:97
@ EMOD
Euclidean division (Boute T. R. (1992). The Euclidean definition of the functions div and mod)....
Definition ast.hpp:105
battery::shared_ptr< A, typename A::allocator_type > abstract_ptr
Definition abstract_deps.hpp:17
int AType
Definition sort.hpp:18
CUDA NI bool is_var_equality(const TFormula< Allocator, ExtendedSig > &f)
Definition algorithm.hpp:33
CUDA NI const char * string_of_sig(Sig sig)
Definition ast.hpp:121
CUDA NI int num_vars(const F &f)
Definition algorithm.hpp:154
battery::string< Allocator > LVar
Definition ast.hpp:25
CUDA NI F eval(const F &f)
Definition algorithm.hpp:814
CUDA bool is_tnf(const F &f)
Definition ternarize.hpp:28
#define UNTYPED
Definition sort.hpp:21
Definition simplifier.hpp:122
Definition simplifier.hpp:154
tell_type(const Alloc &alloc=Alloc())
Definition simplifier.hpp:158
int num_vars
Definition simplifier.hpp:155
VarEnv< Alloc > * env
Definition simplifier.hpp:157
formula_sequence formulas
Definition simplifier.hpp:156
Definition simplifier.hpp:13
size_t eliminated_equality_constraints
Definition simplifier.hpp:15
size_t eliminated_constraints_by_as
Definition simplifier.hpp:16
CUDA void merge(SimplifierStats &other)
Definition simplifier.hpp:38
size_t icse_fixpoint_iterations
Definition simplifier.hpp:18
CUDA void print(StatPrinter &stats)
Definition simplifier.hpp:30
size_t eliminated_constraints_by_icse
Definition simplifier.hpp:14
CUDA void print(StatPrinter &stats, size_t fp_iter)
Definition simplifier.hpp:21
size_t eliminated_entailed_constraints
Definition simplifier.hpp:17