{

uint32_t x;

constexpr explicit Lit(uint32_t i) : x(i) { }

constexpr Lit() : x(var_Undef<<1) {} // (lit_Undef)

constexpr explicit Lit(uint32_t var, bool is_inverted) :

x(var + var + is_inverted)

{}

constexpr const uint32_t& toInt() const { // Guarantees small, positive integers suitable for array indexing.

return x;

}

constexpr Lit operator~() const {

return Lit(x ^ 1);

}

constexpr Lit operator^(const bool b) const {

return Lit(x ^ static_cast<uint32_t>(b));

}

constexpr Lit& operator^=(const bool b) {

x ^= static_cast<uint32_t>(b);

return *this;

}

constexpr bool sign() const {

return x & 1;

}

constexpr uint32_t var() const {

return x >> 1;

}

constexpr Lit unsign() const {

return Lit(x & ~1U);

}

constexpr bool operator==(const Lit& p) const {

return x == p.x;

}

constexpr bool operator!= (const Lit& p) const {

return x != p.x;

}

/**

constexpr bool operator < (const Lit& p) const {

return x < p.x; // '<' guarantees that p, ~p are adjacent in the ordering.

}

constexpr bool operator > (const Lit& p) const {

return x > p.x;

}

constexpr bool operator >= (const Lit& p) const {

return x >= p.x;

}

constexpr static Lit toLit(uint32_t data)

{

return Lit(data);

}

template <class Archive>

void serialize(Archive& ar, const unsigned int /*version*/) {

ar & x;

}

uint8_t value;

constexpr explicit lbool(uint8_t v) : value(v) { }

constexpr lbool() : value(0) { }

constexpr explicit lbool(bool x) : value(!x) { }

constexpr bool operator == (lbool b) const {

return ((b.value & 2) & (value & 2)) | (!(b.value & 2) & (value == b.value));

}

constexpr bool operator != (lbool b) const {

return !(*this == b);

}

constexpr lbool operator ^ (bool b) const {

return lbool(static_cast<uint8_t>(value ^ static_cast<uint8_t>(b)));

}

constexpr lbool operator && (lbool b) const {

uint8_t sel = (value << 1) | (b.value << 3);

uint8_t v = (0xF7F755F4 >> sel) & 3;

return lbool(v);

}

constexpr lbool operator || (lbool b) const {

uint8_t sel = (value << 1) | (b.value << 3);

uint8_t v = (0xFCFCF400 >> sel) & 3;

return lbool(v);

}

template<class Archive>

void serialize(Archive& ar, const unsigned int /*version*/) {

ar & value;

}

constexpr uint8_t getValue() const { return value; }

friend lbool toLbool(uint8_t v);

constexpr friend uint32_t toInt (lbool l);

