mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 03:16:17 +00:00
Code Activity

fix #6121

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-30 19:47:26 -07:00
parent c3d2120bdd
commit 959a0ba370
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ackermannization/lackr_model_constructor.cpp
View file

@ -21,6 +21,7 @@
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
#include "ast/rewriter/bv_rewriter.h" #include "ast/rewriter/bv_rewriter.h"
#include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/bool_rewriter.h"
#include <iostream>
struct lackr_model_constructor::imp { struct lackr_model_constructor::imp {
public: public:
@ -186,7 +187,7 @@ private:
return m_app2val.find(a, val); return m_app2val.find(a, val);
} }
bool evaluate(app * const a, expr_ref& result) { bool evaluate(app * a, expr_ref& result) {
SASSERT(!is_val(a)); SASSERT(!is_val(a));
const unsigned num = a->get_num_args(); const unsigned num = a->get_num_args();
if (num == 0) { // handle constants if (num == 0) { // handle constants
@ -232,20 +233,20 @@ private:
// Check and record the value for a given term, given that all arguments are already checked. // Check and record the value for a given term, given that all arguments are already checked.
// //
bool mk_value(app * a) { bool mk_value(app * a) {
if (is_val(a)) return true; // skip numerals if (is_val(a))
return true; // skip numerals
TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m, 2) << ")\n";); TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m, 2) << ")\n";);
SASSERT(!m_app2val.contains(a)); SASSERT(!m_app2val.contains(a));
expr_ref result(m); expr_ref result(m);
if (!evaluate(a, result)) return false; if (!evaluate(a, result))
SASSERT(is_val(result)); return false;
TRACE("model_constructor", TRACE("model_constructor",
tout << "map term(\n" << mk_ismt2_pp(a, m, 2) << "\n->" tout << "map term(\n" << mk_ismt2_pp(a, m, 2) << "\n->"
<< mk_ismt2_pp(result.get(), m, 2)<< ")\n"; ); << mk_ismt2_pp(result.get(), m, 2)<< ")\n"; );
CTRACE("model_constructor", CTRACE("model_constructor",
!is_val(result.get()), !is_val(result.get()),
tout << "eval fail\n" << mk_ismt2_pp(a, m, 2) << mk_ismt2_pp(result, m, 2) << "\n"; tout << "eval didn't create a constant \n" << mk_ismt2_pp(a, m, 2) << " " << mk_ismt2_pp(result, m, 2) << "\n";
); );
SASSERT(is_val(result.get()));
m_app2val.insert(a, result.get()); // memoize m_app2val.insert(a, result.get()); // memoize
m_pinned.push_back(a); m_pinned.push_back(a);
m_pinned.push_back(result); m_pinned.push_back(result);