3#ifndef TURBO_COMMON_SOLVING_HPP
4#define TURBO_COMMON_SOLVING_HPP
17#include "battery/utility.hpp"
18#include "battery/allocator.hpp"
19#include "battery/vector.hpp"
20#include "battery/shared_ptr.hpp"
22#include "lala/simplifier.hpp"
23#include "lala/vstore.hpp"
24#include "lala/cartesian_product.hpp"
25#include "lala/interval.hpp"
27#include "lala/terms.hpp"
28#include "lala/fixpoint.hpp"
29#include "lala/search_tree.hpp"
30#include "lala/bab.hpp"
31#include "lala/split_strategy.hpp"
32#include "lala/interpretation.hpp"
34#include "lala/flatzinc_parser.hpp"
36#ifdef WITH_XCSP3PARSER
37 #include "lala/XCSP3_parser.hpp"
47static std::atomic<bool> got_signal;
48static void (*prev_sigint)(int);
49static void (*prev_sigterm)(int);
51void signal_handler(
int signum)
53 signal(SIGINT, signal_handler);
54 signal(SIGTERM, signal_handler);
58 if (signum == SIGINT && prev_sigint != SIG_DFL && prev_sigint != SIG_IGN) {
59 (*prev_sigint)(signum);
61 if (signum == SIGTERM && prev_sigterm != SIG_DFL && prev_sigterm != SIG_IGN) {
62 (*prev_sigterm)(signum);
67 prev_sigint = signal(SIGINT, signal_handler);
68 prev_sigterm = signal(SIGTERM, signal_handler);
72 return static_cast<bool>(got_signal);
80 sigaddset(&ctrlc, SIGINT);
81 sigaddset(&ctrlc, SIGTERM);
82 if(sigprocmask(SIG_BLOCK, &ctrlc, NULL) != 0) {
83 printf(
"%% ERROR: Unable to deal with CTRL-C. Therefore, we will not be able to print the latest solution before quitting.\n");
90 sigset_t pending_sigs;
91 sigemptyset(&pending_sigs);
92 sigpending(&pending_sigs);
93 return sigismember(&pending_sigs, SIGINT) == 1 || sigismember(&pending_sigs, SIGTERM) == 1;
100template <
class A,
class Timepo
int>
102 auto now = std::chrono::high_resolution_clock::now();
103 a.stats.duration = std::chrono::duration_cast<std::chrono::milliseconds>(now - start).count();
104 if(a.config.timeout_ms == 0) {
107 if(a.stats.duration >=
static_cast<int64_t
>(a.config.timeout_ms)) {
108 if(a.config.verbose_solving) {
109 printf(
"%% CPU: Timeout reached.\n");
111 a.stats.exhaustive =
false;
118template <
class Alloc,
size_t n>
133template <
class Alloc,
size_t n>
136 return Alloc{}.allocate(bytes);
139 Alloc{}.deallocate(data);
150template <
class Universe,
151 class BasicAllocator,
153 class StoreAllocator>
158 using LIStore = VStore<universe_type, BasicAllocator>;
160 using IStore = VStore<Universe, StoreAllocator>;
161 using IPC = PC<IStore, PropAllocator>;
163 using Split = SplitStrategy<IPC, BasicAllocator>;
164 using IST = SearchTree<IPC, Split, BasicAllocator>;
165 using IBAB = BAB<IST, LIStore>;
182 template <
class U2,
class BasicAlloc2,
class PropAllocator2,
class StoreAllocator2>
206 store = deps.template clone<IStore>(other.
store);
207 ipc = deps.template clone<IPC>(other.
ipc);
208 split = deps.template clone<Split>(other.
split);
211 bab = deps.template clone<IBAB>(other.
bab);
215 template <
class U2,
class BasicAlloc2,
class PropAllocator2,
class StoreAllocator2>
235 template <
class Alloc>
272 VarEnv<BasicAllocator>
env;
295 printf(
"%% Abstract domain allocated.\n");
316 if(f.sig() == ::lala::IN && f.seq(1).is(F::S) && f.seq(1).s().size() > 1) {
317 f.type_as(
ipc->aty());
320 for(
int i = 0; i < f.seq().size(); ++i) {
325 for(
int i = 0; i < f.eseq().size(); ++i) {
335 template <
class F,
class Env,
class A>
336 CUDA
bool interpret_and_diagnose_and_tell(
const F& f, Env&
env, A& a) {
337 IDiagnostics diagnostics;
338 if(!interpret_and_tell(f,
env, a, diagnostics)) {
339 IDiagnostics diagnostics2;
340 interpret_and_tell<true>(f,
env, a, diagnostics2);
341 diagnostics2.print();
351 printf(
"%% Interpreting the formula...\n");
353 if(!interpret_and_diagnose_and_tell(f,
env, *
bab)) {
358 bool can_interpret =
true;
359 if(
split->num_strategies() == 0) {
360 can_interpret &= interpret_default_strategy<F>();
363 can_interpret &= interpret_default_eps_strategy<F>();
365 return can_interpret;
371 printf(
"%% Simplifying the formula...\n");
373 IDiagnostics diagnostics;
374 typename ISimplifier::template tell_type<basic_allocator_type> tell{
basic_allocator};
375 if(top_level_ginterpret_in<IKind::TELL>(*
simplifier, f,
env, tell, diagnostics)) {
380 printf(
"WARNING: Could not simplify the formula because:\n");
381 IDiagnostics diagnostics2;
382 top_level_ginterpret_in<IKind::TELL, true>(*
simplifier, f,
env, tell, diagnostics2);
383 diagnostics2.print();
391 printf(
"%% Typing the formula...\n");
395 printf(
"%% Typed AST:\n");
404 printf(
"%% Interpreted AST:\n");
405 ipc->deinterpret(
env).print(
true);
409 printf(
"%% Formula has been interpreted.\n");
416 auto start = std::chrono::high_resolution_clock::now();
423#ifdef WITH_XCSP3PARSER
429 std::cerr <<
"Could not parse input file." << std::endl;
434 printf(
"%% Input file parsed\n");
438 printf(
"%% Parsed AST:\n");
446 auto interpretation_time = std::chrono::high_resolution_clock::now();
453 auto start = std::chrono::high_resolution_clock::now();
455 GaussSeidelIteration fp_engine;
456 fp_engine.fixpoint(*
ipc);
464 auto interpretation_time = std::chrono::high_resolution_clock::now();
470 CUDA
bool interpret_default_strategy() {
472 printf(
"%% No split strategy provided, using the default one (first_fail, indomain_min).\n");
475 typename F::Sequence seq;
476 seq.push_back(F::make_nary(
"first_fail", {}));
477 seq.push_back(F::make_nary(
"indomain_min", {}));
478 for(
int i = 0; i <
env.num_vars(); ++i) {
479 seq.push_back(F::make_avar(
env[i].avars[0]));
481 F search_strat = F::make_nary(
"search", std::move(seq));
482 if(!interpret_and_diagnose_and_tell(search_strat,
env, *
bab)) {
489 CUDA
bool interpret_default_eps_strategy() {
490 typename F::Sequence seq;
491 seq.push_back(F::make_nary(
"first_fail", {}));
492 seq.push_back(F::make_nary(
"indomain_min", {}));
493 for(
int i = 0; i <
env.num_vars(); ++i) {
494 seq.push_back(F::make_avar(
env[i].avars[0]));
496 F search_strat = F::make_nary(
"search", std::move(seq));
497 if(!interpret_and_diagnose_and_tell(search_strat,
env, *
eps_split)) {
561 if(!
bab->objective_var().is_untyped() && !
best->is_top()) {
569 template <
class U2,
class BasicAlloc2,
class PropAlloc2,
class StoreAlloc2>
571 if(
bab->is_optimization() && !other.
best->is_top() &&
bab->compare_bound(*other.
best, *
best)) {
578using Itv = Interval<local::ZLB>;
580template <
class Universe>
582 battery::statistics_allocator<battery::standard_allocator>,
583 battery::statistics_allocator<UniqueLightAlloc<battery::standard_allocator, 0>>,
584 battery::statistics_allocator<UniqueLightAlloc<battery::standard_allocator, 1>>>;
Interval< local::ZLB > Itv
Definition common_solving.hpp:578
bool must_quit()
Definition common_solving.hpp:89
void block_signal_ctrlc()
Definition common_solving.hpp:77
bool check_timeout(A &a, const Timepoint &start)
Definition common_solving.hpp:101
Definition common_solving.hpp:173
Definition common_solving.hpp:175
Definition common_solving.hpp:154
abstract_ptr< IBAB > bab
Definition common_solving.hpp:269
void type_and_interpret(F &f)
Definition common_solving.hpp:389
SearchTree< IPC, Split, BasicAllocator > IST
Definition common_solving.hpp:164
Configuration< BasicAllocator > config
Definition common_solving.hpp:277
CUDA void typing(F &f) const
Definition common_solving.hpp:313
CUDA bool interpret(const F &f)
Definition common_solving.hpp:349
CUDA void deallocate()
Definition common_solving.hpp:300
VStore< universe_type, BasicAllocator > LIStore
Definition common_solving.hpp:158
CUDA void print_final_solution()
Definition common_solving.hpp:550
StoreAllocator store_allocator
Definition common_solving.hpp:260
CUDA AbstractDomains(const tag_gpu_block_copy &, bool enable_sharing, const AbstractDomains< U2, BasicAlloc2, PropAllocator2, StoreAllocator2 > &other, const BasicAllocator &basic_allocator=BasicAllocator(), const PropAllocator &prop_allocator=PropAllocator(), const StoreAllocator &store_allocator=StoreAllocator())
Definition common_solving.hpp:183
CUDA bool prepare_simplifier(F &f)
Definition common_solving.hpp:369
CUDA void allocate(int num_vars)
Definition common_solving.hpp:280
BasicAllocator basic_allocator
Definition common_solving.hpp:258
BAB< IST, LIStore > IBAB
Definition common_solving.hpp:165
CUDA void meet(AbstractDomains< U2, BasicAlloc2, PropAlloc2, StoreAlloc2 > &other)
Definition common_solving.hpp:570
CUDA bool on_solution_node()
Definition common_solving.hpp:539
CUDA bool on_node()
Definition common_solving.hpp:504
abstract_ptr< LIStore > best
Definition common_solving.hpp:268
battery::shared_ptr< TFormula< basic_allocator_type >, basic_allocator_type > FormulaPtr
Definition common_solving.hpp:413
AbstractDomains(AbstractDomains &&other)=default
abstract_ptr< IStore > store
Definition common_solving.hpp:262
VarEnv< BasicAllocator > env
Definition common_solving.hpp:272
CUDA bool is_printing_intermediate_sol()
Definition common_solving.hpp:514
Simplifier< IPC, BasicAllocator > ISimplifier
Definition common_solving.hpp:162
FormulaPtr prepare_solver()
Definition common_solving.hpp:415
abstract_ptr< IPC > ipc
Definition common_solving.hpp:263
PC< IStore, PropAllocator > IPC
Definition common_solving.hpp:161
CUDA AbstractDomains(const AbstractDomains< U2, BasicAlloc2, PropAllocator2, StoreAllocator2 > &other, const BasicAllocator &basic_allocator=BasicAllocator(), const PropAllocator &prop_allocator=PropAllocator(), const StoreAllocator &store_allocator=StoreAllocator(), const tag_copy_cons &tag=tag_copy_cons{})
Definition common_solving.hpp:216
abstract_ptr< IST > search_tree
Definition common_solving.hpp:267
CUDA void on_failed_node()
Definition common_solving.hpp:546
PropAllocator prop_allocator_type
Definition common_solving.hpp:168
BasicAllocator basic_allocator_type
Definition common_solving.hpp:167
SplitStrategy< IPC, BasicAllocator > Split
Definition common_solving.hpp:163
abstract_ptr< ISimplifier > simplifier
Definition common_solving.hpp:264
abstract_ptr< Split > eps_split
Definition common_solving.hpp:266
void preprocess()
Definition common_solving.hpp:451
abstract_ptr< Split > split
Definition common_solving.hpp:265
Statistics stats
Definition common_solving.hpp:278
SolverOutput< BasicAllocator > solver_output
Definition common_solving.hpp:275
CUDA bool update_solution_stats()
Definition common_solving.hpp:528
PropAllocator prop_allocator
Definition common_solving.hpp:259
typename Universe::local_type universe_type
Definition common_solving.hpp:155
VStore< Universe, StoreAllocator > IStore
Definition common_solving.hpp:160
StoreAllocator store_allocator_type
Definition common_solving.hpp:169
CUDA void print_solution()
Definition common_solving.hpp:518
CUDA void prune()
Definition common_solving.hpp:523
CUDA AbstractDomains(const this_type &other, const BasicAllocator &basic_allocator=BasicAllocator(), const PropAllocator &prop_allocator=PropAllocator(), const StoreAllocator &store_allocator=StoreAllocator())
Definition common_solving.hpp:228
CUDA AbstractDomains(const Configuration< Alloc > &config, const BasicAllocator &basic_allocator=BasicAllocator(), const PropAllocator &prop_allocator=PropAllocator(), const StoreAllocator &store_allocator=StoreAllocator())
Definition common_solving.hpp:236
CUDA void print_mzn_statistics()
Definition common_solving.hpp:557
size_t stop_after_n_nodes
Definition config.hpp:32
battery::string< allocator_type > problem_path
Definition config.hpp:45
CUDA InputFormat input_format() const
Definition config.hpp:181
bool print_intermediate_solutions
Definition config.hpp:30
bool print_ast
Definition config.hpp:36
CUDA void print_mzn_statistics() const
Definition config.hpp:157
bool verbose_solving
Definition config.hpp:35
size_t stop_after_n_solutions
Definition config.hpp:31
bool free_search
Definition config.hpp:33
bool print_statistics
Definition config.hpp:34
Definition statistics.hpp:12
size_t fails
Definition statistics.hpp:19
size_t depth_max
Definition statistics.hpp:21
CUDA void print_mzn_statistics() const
Definition statistics.hpp:78
size_t constraints
Definition statistics.hpp:14
CUDA void print_mzn_objective(const auto &obj, bool is_minimization) const
Definition statistics.hpp:104
CUDA void meet(const Statistics &other)
Definition statistics.hpp:48
int64_t interpretation_duration
Definition statistics.hpp:17
CUDA void print_mzn_end_stats() const
Definition statistics.hpp:100
size_t eliminated_variables
Definition statistics.hpp:28
CUDA void print_mzn_final_separator() const
Definition statistics.hpp:119
size_t nodes
Definition statistics.hpp:18
size_t eliminated_formulas
Definition statistics.hpp:29
size_t solutions
Definition statistics.hpp:20
size_t variables
Definition statistics.hpp:13
CUDA void print_mzn_separator() const
Definition statistics.hpp:115
size_t exhaustive
Definition statistics.hpp:22
Definition common_solving.hpp:119
CUDA void deallocate(void *data)
Definition common_solving.hpp:128
UniqueAlloc(const UniqueAlloc &alloc)=default
UniqueAlloc & operator=(const UniqueAlloc &alloc)=default
Alloc allocator
Definition common_solving.hpp:120
CUDA void * allocate(size_t bytes)
Definition common_solving.hpp:125
CUDA UniqueAlloc(const Alloc &alloc)
Definition common_solving.hpp:122
Definition common_solving.hpp:134
CUDA void * allocate(size_t bytes)
Definition common_solving.hpp:135
CUDA void deallocate(void *data)
Definition common_solving.hpp:138