{

lbool l;

l.value = v;

return l;

public:

template<typename T>

OrGate(const Lit& _rhs, const T& _lits, int32_t _ID) :

lits(_lits), rhs(_rhs), id(_ID)

{

assert(std::is_sorted(lits.begin(), lits.end()));

}

bool operator==(const OrGate& other) const

{

return rhs == other.rhs && lits == other.lits;

}

const std::vector<Lit>& get_lhs() const

{

return lits;

}

//LHS

std::vector<Lit> lits;

//RHS

Lit rhs;

//ID of long clause

int32_t id;

public:

ITEGate() {}

ITEGate(const Lit& _rhs, Lit _lit1, Lit _lit2, Lit _lit3) :

rhs(_rhs)

{

lhs[0] = _lit1;

lhs[1] = _lit2;

lhs[2] = _lit3;

std::sort(lhs.begin(), lhs.end());

}

std::array<Lit, 4> get_all() const

{

return std::array<Lit, 4>{{lhs[0], lhs[1], lhs[2], rhs}};

}

//LHS

std::array<Lit, 3> lhs;

//RHS

Lit rhs;

polarmode_pos

, polarmode_neg

, polarmode_rnd

, polarmode_automatic

, polarmode_stable

, polarmode_best_inv

, polarmode_best

, polarmode_saved

, polarmode_weighted

std::vector<Lit>* _assumptions = nullptr;

std::vector<uint32_t>* indic_to_var = nullptr;

uint32_t orig_num_vars = 0;

std::vector<uint32_t>* non_indep_vars = nullptr;

std::vector<uint32_t>* indep_vars = nullptr;

bool fast_backw_on = false;

uint32_t* test_var = nullptr;

uint32_t* test_indic = nullptr;

uint32_t max_confl = 500;

uint32_t cur_max_confl = 0;

uint32_t indep_because_ran_out_of_confl = 0;

uint64_t start_sumConflicts;

{

typedef Lit* iterator;

typedef const Lit* const_iterator;

BNN()

{}

explicit BNN(

const std::vector<Lit>& _in,

const int32_t _cutoff,

const Lit _out):

cutoff(_cutoff),

out (_out)

{

if (out == lit_Undef) {

set = true;

}

assert(_in.size() > 0);

undefs = _in.size();

ts = 0;

sz = _in.size();

std::copy(_in.begin(), _in.end(), getData());

}

Lit* getData()

{

return reinterpret_cast<Lit*>(reinterpret_cast<char*>(this) + sizeof(BNN));

}

const Lit* getData() const

{

return reinterpret_cast<const Lit*>(reinterpret_cast<const char*>(this) + sizeof(BNN));

}

const Lit& operator[](const uint32_t at) const

{

return getData()[at];

}

Lit& operator[](const uint32_t at)

{

return getData()[at];

}

const Lit& get_out() const

{

return out;

}

const Lit* begin() const

{

return getData();

}

Lit* begin()

{

return getData();

}

const Lit* end() const

{

return getData()+size();

}

Lit* end()

{

return getData()+size();

}

bool empty() const

{

return sz == 0;

}

void resize(uint32_t _sz) {

sz = _sz;

}

uint32_t size() const {

return sz;

}

int32_t cutoff;

Lit out = lit_Undef;

bool set = false;

bool isRemoved = false;

int32_t ts = 0;

int32_t undefs = 0;

uint32_t sz;

virtual ~Field() = default;

// Virtual methods for field operations

virtual Field& operator=(const Field& other) = 0;

virtual Field& operator+=(const Field& other) = 0;

virtual std::unique_ptr<Field> add(const Field& other) = 0;

virtual Field& operator-=(const Field& other) = 0;

virtual Field& operator*=(const Field& other) = 0;

virtual Field& operator/=(const Field& other) = 0;

virtual bool operator==(const Field&) const = 0;

virtual bool is_zero() const = 0;

virtual bool is_one() const = 0;

virtual void set_zero() = 0;

virtual void set_one() = 0;

virtual uint64_t bytes_used() const = 0;

virtual std::unique_ptr<Field> dup() const = 0;

virtual bool parse(const std::string& str, const uint32_t line_no) = 0;

// A method to display the value (for demonstration purposes)

virtual std::ostream& display(std::ostream& os) const = 0;

static void skip_whitespace(const std::string& str, uint32_t& at) {

char c = str[at];

while (c == '\t' || c == '\r' || c == ' ') {

at++;

c = str[at];

}

}

static mpz_class parse_sign(const std::string& str, uint32_t& at) {

mpz_class sign = 1;

if (str[at] == '-') {sign = -1; at++;}

else if (str[at] == '+') {sign = 1; at++;}

return sign;

}

static bool parse_int(mpz_class& ret, const std::string& str, uint32_t& at,

const size_t line_num, int* len = nullptr) {

mpz_class val = 0;

skip_whitespace(str, at);

char c = str[at];

if (c < '0' || c > '9') {

std::cerr

<< "PARSE ERROR! Unexpected char (dec: '" << c << ")"

<< " At line " << line_num

<< " we expected a number"

<< std::endl;

return false;

}

while (c >= '0' && c <= '9') {

if (len) (*len)++;

mpz_class val2 = val*10 + (c - '0');

if (val2 < val) {

std::cerr << "PARSE ERROR! At line " << line_num

<< " the variable number is to high"

<< std::endl;

return false;

}

val = val2;

c = str[++at];

}

ret = val;

return true;

}

static bool check_end_of_weight(const std::string& str, uint32_t& at, const uint32_t line_no) {

skip_whitespace(str, at);

if (str[at] != '0') {

std::cerr << "PARSE ERROR! expected 0 at the end of the weight."

<< "At line " << line_no

<< " -- did you forget to set the mode?" << std::endl;

return false;

}

at++;

skip_whitespace(str, at);

if (at < str.size() && str[at] != '\n') {

std::cerr << "PARSE ERROR! expected end of line at the end of the weight."

<< "At line " << line_no

<< " -- did you forget to set the mode?" << std::endl;

return false;

}

return true;

}

virtual ~FieldGen() = default;

virtual std::unique_ptr<Field> zero() const = 0;

virtual std::unique_ptr<Field> one() const = 0;

virtual std::unique_ptr<FieldGen> dup() const = 0;

virtual bool larger_than(const Field&, const Field&) const = 0;

virtual bool weighted() const = 0;

virtual bool exact() const = 0;

double val;

FDouble(const double _val) : val(_val) {}

FDouble(const FDouble& other) : val(other.val) {}

Field& operator=(const Field& other) final {

const auto& od = static_cast<const FDouble&>(other);

val = od.val;

return *this;

}

Field& operator+=(const Field& other) final {

const auto& od = static_cast<const FDouble&>(other);

val += od.val;

return *this;

}

std::unique_ptr<Field> add(const Field& other) final {

const auto& od = static_cast<const FDouble&>(other);

return std::make_unique<FDouble>(val + od.val);

}

Field& operator-=(const Field& other) final {

const auto& od = static_cast<const FDouble&>(other);

val -= od.val;

return *this;

}

Field& operator*=(const Field& other) final {

const auto& od = static_cast<const FDouble&>(other);

val *= od.val;

return *this;

}

Field& operator/=(const Field& other) final {

const auto& od = static_cast<const FDouble&>(other);

if (od.val == 0) throw std::runtime_error("Division by zero");

val /= od.val;

return *this;

}

bool operator==(const Field& other) const final {

const auto& od = static_cast<const FDouble&>(other);

return od.val == val;

}

std::ostream& display(std::ostream& os) const final {

os << val;

return os;

}

std::unique_ptr<Field> dup() const final {

return std::make_unique<FDouble>(val);

}

bool is_zero() const final { return val == 0; }

bool is_one() const final { return val == 1; }

void set_zero() final { val = 0; }

void set_one() final { val = 1; }

uint64_t bytes_used() const final { return sizeof(FDouble); }

bool parse(const std::string& str, const uint32_t line_no) final {

mpz_class head;

mpz_class mult;

uint32_t at = 0;

auto sign = parse_sign(str, at);

parse_int(head, str, at, line_no);

mpq_class vald;

if (str[at] == '.') {

at++;

mpz_class tail;

int len = 0;

if (!parse_int(tail, str, at, line_no, &len)) return false;

mpz_class ten(10);

mpz_ui_pow_ui(ten.get_mpz_t(), 10, len);

mpq_class tenq(ten);

mpq_class tailq(tail);

vald = head + tailq/tenq;

} else {

vald = head;

}

vald *= sign;

val = vald.get_d();

return check_end_of_weight(str, at, line_no);

}

~FGenDouble() final = default;

std::unique_ptr<Field> zero() const final {

return std::make_unique<FDouble>(0);

}

std::unique_ptr<Field> one() const final {

return std::make_unique<FDouble>(1.0);

}

std::unique_ptr<FieldGen> dup() const final {

return std::make_unique<FGenDouble>();

}

bool larger_than(const Field& a, const Field& b) const final {

const auto& ad = static_cast<const FDouble&>(a);

const auto& bd = static_cast<const FDouble&>(b);

return ad.val > bd.val;

}

bool weighted() const final { return true; }

bool exact() const final { return false; }