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

prepare for arithmetic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-14 22:21:43 -07:00
parent 2481e6b910
commit 6733a8a5dd
2 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -19,6 +19,9 @@ Author:
#include "ast/rewriter/th_rewriter.h"
#include "sat/smt/synth_solver.h"
#include "sat/smt/euf_solver.h"
#include "qe/mbp/mbp_term_graph.h"
#include "qe/mbp/mbp_arith.h"
#include "qe/mbp/mbp_arrays.h"
namespace synth {
@ -90,10 +93,13 @@ namespace synth {
expr* arg = nullptr;
if (util.is_synthesiz3(e))
add_synth_objective(synth_objective(m, a));
if (util.is_grammar(e))
else if (util.is_grammar(e))
add_uncomputable(a);
if (util.is_specification(e, arg))
else if (util.is_specification(e, arg))
add_specification(a, arg);
else {
IF_VERBOSE(0, verbose_stream() << "unrecognized synthesis objective " << mk_pp(e, m) << "\n");
}
}
sat::check_result solver::check() {
@ -103,8 +109,9 @@ namespace synth {
for (auto& s : m_synth) {
if (s.is_solved())
continue;
if (m.is_uninterp(s.output()->get_sort()) &&
synthesize_uninterpreted_sort(s))
if (synthesize_uninterpreted_sort(s))
continue;
if (synthesize_arithmetic(s))
continue;
IF_VERBOSE(2, ctx.display(verbose_stream()));
return sat::check_result::CR_GIVEUP;
@ -359,6 +366,9 @@ namespace synth {
}
bool solver::synthesize_uninterpreted_sort(synth_objective& obj) {
if (!m.is_uninterp(obj.output()->get_sort()))
return false;
sort* srt = obj.output()->get_sort();
euf::enode* r = expr2enode(obj.output());
VERIFY(r);
@ -398,4 +408,9 @@ namespace synth {
return false;
}
bool solver::synthesize_arithmetic(synth_objective& obj) {
return false;
}
}

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

@ -75,6 +75,7 @@ namespace synth {
void compute_rep();
bool synthesize_uninterpreted_sort(synth_objective& obj);
bool synthesize_arithmetic(synth_objective& obj);
expr* get_rep(euf::enode* n) { return m_rep.get(n->get_root_id(), nullptr); };
bool has_rep(euf::enode* n) { return !!get_rep(n); };