Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

CNF conversion refactoring #5547

Merged
merged 2 commits into from Sep 20, 2021
Merged

CNF conversion refactoring #5547

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3ec1a10
split sat2goal out of goal2sat
jameysharp Sep 13, 2021
52432c1
limit solver_core methods to those needed by goal2sat
jameysharp Sep 13, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions src/api/api_solver.cpp
View file
Open in desktop
Expand Up @@ -42,6 +42,7 @@ Revision History:
#include "sat/dimacs.h"
#include "sat/sat_solver.h"
#include "sat/tactic/goal2sat.h"
#include "sat/tactic/sat2goal.h"


extern "C" {
Expand Down
68 changes: 46 additions & 22 deletions src/sat/sat_solver.h
View file
Open in desktop
Expand Up @@ -244,12 +244,13 @@ namespace sat {
// Misc
//
// -----------------------
void updt_params(params_ref const & p) override;
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);

void collect_statistics(statistics & st) const override;
// collect statistics from sat solver
void collect_statistics(statistics & st) const;
void reset_statistics();
void display_status(std::ostream & out) const override;
void display_status(std::ostream & out) const;

/**
\brief Copy (non learned) clauses from src to this solver.
Expand Down Expand Up @@ -351,14 +352,19 @@ namespace sat {
//
// -----------------------
public:
bool inconsistent() const override { return m_inconsistent; }
unsigned num_vars() const override { return m_justification.size(); }
unsigned num_clauses() const override;
// is the state inconsistent?
bool inconsistent() const { return m_inconsistent; }

// number of variables and clauses
unsigned num_vars() const { return m_justification.size(); }
unsigned num_clauses() const;

void num_binary(unsigned& given, unsigned& learned) const;
unsigned num_restarts() const { return m_restarts; }
bool is_external(bool_var v) const override { return m_external[v]; }
bool is_external(bool_var v) const { return m_external[v]; }
bool is_external(literal l) const { return is_external(l.var()); }
void set_external(bool_var v) override;
void set_non_external(bool_var v) override;
void set_non_external(bool_var v);
bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
void set_eliminated(bool_var v, bool f) override;
bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
Expand All @@ -368,16 +374,14 @@ namespace sat {
unsigned scope_lvl() const { return m_scope_lvl; }
unsigned search_lvl() const { return m_search_lvl; }
bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
bool at_base_lvl() const override { return m_scope_lvl == 0; }
bool at_base_lvl() const { return m_scope_lvl == 0; }
lbool value(literal l) const { return m_assignment[l.index()]; }
lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
justification get_justification(literal l) const { return m_justification[l.var()]; }
justification get_justification(bool_var v) const { return m_justification[v]; }
unsigned lvl(bool_var v) const { return m_justification[v].level(); }
unsigned lvl(literal l) const { return m_justification[l.var()].level(); }
unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
unsigned trail_size() const { return m_trail.size(); }
literal trail_literal(unsigned i) const override { return m_trail[i]; }
literal scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
void assign(literal l, justification j) {
TRACE("sat_assign", tout << l << " previous value: " << value(l) << " j: " << j << "\n";);
Expand Down Expand Up @@ -430,7 +434,7 @@ namespace sat {
bool canceled() { return !m_rlimit.inc(); }
config const& get_config() const { return m_config; }
drat& get_drat() { return m_drat; }
drat* get_drat_ptr() override { return &m_drat; }
drat* get_drat_ptr() { return &m_drat; }
void set_incremental(bool b) { m_config.m_incremental = b; }
bool is_incremental() const { return m_config.m_incremental; }
extension* get_extension() const override { return m_ext.get(); }
Expand Down Expand Up @@ -472,15 +476,37 @@ namespace sat {
//
// -----------------------
public:
lbool check(unsigned num_lits = 0, literal const* lits = nullptr) override;
lbool check(unsigned num_lits = 0, literal const* lits = nullptr);

model const & get_model() const override { return m_model; }
// retrieve model if solver return sat
model const & get_model() const { return m_model; }
bool model_is_current() const { return m_model_is_current; }
literal_vector const& get_core() const override { return m_core; }

// retrieve core from assumptions
literal_vector const& get_core() const { return m_core; }

model_converter const & get_model_converter() const { return m_mc; }
void flush(model_converter& mc) override { mc.flush(m_mc); }

// The following methods are used when converting the state from the SAT solver back
// to a set of assertions.

// retrieve model converter that handles variable elimination and other transformations
void flush(model_converter& mc) { mc.flush(m_mc); }

// size of initial trail containing unit clauses
unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }

// literal at trail index i
literal trail_literal(unsigned i) const { return m_trail[i]; }

// collect n-ary clauses
clause_vector const& clauses() const { return m_clauses; }

// collect binary clauses
void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const;

void set_model(model const& mdl, bool is_current);
char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); }
char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
bool check_clauses(model const& m) const;
bool is_assumption(bool_var v) const;
void set_activity(bool_var v, unsigned act);
Expand Down Expand Up @@ -688,7 +714,7 @@ namespace sat {
public:
void user_push() override;
void user_pop(unsigned num_scopes) override;
void pop_to_base_level() override;
void pop_to_base_level();
unsigned num_user_scopes() const override { return m_user_scope_literals.size(); }
unsigned num_scopes() const override { return m_scopes.size(); }
reslimit& rlimit() { return m_rlimit; }
Expand Down Expand Up @@ -788,8 +814,6 @@ namespace sat {
clause * const * begin_learned() const { return m_learned.begin(); }
clause * const * end_learned() const { return m_learned.end(); }
clause_vector const& learned() const { return m_learned; }
clause_vector const& clauses() const override { return m_clauses; }
void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const override;


// -----------------------
Expand All @@ -798,11 +822,11 @@ namespace sat {
//
// -----------------------
public:
bool check_invariant() const override;
bool check_invariant() const;
void display(std::ostream & out) const;
void display_watches(std::ostream & out) const;
void display_watches(std::ostream & out, literal lit) const;
void display_dimacs(std::ostream & out) const override;
void display_dimacs(std::ostream & out) const;
std::ostream& display_model(std::ostream& out) const;
void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
void display_assignment(std::ostream & out) const;
Expand Down
1 change: 1 addition & 0 deletions src/sat/sat_solver/inc_sat_solver.cpp
View file
Open in desktop
Expand Up @@ -42,6 +42,7 @@ Module Name:
#include "sat/sat_params.hpp"
#include "sat/smt/euf_solver.h"
#include "sat/tactic/goal2sat.h"
#include "sat/tactic/sat2goal.h"
#include "sat/tactic/sat_tactic.h"
#include "sat/sat_simplifier_params.hpp"

Expand Down
61 changes: 1 addition & 60 deletions src/sat/sat_solver_core.h
View file
Open in desktop
Expand Up @@ -18,14 +18,13 @@ Revision History:
--*/
#pragma once


#include "sat/sat_model_converter.h"
#include "sat/sat_types.h"

namespace sat {

class cut_simplifier;
class extension;
class drat;

class solver_core {
protected:
Expand All @@ -34,27 +33,6 @@ namespace sat {
solver_core(reslimit& l) : m_rlimit(l) {}
virtual ~solver_core() {}

virtual void pop_to_base_level() {}
virtual bool at_base_lvl() const { return true; }

// retrieve model if solver return sat
virtual model const & get_model() const = 0;

// retrieve core from assumptions
virtual literal_vector const& get_core() const = 0;

// is the state inconsistent?
virtual bool inconsistent() const = 0;

// number of variables and clauses
virtual unsigned num_vars() const = 0;
virtual unsigned num_clauses() const = 0;

// check satisfiability
virtual lbool check(unsigned num_lits = 0, literal const* lits = nullptr) = 0;

virtual char const* get_reason_unknown() const { return "reason unavailable"; }

// add clauses
virtual void add_clause(unsigned n, literal* lits, status st) = 0;
void add_clause(literal l1, literal l2, status st) {
Expand All @@ -68,18 +46,7 @@ namespace sat {
// create boolean variable, tagged as external (= true) or internal (can be eliminated).
virtual bool_var add_var(bool ext) = 0;

// update parameters
virtual void updt_params(params_ref const& p) {}


virtual bool check_invariant() const { return true; }
virtual void display_status(std::ostream& out) const {}
virtual void display_dimacs(std::ostream& out) const {}

virtual bool is_external(bool_var v) const { return true; }
bool is_external(literal l) const { return is_external(l.var()); }
virtual void set_external(bool_var v) {}
virtual void set_non_external(bool_var v) {}
virtual void set_eliminated(bool_var v, bool f) {}
virtual void set_phase(literal l) { }

Expand All @@ -96,32 +63,6 @@ namespace sat {
virtual void set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); }

virtual cut_simplifier* get_cut_simplifier() { return nullptr; }

virtual drat* get_drat_ptr() { return nullptr; }


// The following methods are used when converting the state from the SAT solver back
// to a set of assertions.

// retrieve model converter that handles variable elimination and other transformations
virtual void flush(model_converter& mc) {}

// size of initial trail containing unit clauses
virtual unsigned init_trail_size() const = 0;

// literal at trail index i
virtual literal trail_literal(unsigned i) const = 0;

// collect n-ary clauses
virtual clause_vector const& clauses() const = 0;

// collect binary clauses
typedef std::pair<literal, literal> bin_clause;
virtual void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const = 0;

// collect statistics from sat solver
virtual void collect_statistics(statistics & st) const {}

};
};

35 changes: 35 additions & 0 deletions src/sat/smt/sat_internalizer.h
View file
Open in desktop
@@ -0,0 +1,35 @@
/*++
Copyright (c) 2020 Microsoft Corporation

Module Name:

sat_internalizer.h

Abstract:

Header for SMT theories over SAT solver

Author:

Nikolaj Bjorner (nbjorner) 2020-08-25

--*/
#pragma once

#include "util/sat_literal.h"

namespace sat {
class sat_internalizer {
public:
virtual ~sat_internalizer() {}
virtual bool is_bool_op(expr* e) const = 0;
virtual literal internalize(expr* e, bool learned) = 0;
virtual bool_var to_bool_var(expr* e) = 0;
virtual bool_var add_bool_var(expr* e) = 0;
virtual void cache(app* t, literal l) = 0;
virtual void uncache(literal l) = 0;
virtual void push() = 0;
virtual void pop(unsigned n) = 0;
virtual void set_expr2var_replay(obj_map<expr, sat::bool_var>* r) = 0;
};
}
15 changes: 1 addition & 14 deletions src/sat/smt/sat_smt.h
View file
Open in desktop
Expand Up @@ -19,6 +19,7 @@ Module Name:
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "sat/sat_solver.h"
#include "sat/smt/sat_internalizer.h"

namespace sat {

Expand All @@ -28,20 +29,6 @@ namespace sat {
eframe(expr* e) : m_e(e), m_idx(0) {}
};

class sat_internalizer {
public:
virtual ~sat_internalizer() {}
virtual bool is_bool_op(expr* e) const = 0;
virtual literal internalize(expr* e, bool learned) = 0;
virtual bool_var to_bool_var(expr* e) = 0;
virtual bool_var add_bool_var(expr* e) = 0;
virtual void cache(app* t, literal l) = 0;
virtual void uncache(literal l) = 0;
virtual void push() = 0;
virtual void pop(unsigned n) = 0;
virtual void set_expr2var_replay(obj_map<expr, sat::bool_var>* r) = 0;
};

class constraint_base {
extension* m_ex;
unsigned m_mem[0];
Expand Down
1 change: 1 addition & 0 deletions src/sat/tactic/CMakeLists.txt
View file
Open in desktop
@@ -1,6 +1,7 @@
z3_add_component(sat_tactic
SOURCES
goal2sat.cpp
sat2goal.cpp
sat_tactic.cpp
COMPONENT_DEPENDENCIES
sat
Expand Down