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

add synth_solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-12 20:31:15 -07:00
parent 31677a0570
commit 8e16acce19
2 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -96,14 +96,12 @@ namespace synth {
}
sat::check_result solver::check() {
// TODO: need to know if there are quantifiers to instantiate
if (m_solved.size() < m_synth.size()) {
IF_VERBOSE(2, ctx.display(verbose_stream()));
if (m_synth.empty())
return sat::check_result::CR_DONE;
}
if (!compute_solutions())
return sat::check_result::CR_GIVEUP;
return sat::check_result::CR_CONTINUE;
SASSERT(m_solved.size() < m_synth.size());
IF_VERBOSE(2, ctx.display(verbose_stream()));
return sat::check_result::CR_GIVEUP;
}
// display current state (eg. current set of realizers)
@ -118,6 +116,13 @@ namespace synth {
return alloc(solver, ctx);
}
void solver::asserted(sat::literal lit) {
// lit corresponds to a Boolean output variable.
// it is asserted.
// assume that we attach this theory to such Boolean output variables.
}
void solver::on_merge_eh(euf::enode* root, euf::enode* other) {
auto is_computable = [&](euf::enode* n) { return !contains_uncomputable(n->get_expr()) || m_is_computable.get(n->get_root_id(), false); };

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

@ -24,7 +24,7 @@ namespace synth {
public:
solver(euf::solver& ctx);
~solver() override;
void asserted(sat::literal lit) override {}
void asserted(sat::literal lit) override;
sat::check_result check() override;
void push_core() override {}
void pop_core(unsigned n) override {}