mirror of
https://github.com/Z3Prover/z3
synced 2025-08-23 03:27:52 +00:00
77 lines
1.9 KiB
C++
77 lines
1.9 KiB
C++
/*++
|
|
Copyright (c) 2020 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
sat_dual_solver.h
|
|
|
|
Abstract:
|
|
|
|
Solver for obtaining implicant.
|
|
Based on an idea by Armin Biere to use dual propagation
|
|
for representation of negated goal.
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2020-08-25
|
|
|
|
--*/
|
|
#pragma once
|
|
#include "util/lim_vector.h"
|
|
#include "sat/sat_solver.h"
|
|
|
|
namespace sat {
|
|
|
|
class dual_solver {
|
|
struct no_drat_params : public params_ref {
|
|
no_drat_params();
|
|
};
|
|
no_drat_params m_params;
|
|
solver m_solver;
|
|
lim_svector<literal> m_units, m_roots;
|
|
lim_svector<bool_var> m_tracked_vars;
|
|
literal_vector m_lits, m_core;
|
|
bool_var_vector m_is_tracked;
|
|
unsigned_vector m_ext2var;
|
|
unsigned_vector m_var2ext;
|
|
lim_svector<unsigned> m_vars;
|
|
void add_literal(literal lit);
|
|
|
|
bool_var ext2var(bool_var v);
|
|
bool_var var2ext(bool_var v);
|
|
literal ext2lit(literal lit);
|
|
literal lit2ext(literal lit);
|
|
|
|
void add_assumptions(solver const& s);
|
|
|
|
std::ostream& display(solver const& s, std::ostream& out) const;
|
|
|
|
public:
|
|
dual_solver(reslimit& l);
|
|
void push();
|
|
void pop(unsigned num_scopes);
|
|
|
|
/*
|
|
* track model relevancy for variable
|
|
*/
|
|
void track_relevancy(bool_var v);
|
|
|
|
/*
|
|
* Add a root clause from the input problem.
|
|
* At least one literal has to be satisfied in every root.
|
|
*/
|
|
void add_root(unsigned sz, literal const* clause);
|
|
|
|
/*
|
|
* Add auxiliary clauses that originate from compiling definitions.
|
|
*/
|
|
void add_aux(unsigned sz, literal const* clause);
|
|
|
|
/*
|
|
* Extract a minimized subset of relevant literals from a model for s.
|
|
*/
|
|
bool operator()(solver const& s);
|
|
|
|
literal_vector const& core() const { return m_core; }
|
|
};
|
|
}
|