mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge pull request #1686 from agurfinkel/deep_space

Browse source 
switching spacer to new model api
This commit is contained in:
Nikolaj Bjorner 2018-06-17 09:40:13 -07:00 • committed by GitHub
commit 6bc14afa5e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 299 additions and 409 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/api/api_qe.cpp
View file

@ -52,7 +52,7 @@ extern "C"
Z3_TRY;
LOG_Z3_qe_model_project (c, m, num_bounds, bound, body);
RESET_ERROR_CODE();
app_ref_vector vars(mk_c(c)->m ());
if (!to_apps(num_bounds, bound, vars)) {
SET_ERROR_CODE (Z3_INVALID_ARG);
@ -62,7 +62,7 @@ extern "C"
expr_ref result (mk_c(c)->m ());
result = to_expr (body);
model_ref model (to_model_ref (m));
spacer::qe_project (mk_c(c)->m (), vars, result, model);
spacer::qe_project (mk_c(c)->m (), vars, result, *model);
mk_c(c)->save_ast_trail (result.get ());
return of_expr (result.get ());
@ -119,11 +119,8 @@ extern "C"
facts.push_back (to_expr (fml));
flatten_and (facts);
spacer::model_evaluator_util mev (mk_c(c)->m());
mev.set_model (*model);
expr_ref_vector lits (mk_c(c)->m());
spacer::compute_implicant_literals (mev, facts, lits);
spacer::compute_implicant_literals (*model, facts, lits);
expr_ref result (mk_c(c)->m ());
result = mk_and (lits);