mirror of
https://github.com/Z3Prover/z3
synced 2025-04-11 11:43:36 +00:00
75 lines
2.5 KiB
C++
75 lines
2.5 KiB
C++
/*++
|
|
Copyright (c) 2020 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_xor_finder.h
|
|
|
|
Abstract:
|
|
|
|
xor finder
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner 2020-01-02
|
|
|
|
Notes:
|
|
|
|
Based on xor extraction paper by Meel & Soos, AAAI 2018.
|
|
|
|
--*/
|
|
|
|
#pragma once
|
|
|
|
#include "util/params.h"
|
|
#include "util/statistics.h"
|
|
#include "sat/sat_clause.h"
|
|
#include "sat/sat_types.h"
|
|
#include "sat/sat_solver.h"
|
|
|
|
namespace sat {
|
|
|
|
class xor_finder {
|
|
solver& s;
|
|
struct clause_filter {
|
|
unsigned m_filter;
|
|
clause* m_clause;
|
|
clause_filter(unsigned f, clause* cp):
|
|
m_filter(f), m_clause(cp) {}
|
|
};
|
|
unsigned m_max_xor_size;
|
|
vector<svector<clause_filter>> m_clause_filters; // index of clauses.
|
|
unsigned m_combination; // bit-mask of parities that have been found
|
|
vector<bool_vector> m_parity; // lookup parity for clauses
|
|
clause_vector m_clauses_to_remove; // remove clauses that become xors
|
|
unsigned_vector m_var_position; // position of var in main clause
|
|
literal_vector m_clause; // reference clause with literals sorted according to main clause
|
|
unsigned_vector m_missing; // set of indices not occurring in clause.
|
|
clause_vector m_removed_clauses;
|
|
std::function<void (literal_vector const& lits)> m_on_xor;
|
|
|
|
void set_combination(unsigned mask);
|
|
inline bool get_combination(unsigned mask) const { return (m_combination & (1 << mask)) != 0; }
|
|
void extract_xor(clause& c);
|
|
void add_xor(bool parity, clause& c);
|
|
bool extract_xor(bool parity, clause& c, literal l1, literal l2);
|
|
bool extract_xor(bool parity, clause& c, clause& c2);
|
|
bool update_combinations(clause& c, bool parity, unsigned mask);
|
|
void init_parity();
|
|
void init_clause_filter();
|
|
void init_clause_filter(clause_vector& clauses);
|
|
unsigned get_clause_filter(clause& c);
|
|
|
|
public:
|
|
xor_finder(solver& s) : s(s), m_max_xor_size(5) { init_parity(); }
|
|
|
|
void set(std::function<void (literal_vector const& lits)>& f) { m_on_xor = f; }
|
|
|
|
bool parity(unsigned i, unsigned j) const { return m_parity[i][j]; }
|
|
unsigned max_xor_size() const { return m_max_xor_size; }
|
|
|
|
void operator()(clause_vector& clauses);
|
|
clause_vector const& removed_clauses() const { return m_removed_clauses; }
|
|
};
|
|
}
|