mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

remove opt dependency

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-25 18:18:19 -08:00
parent 46f3b7374c
commit d9b4f237fe
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/qe/qe_mbi.cpp
View file

@ -38,7 +38,7 @@ Notes:
#include "qe/qe_mbi.h" #include "qe/qe_mbi.h"
#include "qe/qe_term_graph.h" #include "qe/qe_term_graph.h"
#include "qe/qe_arith.h" #include "qe/qe_arith.h"
#include "opt/opt_context.h" // include "opt/opt_context.h"
namespace qe { namespace qe {
@ -339,6 +339,7 @@ namespace qe {
} }
void euf_arith_mbi_plugin::minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies) { void euf_arith_mbi_plugin::minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies) {
#if 0
arith_util a(m); arith_util a(m);
opt::context opt(m); opt::context opt(m);
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
@ -366,6 +367,7 @@ namespace qe {
opt.get_model(mdl); opt.get_model(mdl);
model_evaluator mev(*mdl.get()); model_evaluator mev(*mdl.get());
std::cout << mev(t) << "\n"; std::cout << mev(t) << "\n";
#endif
} }
/** /**