mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fixing build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-03 22:08:21 -07:00
parent e8112a6564
commit 626380b3c7
2 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/simplifiers/model_reconstruction_trail.cpp
View file

@ -12,6 +12,7 @@ Author:
--*/
#include "ast/for_each_expr.h"
#include "ast/simplifiers/model_reconstruction_trail.h"
#include "ast/converters/generic_model_converter.h"
@ -20,9 +21,9 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
// accumulate a set of dependent exprs, updating m_trail to exclude loose
// substitutions that use variables from the dependent expressions.
ast_mark free_vars;
auto [f, dep] = d;
auto [f, dep] = d();
for (expr* t : subterms::all(expr_ref(f, m)))
free_vars.mark(t);
free_vars.mark(t, true);
NOT_IMPLEMENTED_YET();
}
@ -32,7 +33,7 @@ void model_reconstruction_trail::replay(dependent_expr const& d, vector<dependen
*/
model_converter_ref model_reconstruction_trail::get_model_converter() {
model_converter_ref mc = alloc(generic_model_converter, m, "dependent-expr-model");
// walk the trail from the back.
// walk the trail from the back
// add substitutions from the back to the generic model converter
// after they have been normalized using a global replace that replaces
// substituted variables by their terms.

2
src/test/horn_subsume_model_converter.cpp
View file

@ -5,7 +5,7 @@ Copyright (c) 2015 Microsoft Corporation
--*/
#include "tactic/horn_subsume_model_converter.h"
#include "ast/converters/horn_subsume_model_converter.h"
#include "ast/arith_decl_plugin.h"
#include "model/model_smt2_pp.h"
#include "ast/reg_decl_plugins.h"