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

init

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-14 22:38:29 -07:00
parent 6733a8a5dd
commit 4d48dba1e3
1 changed files with 24 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -409,6 +409,30 @@ namespace synth {
}
bool solver::synthesize_arithmetic(synth_objective& obj) {
arith_util a(m);
if (!a.is_int_real(obj.output()))
return false;
verbose_stream() << "int-real-objective\n";
#if 0
// 1 retrieve a model
// 1.5 - difference cert?
// 1.6 - split arith?
// 2 retrieve literal dependencies
// 3 split_arith, arith_vars, rpoejct, project_euf,
// produce projection
add_dcert(mdl, lits);
expr_ref_vector alits(m), uflits(m);
split_arith(lits, alits, uflits);
auto avars = get_arith_vars(lits);
vector<mbp::def> defs = arith_project(mdl, avars, alits);
for (auto const& d : defs) uflits.push_back(m.mk_eq(d.var, d.term));
TRACE("qe", tout << "uflits: " << uflits << "\n";);
project_euf(mdl, uflits);
lits.reset();
lits.append(alits);
lits.append(uflits);
#endif
return false;
}