mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

clean up header/cpp division

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-08 20:08:27 -07:00
parent f4a6c0df3e
commit 90780576f1
2 changed files with 12 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/sat/smt/synth_solver.cpp
View file

@ -23,13 +23,6 @@ namespace synth {
solver::~solver() {}
// recognize synthesis objective as part of search objective.
// register it for calls to check.
void solver::asserted(sat::literal lit) {
}
bool solver::synthesize(app* e) {
if (e->get_num_args() == 0)
@ -83,27 +76,6 @@ namespace synth {
return sat::check_result::CR_DONE;
}
// nothing particular to do
void solver::push_core() {
}
// nothing particular to do
void solver::pop_core(unsigned n) {
}
// nothing particular to do
bool solver::unit_propagate() {
return false;
}
// retrieve explanation for assertions made by synth solver. It only asserts unit literals so nothing to retrieve
void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) {
}
// where we collect statistics (number of invocations?)
void solver::collect_statistics(statistics& st) const {}
// recognize synthesis objectives here.
sat::literal solver::internalize(expr* e, bool sign, bool root) {
internalize(e);
@ -126,22 +98,14 @@ namespace synth {
// display current state (eg. current set of realizers)
std::ostream& solver::display(std::ostream& out) const {
for (auto * e : m_synth)
out << "synth objective " << mk_pp(e, m) << "\n";
return out;
}
// justified by "synth".
std::ostream& solver::display_justification(std::ostream& out, sat::ext_justification_idx idx) const {
return out << "synth";
}
std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
return out << "synth";
}
// create a clone of the solver.
euf::th_solver* solver::clone(euf::solver& ctx) {
NOT_IMPLEMENTED_YET();
return nullptr;
return alloc(solver, ctx);
}
}

23
src/sat/smt/synth_solver.h
View file

@ -21,26 +21,21 @@ Author:
namespace synth {
class solver : public euf::th_euf_solver {
public:
solver(euf::solver& ctx);
~solver() override;
void asserted(sat::literal lit) override;
~solver() override;
void asserted(sat::literal lit) override {}
sat::check_result check() override;
void push_core() override;
void pop_core(unsigned n) override;
bool unit_propagate() override;
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override;
void collect_statistics(statistics& st) const override;
void push_core() override {}
void pop_core(unsigned n) override {}
bool unit_propagate() override { return false; }
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override {}
void collect_statistics(statistics& st) const override {}
sat::literal internalize(expr* e, bool sign, bool root) override;
void internalize(expr* e) override;
std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override;
std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { return out << "synth"; }
std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { return out << "synth"; }
euf::th_solver* clone(euf::solver& ctx) override;
private: