common_solving.hpp File Reference

#include <atomic>
#include <algorithm>
#include <chrono>
#include <thread>
#include <csignal>
#include "config.hpp"
#include "statistics.hpp"
#include "battery/utility.hpp"
#include "battery/allocator.hpp"
#include "battery/vector.hpp"
#include "battery/shared_ptr.hpp"
#include "lala/simplifier.hpp"
#include "lala/vstore.hpp"
#include "lala/cartesian_product.hpp"
#include "lala/interval.hpp"
#include "lala/pc.hpp"
#include "lala/pir.hpp"
#include "lala/fixpoint.hpp"
#include "lala/search_tree.hpp"
#include "lala/bab.hpp"
#include "lala/split_strategy.hpp"
#include "lala/interpretation.hpp"
#include "lala/flatzinc_parser.hpp"

Go to the source code of this file.

Classes
struct	UniqueAlloc< Alloc, n >
struct	UniqueLightAlloc< Alloc, n >
struct	AbstractDomains< Universe, BasicAllocator, PropAllocator, StoreAllocator >
struct	AbstractDomains< Universe, BasicAllocator, PropAllocator, StoreAllocator >::tag_copy_cons
struct	AbstractDomains< Universe, BasicAllocator, PropAllocator, StoreAllocator >::tag_gpu_block_copy

Macros
#define	TURBO_ITV_BITS   32
#define	STR_(x)   #x
#define	STR(x)   STR_(x)

Typedefs
using	bound_value_type = int
using	Itv = Interval< ZLB< bound_value_type, battery::local_memory > >
template<class Universe , class Allocator = battery::standard_allocator>
using	CP = AbstractDomains< Universe, battery::statistics_allocator< Allocator >, battery::statistics_allocator< UniqueLightAlloc< Allocator, 0 > >, battery::statistics_allocator< UniqueLightAlloc< Allocator, 1 > > >

Functions
void	signal_handler (int signum)
void	block_signal_ctrlc ()
template<class A >
bool	must_quit (A &a)
template<class A , class Timepoint >
bool	check_timeout (A &a, const Timepoint &start)

Macro Definition Documentation

TURBO_ITV_BITS

#define TURBO_ITV_BITS   32

STR_

#define STR_

(

x

)

#x

STR

#define STR

(

x

)

STR_(x)

Typedef Documentation

bound_value_type

using bound_value_type = int

Itv

using Itv = Interval<ZLB<bound_value_type, battery::local_memory> >

CP

template<class Universe , class Allocator = battery::standard_allocator>

using CP = AbstractDomains<Universe, battery::statistics_allocator<Allocator>, battery::statistics_allocator<UniqueLightAlloc<Allocator, 0> >, battery::statistics_allocator<UniqueLightAlloc<Allocator, 1> >>

Function Documentation

signal_handler()

void signal_handler

(

int

signum

)

block_signal_ctrlc()

void block_signal_ctrlc

(

)

must_quit()

template<class A >

bool must_quit

(

A &

a

)

check_timeout()

template<class A , class Timepoint >

bool check_timeout	(	A &	a,
		const Timepoint &	start
	)

Check if the timeout of the current execution is exceeded and returns false otherwise. It also update the statistics relevant to the solving duration and the exhaustive flag if we reach the timeout.