From 0bfd24aae90d48ca0c9cce66038be19598b09f15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Jul 2021 12:05:52 +0200 Subject: [PATCH] add comments --- src/sat/smt/q_model_fixer.cpp | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 86c502932..c2defc71a 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -141,6 +141,19 @@ namespace q { mdl.register_decl(f_new, fi); } + /* + * For function f(...,t_idx, ..) collect the values of terms at position idx of f + * as "values". + * Map t_idx |-> mdl(t_idx) + * and mdl(t_idx) |-> t_idx + * Sort the values as [v_1, v_2, ..., v_n] with corresponding terms + * [t_1, t_2, ..., t_n] + * + * Create the term if p(x) = if x <= v_1 then t_1 else if x <= v_2 then t_2 else ... t_n + * where p is a fresh function + * and return p(x) + */ + expr_ref model_fixer::add_projection_function(model& mdl, func_decl* f, unsigned idx) { sort* srt = f->get_domain(idx); projection_function* proj = get_projection(srt); @@ -230,6 +243,15 @@ namespace q { return value; } + /** + * We are given a term f(...,arg_i,..) and value = mdl(arg_i) + * Create + * 1 the bounds t_j <= arg_i < t_{j+1} where + * v_j <= value < v_{j+1} for the corresponding values of t_j, t_{j+1} + * 2 or the bound arg_i < t_0 if value < v_0 + * 3 or the bound arg_i >= t_last if value > v_last + */ + void model_fixer::invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) { TRACE("q", tout << "invert-arg " << mk_pp(t, m) << " " << i << " " << mk_pp(value, m) << "\n";); auto const* md = get_projection_data(t->get_decl(), i);