From 3c761b4c882d3ecfc76fccfc757344ce6bfc7a85 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Fri, 31 Jan 2025 19:32:07 +0100 Subject: [PATCH 1/5] ADT fix: found the issue and initial ideas on how to fix it --- include/ae/SMTUtils.hpp | 3 +- include/deep/NonlinCHCsolver.hpp | 2 +- include/ufo/Smt/Z3n.hpp | 5 +- include/ufo/Smt/ZExprConverter.hpp | 137 +++++++++++++++++------------ tools/nonlin/NonlinSolver.cpp | 5 ++ 5 files changed, 90 insertions(+), 62 deletions(-) diff --git a/include/ae/SMTUtils.hpp b/include/ae/SMTUtils.hpp index 4e4a14ecd..7e2099e63 100644 --- a/include/ae/SMTUtils.hpp +++ b/include/ae/SMTUtils.hpp @@ -42,12 +42,13 @@ namespace ufo ; } - SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, std::vector adts, std::vector adts_seen) : + SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, std::vector adts, std::vector adts_seen, std::map> constructors) : efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL) { z3.adts = adts; z3.adts_seen = adts_seen; + z3.constructors = constructors; for(auto b : _accessors) if (b->arity() == 3) accessors.insert(b); diff --git a/include/deep/NonlinCHCsolver.hpp b/include/deep/NonlinCHCsolver.hpp index fbe56988d..82ff5e2ab 100644 --- a/include/deep/NonlinCHCsolver.hpp +++ b/include/deep/NonlinCHCsolver.hpp @@ -71,7 +71,7 @@ namespace ufo NonlinCHCsolver(CHCs &r, map>> & s) : m_efac(r.m_efac), ruleManager(r), - u(m_efac, r.m_z3.getAdtAccessors(), 10000, r.m_z3.adts, r.m_z3.adts_seen), signature(s) {} + u(m_efac, r.m_z3.getAdtAccessors(), 10000, r.m_z3.adts, r.m_z3.adts_seen, r.m_z3.constructors), signature(s) {} bool checkAllOver(bool checkQuery = false) { for (auto &hr: ruleManager.chcs) { diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp index f5ecfd222..539f20f40 100644 --- a/include/ufo/Smt/Z3n.hpp +++ b/include/ufo/Smt/Z3n.hpp @@ -286,6 +286,7 @@ namespace ufo public: std::vector adts; std::vector adts_seen; + std::map> constructors; protected: z3::context &get_ctx () { return ctx; } @@ -294,14 +295,14 @@ namespace ufo expr_ast_map seen_expr; z3::ast toAst (Expr e) { - return M::marshal (e, get_ctx (), cache.left, seen_expr, adts, adts_seen); + return M::marshal (e, get_ctx (), cache.left, seen_expr, adts, adts_seen, constructors); } Expr toExpr (z3::ast a) { if (!a) return Expr(); // ast_expr_map seen; - auto res = U::unmarshal (a, get_efac (), cache.right, seen_ast, adts_seen, adts, accessors); + auto res = U::unmarshal (a, get_efac (), cache.right, seen_ast, adts_seen, adts, accessors, constructors); return res; } diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index eee0daf73..def978c33 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -42,7 +42,7 @@ namespace ufo { template static z3::ast marshal (Expr e, z3::context &ctx, - C &cache, expr_ast_map &seen, std::vector adts, std::vector &adts_seen) + C &cache, expr_ast_map &seen, std::vector adts, std::vector &adts_seen, std::map> &constructors) { assert (e); if (isOpX(e)) return z3::ast (ctx, Z3_mk_true (ctx)); @@ -65,25 +65,38 @@ namespace ufo if (bind::isBVar (e)) { - z3::ast sort (marshal (bind::type (e), ctx, cache, seen, adts, adts_seen)); + z3::ast sort (marshal (bind::type (e), ctx, cache, seen, adts, adts_seen, constructors)); res = Z3_mk_bound (ctx, bind::bvarId (e), reinterpret_cast (static_cast (sort))); } - else if (isOpX (e)) - res = reinterpret_cast (Z3_mk_int_sort (ctx)); + else if (isOpX (e)) { + res = reinterpret_cast (Z3_mk_int_sort(ctx)); + printf("Post reinterpret: %s\n", Z3_ast_to_string(ctx, res)); + } else if (isOpX (e)) res = reinterpret_cast (Z3_mk_real_sort(ctx)); else if (isOpX (e)) res = reinterpret_cast (Z3_mk_bool_sort (ctx)); else if (isOpX (e)) { - res = reinterpret_cast (Z3_mk_int_sort (ctx)); -// res = reinterpret_cast (Z3_mk_datatype_sort(ctx, Z3_mk_string_symbol(ctx, lexical_cast(e->left ()).c_str()))); +// res = reinterpret_cast (Z3_mk_int_sort (ctx)); + std::string name = lexical_cast(e->left()); + Z3_symbol z3_name = Z3_mk_string_symbol(ctx, name.c_str()); + Z3_func_decl csts [constructors[name].size()]; + for(int i = 0; i (typeDt); +// auto kind = Z3_get_sort_kind(ctx, typeDt); + auto consts = Z3_get_datatype_sort_num_constructors(ctx, typeDt); + printf("Post reinterpret: %s\n", Z3_ast_to_string(ctx, res)); }// GF: hack for now else if (isOpX (e)) { - z3::ast _idx_sort (marshal (e->left (), ctx, cache, seen, adts, adts_seen)); - z3::ast _val_sort (marshal (e->right (), ctx, cache, seen, adts, adts_seen)); + z3::ast _idx_sort (marshal (e->left (), ctx, cache, seen, adts, adts_seen, constructors)); + z3::ast _val_sort (marshal (e->right (), ctx, cache, seen, adts, adts_seen, constructors)); Z3_sort idx_sort = reinterpret_cast (static_cast (_idx_sort)); Z3_sort val_sort = reinterpret_cast @@ -178,7 +191,7 @@ namespace ufo for (size_t i = 0; i < bind::domainSz (e); ++i) { - z3::ast a (marshal (bind::domainTy (e, i), ctx, cache, seen, adts, adts_seen)); + z3::ast a (marshal (bind::domainTy (e, i), ctx, cache, seen, adts, adts_seen, constructors)); pinned.push_back (a); domain [i] = reinterpret_cast (static_cast(a)); } @@ -187,7 +200,7 @@ namespace ufo z3::sort range (ctx, reinterpret_cast (static_cast - (marshal (bind::rangeTy (e), ctx, cache, seen, adts, adts_seen)))); + (marshal (bind::rangeTy (e), ctx, cache, seen, adts, adts_seen, constructors)))); Expr fname = bind::fname (e); @@ -213,7 +226,7 @@ namespace ufo z3::func_decl zfdecl (ctx, reinterpret_cast (static_cast - (marshal (bind::fname (e), ctx, cache, seen, adts, adts_seen)))); + (marshal (bind::fname (e), ctx, cache, seen, adts, adts_seen, constructors)))); // -- marshall all arguments except for the first one // -- (which is the fdecl) std::vector args (e->arity ()); @@ -224,7 +237,7 @@ namespace ufo for (ENode::args_iterator it = ++ (e->args_begin ()), end = e->args_end (); it != end; ++it) { - z3::ast a (marshal (*it, ctx, cache, seen, adts, adts_seen)); + z3::ast a (marshal (*it, ctx, cache, seen, adts, adts_seen, constructors)); pinned_args.push_back (a); args [pos++] = a; } @@ -239,11 +252,11 @@ namespace ufo for (int i = 0; i < e->arity() - 1; i++) vars.push_back(bind::fapp(e->arg(i))); - z3::ast ast (marshal (e->last(), ctx, cache, seen, adts, adts_seen)); //z3.toAst (e->last())); + z3::ast ast (marshal (e->last(), ctx, cache, seen, adts, adts_seen, constructors)); //z3.toAst (e->last())); std::vector bound; bound.reserve (boost::size (vars)); for (const Expr &v : vars) - bound.push_back (Z3_to_app (ctx, marshal (v, ctx, cache, seen, adts, adts_seen))); + bound.push_back (Z3_to_app (ctx, marshal (v, ctx, cache, seen, adts, adts_seen, constructors))); if (isOpX (e)) res = Z3_mk_forall_const (ctx, 0, @@ -272,49 +285,49 @@ namespace ufo // -- then it's a NEG or UN_MINUS if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); return z3::ast (ctx, Z3_mk_unary_minus(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); return z3::ast (ctx, Z3_mk_not(ctx, arg)); } if (isOpX (e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); return z3::ast (ctx, Z3_mk_array_default (ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); return z3::ast (ctx, Z3_mk_bvnot(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); return z3::ast (ctx, Z3_mk_bvneg(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); return z3::ast (ctx, Z3_mk_bvredand(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); return z3::ast (ctx, Z3_mk_bvredor(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); //TODO: SECOND NUMBER IS THE AMOUNT OF BITS IN THE BV ENCODING return z3::ast (ctx, Z3_mk_int2bv(ctx, 64, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen); + z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); //TODO: BOOL DESCRIBES IF NUMBER IS UNSIGNED OR NOT return z3::ast (ctx, Z3_mk_bv2int(ctx, arg, true)); } @@ -323,8 +336,8 @@ namespace ufo } else if (arity == 2) { - z3::ast t1 = marshal(e->left(), ctx, cache, seen, adts, adts_seen); - z3::ast t2 = marshal(e->right(), ctx, cache, seen, adts, adts_seen); + z3::ast t1 = marshal(e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast t2 = marshal(e->right(), ctx, cache, seen, adts, adts_seen, constructors); Z3_ast args [2] = {t1, t2}; @@ -458,7 +471,7 @@ namespace ufo else if (isOpX (e)) { assert (bv::high (e) > bv::low (e)); - z3::ast a (ctx, marshal (bv::earg (e), ctx, cache, seen, adts, adts_seen)); + z3::ast a (ctx, marshal (bv::earg (e), ctx, cache, seen, adts, adts_seen, constructors)); res = Z3_mk_extract (ctx, bv::high (e), bv::low (e), a); } else if (isOpX (e) || isOpX (e) || @@ -473,7 +486,7 @@ namespace ufo for (ENode::args_iterator it = e->args_begin(), end = e->args_end(); it != end; ++it) { - z3::ast a = z3::ast (ctx, marshal (*it, ctx, cache, seen, adts, adts_seen)); + z3::ast a = z3::ast (ctx, marshal (*it, ctx, cache, seen, adts, adts_seen, constructors)); args.push_back (a); pinned.push_back (a); } @@ -526,7 +539,7 @@ namespace ufo template static Expr unmarshal (const z3::ast &z, ExprFactory &efac, C &cache, ast_expr_map &seen, - std::vector &adts_seen, std::vector &adts, std::vector &accessors) + std::vector &adts_seen, std::vector &adts, std::vector &accessors, std::map> &constructors) { z3::context &ctx = z.ctx (); @@ -572,31 +585,39 @@ namespace ufo case Z3_BV_SORT: return bv::bvsort (Z3_get_bv_sort_size (ctx, sort), efac); case Z3_ARRAY_SORT: - domain = - unmarshal (z3::ast (ctx, - Z3_sort_to_ast + domain = + unmarshal (z3::ast (ctx, + Z3_sort_to_ast (ctx, Z3_get_array_sort_domain (ctx, sort))), - efac, cache, seen, adts_seen, adts, accessors); - range = + efac, cache, seen, adts_seen, adts, accessors, constructors); + range = unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, Z3_get_array_sort_range (ctx, sort))), - efac, cache, seen, adts_seen, adts, accessors); + efac, cache, seen, adts_seen, adts, accessors, constructors); return sort::arrayTy (domain, range); case Z3_DATATYPE_SORT: { unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort); + std::vector dt_constructors; + std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)); while (num > 0) { num--; auto c = Z3_get_datatype_sort_constructor(ctx, sort, num); + dt_constructors.push_back(c); unsigned num_accessors = Z3_get_domain_size(ctx, c); + Z3_Constructor const = Z3_mk_constructor(ctx, + Z3_get_sort_name(ctx, sort), + Z3_get_decl_name(ctx, c), + Z3_get_arity(ctx, c), + ) while(num_accessors > 0){ num_accessors--; auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); } } - std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)); + constructors.insert({name, dt_constructors}); Expr adt_name = mkTerm (name, efac); if (find(adts_seen.begin(), adts_seen.end(), name) == adts_seen.end()) { @@ -605,7 +626,7 @@ namespace ufo { Z3_func_decl decl = Z3_get_datatype_sort_constructor(ctx, sort, i); Z3_ast zdecl = Z3_func_decl_to_ast(ctx, decl); - adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts, accessors)); + adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts, accessors, constructors)); } } @@ -625,7 +646,7 @@ namespace ufo { unsigned idx = Z3_get_index_value (ctx, z); z3::ast zsort (ctx, Z3_sort_to_ast (ctx, Z3_get_sort (ctx, z))); - Expr sort = unmarshal (zsort, efac, cache, seen, adts_seen, adts, accessors); + Expr sort = unmarshal (zsort, efac, cache, seen, adts_seen, adts, accessors, constructors); return bind::bvar (idx, sort); } @@ -656,13 +677,13 @@ namespace ufo { Z3_sort sort = Z3_get_domain (ctx, fdecl, p); type.push_back(unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); } type.push_back(unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, Z3_get_range (ctx, fdecl))), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); return bind::fdecl (name, type); } @@ -678,11 +699,11 @@ namespace ufo 0, nullptr, Z3_get_quantifier_bound_sort (ctx, z, i)); z3::ast zdecl (ctx, Z3_func_decl_to_ast (ctx, decl)); - args.push_back (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors)); + args.push_back (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors, constructors)); assert (args.back ().get ()); } args.push_back (unmarshal (z3::ast (ctx, Z3_get_quantifier_body (ctx, z)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); return Z3_is_quantifier_forall (ctx, z) ? mknary (args) : mknary (args); } @@ -700,35 +721,35 @@ namespace ufo { assert (Z3_get_app_num_args (ctx, app) == 1); return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); } if (dkind == Z3_OP_UMINUS) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); // XXX ignore to_real and to_int operators if (dkind == Z3_OP_TO_REAL || dkind == Z3_OP_TO_INT) return unmarshal(z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors); + efac, cache, seen, adts_seen, adts, accessors, constructors); if (dkind == Z3_OP_BNOT) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); if (dkind == Z3_OP_BNEG) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); if (dkind == Z3_OP_BREDAND) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); if (dkind == Z3_OP_BREDOR) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors)); + efac, cache, seen, adts_seen, adts, accessors, constructors)); if (dkind == Z3_OP_SIGN_EXT || dkind == Z3_OP_ZERO_EXT) { Expr sort = bv::bvsort (Z3_get_bv_sort_size (ctx, Z3_get_sort (ctx, z)), efac); Expr arg = unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors); + efac, cache, seen, adts_seen, adts, accessors, constructors); switch (dkind) { case Z3_OP_SIGN_EXT: @@ -742,7 +763,7 @@ namespace ufo if (dkind == Z3_OP_EXTRACT) { Expr arg = unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts, accessors); + efac, cache, seen, adts_seen, adts, accessors, constructors); Z3_func_decl d = Z3_get_app_decl (ctx, app); unsigned high = Z3_get_decl_int_parameter (ctx, d, 0); @@ -756,7 +777,7 @@ namespace ufo z3::ast zdecl (ctx, Z3_func_decl_to_ast (ctx, Z3_get_as_array_func_decl (ctx, z))); - return mk (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors)); + return mk (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors, constructors)); } { @@ -778,7 +799,7 @@ namespace ufo left = args[0]; } args.push_back (unmarshal - (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts, accessors)); + (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts, accessors, constructors)); } /** newly introduced Z3 symbol */ @@ -801,11 +822,11 @@ namespace ufo ExprVector eq; // Put value from the constructor into equality eq.push_back (bind::fapp (unmarshal (z3::func_decl (ctx, as), - efac, cache, seen, adts_seen, adts, accessors), { left })); + efac, cache, seen, adts_seen, adts, accessors, constructors), { left })); eq.push_back (args[num_accessors]); accessors.push_back(bind::fname((unmarshal (z3::func_decl (ctx, as), - efac, cache, seen, adts_seen, adts, accessors)))); + efac, cache, seen, adts_seen, adts, accessors, constructors)))); // accessor(data) = value subexpr.push_back(mknary (eq.begin(), eq.end())); } @@ -813,7 +834,7 @@ namespace ufo } Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), - efac, cache, seen, adts_seen, adts, accessors), args); + efac, cache, seen, adts_seen, adts, accessors, constructors), args); cache.insert (typename C::value_type (z, res)); left = NULL; return res; @@ -821,7 +842,7 @@ namespace ufo if (dkind == Z3_OP_UNINTERPRETED) { Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), - efac, cache, seen, adts_seen, adts, accessors), args); + efac, cache, seen, adts_seen, adts, accessors, constructors), args); // -- XXX maybe use seen instead. not sure what is best. cache.insert (typename C::value_type (z, res)); return res; @@ -832,7 +853,7 @@ namespace ufo // TODO: CHANGE THIS HARDCODE OF ACCESSORS Z3_func_decl acc = Z3_get_datatype_sort_constructor_accessor(ctx, srt, 1, 1); Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), - efac, cache, seen, adts_seen, adts, accessors), args); + efac, cache, seen, adts_seen, adts, accessors, constructors), args); accessors.push_back(bind::fname(res)); // -- XXX maybe use seen instead. not sure what is best. cache.insert (typename C::value_type (z, res)); @@ -918,7 +939,7 @@ namespace ufo Expr domain = unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, Z3_get_array_sort_domain (ctx, sort))), - efac, cache, seen, adts_seen, adts, accessors); + efac, cache, seen, adts_seen, adts, accessors, constructors); e = op::array::constArray (domain, args[0]); } diff --git a/tools/nonlin/NonlinSolver.cpp b/tools/nonlin/NonlinSolver.cpp index 3ebe23859..d53734968 100644 --- a/tools/nonlin/NonlinSolver.cpp +++ b/tools/nonlin/NonlinSolver.cpp @@ -152,6 +152,7 @@ int main (int argc, char ** argv) bool lmax = getBoolValue(OPT_LMAX, false, argc, argv); // All other attrs are inherited from FreqHorn: + bool help = getBoolValue(OPT_HELP, false, argc, argv); int max_attempts = getIntValue(OPT_MAX_ATTEMPTS, 10, argc, argv); int to = getIntValue(OPT_TO, 1000, argc, argv); bool densecode = getBoolValue(OPT_GET_FREQS, false, argc, argv); @@ -169,6 +170,10 @@ int main (int argc, char ** argv) bool d_s = getBoolValue(OPT_D4, false, argc, argv); int debug = getIntValue(OPT_DEBUG, 0, argc, argv); + if (help) { + // TODO: write help message + } + if (do_disj && (!d_p && !d_d)) { errs() << "WARNING: either \"" << OPT_D2 << "\" or \"" << OPT_D3 << "\" should be enabled\n" From e2e821b38da8e0c3dbf10587cc9d30605b63cc2f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E2=80=9CBritikovKI=E2=80=9D?= <“BritikovKI@yandex.ru”> Date: Sun, 2 Feb 2025 18:44:58 +0100 Subject: [PATCH 2/5] ADT fix: fixes on the go --- include/ae/SMTUtils.hpp | 2 +- include/ufo/Smt/Z3n.hpp | 2 +- include/ufo/Smt/ZExprConverter.hpp | 36 +++++++++++++++++++++--------- 3 files changed, 27 insertions(+), 13 deletions(-) diff --git a/include/ae/SMTUtils.hpp b/include/ae/SMTUtils.hpp index 7e2099e63..f4329d7bc 100644 --- a/include/ae/SMTUtils.hpp +++ b/include/ae/SMTUtils.hpp @@ -42,7 +42,7 @@ namespace ufo ; } - SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, std::vector adts, std::vector adts_seen, std::map> constructors) : + SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, std::vector adts, std::vector adts_seen, std::map> constructors) : efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL) { diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp index 539f20f40..3b0ed9f87 100644 --- a/include/ufo/Smt/Z3n.hpp +++ b/include/ufo/Smt/Z3n.hpp @@ -286,7 +286,7 @@ namespace ufo public: std::vector adts; std::vector adts_seen; - std::map> constructors; + std::map> constructors; protected: z3::context &get_ctx () { return ctx; } diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index def978c33..9e671daab 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -42,7 +42,7 @@ namespace ufo { template static z3::ast marshal (Expr e, z3::context &ctx, - C &cache, expr_ast_map &seen, std::vector adts, std::vector &adts_seen, std::map> &constructors) + C &cache, expr_ast_map &seen, std::vector adts, std::vector &adts_seen, std::map> &constructors) { assert (e); if (isOpX(e)) return z3::ast (ctx, Z3_mk_true (ctx)); @@ -82,7 +82,7 @@ namespace ufo // res = reinterpret_cast (Z3_mk_int_sort (ctx)); std::string name = lexical_cast(e->left()); Z3_symbol z3_name = Z3_mk_string_symbol(ctx, name.c_str()); - Z3_func_decl csts [constructors[name].size()]; + Z3_constructor csts [constructors[name].size()]; for(int i = 0; i static Expr unmarshal (const z3::ast &z, ExprFactory &efac, C &cache, ast_expr_map &seen, - std::vector &adts_seen, std::vector &adts, std::vector &accessors, std::map> &constructors) + std::vector &adts_seen, std::vector &adts, std::vector &accessors, std::map> &constructors) { z3::context &ctx = z.ctx (); @@ -599,24 +599,38 @@ namespace ufo case Z3_DATATYPE_SORT: { unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort); - std::vector dt_constructors; + std::vector dt_constructors; std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)); while (num > 0) { num--; auto c = Z3_get_datatype_sort_constructor(ctx, sort, num); - dt_constructors.push_back(c); unsigned num_accessors = Z3_get_domain_size(ctx, c); - Z3_Constructor const = Z3_mk_constructor(ctx, - Z3_get_sort_name(ctx, sort), - Z3_get_decl_name(ctx, c), - Z3_get_arity(ctx, c), - ) - + std::vector names; + std::vector sorts; while(num_accessors > 0){ num_accessors--; auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); + names.push_back( Z3_get_decl_name(ctx, as)); + sorts.push_back( Z3_get_sort(ctx, Z3_func_decl_to_ast(ctx, as))); + } + Z3_symbol names_array[names.size()]; + Z3_sort sorts_array[sorts.size()]; + for(unsigned i = 0; i < names.size(); ++i){ + names_array[i] = names[i]; + sorts_array[i] = sorts[i]; } + + Z3_constructor constr = Z3_mk_constructor(ctx, + Z3_get_sort_name(ctx, sort), + Z3_get_decl_name(ctx, c), + Z3_get_arity(ctx, c), + names_array, + sorts_array, + {} + ); + dt_constructors.push_back (constr); } + constructors.insert({name, dt_constructors}); Expr adt_name = mkTerm (name, efac); if (find(adts_seen.begin(), adts_seen.end(), name) == adts_seen.end()) From cf05ecbb1a9bd5b952f400784d3cc36d6cfaf20c Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 3 Feb 2025 14:13:50 +0100 Subject: [PATCH 3/5] ADT fix: TODO rework fParser and SMTUtils so they have same ctx and z3 in core --- include/ufo/Smt/ZExprConverter.hpp | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index 9e671daab..a5cd0f227 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -88,9 +88,13 @@ namespace ufo } Z3_mk_datatype(ctx, z3_name, unsigned(constructors[name].size()), csts); Z3_sort typeDt = Z3_mk_datatype_sort(ctx, z3_name); -// res = reinterpret_cast (typeDt); // auto kind = Z3_get_sort_kind(ctx, typeDt); auto consts = Z3_get_datatype_sort_num_constructors(ctx, typeDt); + auto c = Z3_get_datatype_sort_constructor(ctx, typeDt, 0); + unsigned num_accessors = Z3_get_domain_size(ctx, c); + + std::string name_DT = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx,typeDt)); + res = reinterpret_cast (typeDt); printf("Post reinterpret: %s\n", Z3_ast_to_string(ctx, res)); }// GF: hack for now else if (isOpX (e)) @@ -607,17 +611,27 @@ namespace ufo unsigned num_accessors = Z3_get_domain_size(ctx, c); std::vector names; std::vector sorts; + std::vector dt_sorts; + int j = 0; while(num_accessors > 0){ num_accessors--; - auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); + auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, j); names.push_back( Z3_get_decl_name(ctx, as)); sorts.push_back( Z3_get_sort(ctx, Z3_func_decl_to_ast(ctx, as))); + if(Z3_get_sort_kind(ctx, sorts.back()) == Z3_DATATYPE_SORT){ + dt_sorts.push_back(num_accessors); + } + j++; } Z3_symbol names_array[names.size()]; Z3_sort sorts_array[sorts.size()]; + unsigned dtsorts_array[dt_sorts.size()]; for(unsigned i = 0; i < names.size(); ++i){ names_array[i] = names[i]; sorts_array[i] = sorts[i]; + if(i Date: Tue, 4 Feb 2025 00:28:59 +0100 Subject: [PATCH 4/5] ADT fix: working version of testgen with datatypes --- include/ae/AeValSolver.hpp | 8 +++++--- include/ae/SMTUtils.hpp | 19 ++++++++++--------- include/deep/NonlinCHCsolver.hpp | 2 +- include/ufo/Smt/Z3n.hpp | 3 ++- include/ufo/Smt/ZExprConverter.hpp | 12 ++++++------ 5 files changed, 24 insertions(+), 20 deletions(-) diff --git a/include/ae/AeValSolver.hpp b/include/ae/AeValSolver.hpp index 219199d5b..eb96424eb 100644 --- a/include/ae/AeValSolver.hpp +++ b/include/ae/AeValSolver.hpp @@ -49,7 +49,7 @@ namespace ufo efac(s->getFactory()), z3(efac), smt (z3), - u(efac), + u(efac,z3), fresh_var_ind(0), partitioning_size(0), debug(0) @@ -794,7 +794,8 @@ namespace ufo template static Expr eliminateQuantifiersRepl(Expr fla, Range& vars) { ExprFactory &efac = fla->getFactory(); - SMTUtils u(efac); + EZ3 ez3(efac); + SMTUtils u(efac, ez3); ExprSet complex; findComplexNumerics(fla, complex); ExprMap repls; @@ -831,7 +832,8 @@ namespace ufo inline static Expr abduce (Expr goal, Expr assm) { ExprFactory &efac = goal->getFactory(); - SMTUtils u(efac); + EZ3 ez3(efac); + SMTUtils u(efac, ez3); ExprSet complex; findComplexNumerics(assm, complex); findComplexNumerics(goal, complex); diff --git a/include/ae/SMTUtils.hpp b/include/ae/SMTUtils.hpp index f4329d7bc..35ff3e71f 100644 --- a/include/ae/SMTUtils.hpp +++ b/include/ae/SMTUtils.hpp @@ -15,7 +15,7 @@ namespace ufo private: ExprFactory &efac; - EZ3 z3; + EZ3& z3; ZSolver smt; bool can_get_model; ZSolver::Model* m; @@ -24,14 +24,15 @@ namespace ufo public: - SMTUtils (ExprFactory& _efac) : - efac(_efac), z3(efac), smt (z3), can_get_model(0), m(NULL) {} - SMTUtils (ExprFactory& _efac, unsigned _to) : - efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL) {} + SMTUtils (ExprFactory& _efac, EZ3& _z3) : + efac(_efac), z3(_z3), smt (z3), can_get_model(0), m(NULL) {} - SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, bool _bv) : - efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL) + SMTUtils (ExprFactory& _efac, EZ3& _z3, unsigned _to) : + efac(_efac), z3(_z3), smt (z3, _to), can_get_model(0), m(NULL) {} + + SMTUtils (ExprFactory& _efac, EZ3& _z3, ExprVector& _accessors, unsigned _to, bool _bv) : + efac(_efac), z3(_z3), smt (z3, _to), can_get_model(0), m(NULL) { approxBV = _bv; for(auto b : _accessors) @@ -42,8 +43,8 @@ namespace ufo ; } - SMTUtils (ExprFactory& _efac, ExprVector& _accessors, unsigned _to, std::vector adts, std::vector adts_seen, std::map> constructors) : - efac(_efac), z3(efac), smt (z3, _to), can_get_model(0), m(NULL) + SMTUtils (ExprFactory& _efac, EZ3& _z3, ExprVector& _accessors, unsigned _to, std::vector adts, std::vector adts_seen, std::map> constructors) : + efac(_efac), z3(_z3), smt (z3, _to), can_get_model(0), m(NULL) { z3.adts = adts; diff --git a/include/deep/NonlinCHCsolver.hpp b/include/deep/NonlinCHCsolver.hpp index 82ff5e2ab..11adae699 100644 --- a/include/deep/NonlinCHCsolver.hpp +++ b/include/deep/NonlinCHCsolver.hpp @@ -71,7 +71,7 @@ namespace ufo NonlinCHCsolver(CHCs &r, map>> & s) : m_efac(r.m_efac), ruleManager(r), - u(m_efac, r.m_z3.getAdtAccessors(), 10000, r.m_z3.adts, r.m_z3.adts_seen, r.m_z3.constructors), signature(s) {} + u(m_efac, r.m_z3, r.m_z3.getAdtAccessors(), 10000, r.m_z3.adts, r.m_z3.adts_seen, r.m_z3.constructors), signature(s) {} bool checkAllOver(bool checkQuery = false) { for (auto &hr: ruleManager.chcs) { diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp index 3b0ed9f87..e5f034405 100644 --- a/include/ufo/Smt/Z3n.hpp +++ b/include/ufo/Smt/Z3n.hpp @@ -274,7 +274,6 @@ namespace ufo z3::ast_ptr_equal_to> > cache_type; ExprFactory& efac; - z3::context ctx; cache_type cache; @@ -284,6 +283,8 @@ namespace ufo } public: + + z3::context ctx; std::vector adts; std::vector adts_seen; std::map> constructors; diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index a5cd0f227..69d33c643 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -79,14 +79,14 @@ namespace ufo else if (isOpX (e)) res = reinterpret_cast (Z3_mk_bool_sort (ctx)); else if (isOpX (e)) { -// res = reinterpret_cast (Z3_mk_int_sort (ctx)); + // res = reinterpret_cast (Z3_mk_int_sort (ctx)); std::string name = lexical_cast(e->left()); Z3_symbol z3_name = Z3_mk_string_symbol(ctx, name.c_str()); - Z3_constructor csts [constructors[name].size()]; - for(int i = 0; i Date: Tue, 4 Feb 2025 14:44:33 +0100 Subject: [PATCH 5/5] ADT fix: cleaning up marshalling --- include/ae/SMTUtils.hpp | 6 +- include/deep/NonlinCHCsolver.hpp | 2 +- include/ufo/Smt/Z3n.hpp | 12 +- include/ufo/Smt/ZExprConverter.hpp | 202 +++++++++++------------------ 4 files changed, 78 insertions(+), 144 deletions(-) diff --git a/include/ae/SMTUtils.hpp b/include/ae/SMTUtils.hpp index 35ff3e71f..07bed1978 100644 --- a/include/ae/SMTUtils.hpp +++ b/include/ae/SMTUtils.hpp @@ -43,13 +43,9 @@ namespace ufo ; } - SMTUtils (ExprFactory& _efac, EZ3& _z3, ExprVector& _accessors, unsigned _to, std::vector adts, std::vector adts_seen, std::map> constructors) : + SMTUtils (ExprFactory& _efac, EZ3& _z3, ExprVector& _accessors, unsigned _to) : efac(_efac), z3(_z3), smt (z3, _to), can_get_model(0), m(NULL) { - - z3.adts = adts; - z3.adts_seen = adts_seen; - z3.constructors = constructors; for(auto b : _accessors) if (b->arity() == 3) accessors.insert(b); diff --git a/include/deep/NonlinCHCsolver.hpp b/include/deep/NonlinCHCsolver.hpp index 11adae699..2c98429d7 100644 --- a/include/deep/NonlinCHCsolver.hpp +++ b/include/deep/NonlinCHCsolver.hpp @@ -71,7 +71,7 @@ namespace ufo NonlinCHCsolver(CHCs &r, map>> & s) : m_efac(r.m_efac), ruleManager(r), - u(m_efac, r.m_z3, r.m_z3.getAdtAccessors(), 10000, r.m_z3.adts, r.m_z3.adts_seen, r.m_z3.constructors), signature(s) {} + u(m_efac, r.m_z3, r.m_z3.getAdtAccessors(), 10000), signature(s) {} bool checkAllOver(bool checkQuery = false) { for (auto &hr: ruleManager.chcs) { diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp index e5f034405..ef3d16837 100644 --- a/include/ufo/Smt/Z3n.hpp +++ b/include/ufo/Smt/Z3n.hpp @@ -274,6 +274,7 @@ namespace ufo z3::ast_ptr_equal_to> > cache_type; ExprFactory& efac; + z3::context ctx; cache_type cache; @@ -282,12 +283,6 @@ namespace ufo Z3_set_ast_print_mode (ctx, Z3_PRINT_SMTLIB2_COMPLIANT); } - public: - - z3::context ctx; - std::vector adts; - std::vector adts_seen; - std::map> constructors; protected: z3::context &get_ctx () { return ctx; } @@ -296,14 +291,14 @@ namespace ufo expr_ast_map seen_expr; z3::ast toAst (Expr e) { - return M::marshal (e, get_ctx (), cache.left, seen_expr, adts, adts_seen, constructors); + return M::marshal (e, get_ctx (), cache.left, seen_expr); } Expr toExpr (z3::ast a) { if (!a) return Expr(); // ast_expr_map seen; - auto res = U::unmarshal (a, get_efac (), cache.right, seen_ast, adts_seen, adts, accessors, constructors); + auto res = U::unmarshal (a, get_efac (), cache.right, seen_ast, accessors); return res; } @@ -354,7 +349,6 @@ namespace ufo return out.str (); } - ExprVector& getAdtConstructors(){ return adts; } ExprVector& getAdtAccessors(){ return accessors; } template diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index 69d33c643..a6852b9ff 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -42,7 +42,7 @@ namespace ufo { template static z3::ast marshal (Expr e, z3::context &ctx, - C &cache, expr_ast_map &seen, std::vector adts, std::vector &adts_seen, std::map> &constructors) + C &cache, expr_ast_map &seen) { assert (e); if (isOpX(e)) return z3::ast (ctx, Z3_mk_true (ctx)); @@ -65,7 +65,7 @@ namespace ufo if (bind::isBVar (e)) { - z3::ast sort (marshal (bind::type (e), ctx, cache, seen, adts, adts_seen, constructors)); + z3::ast sort (marshal (bind::type (e), ctx, cache, seen)); res = Z3_mk_bound (ctx, bind::bvarId (e), reinterpret_cast (static_cast (sort))); @@ -99,18 +99,18 @@ namespace ufo }// GF: hack for now else if (isOpX (e)) { - z3::ast _idx_sort (marshal (e->left (), ctx, cache, seen, adts, adts_seen, constructors)); - z3::ast _val_sort (marshal (e->right (), ctx, cache, seen, adts, adts_seen, constructors)); - Z3_sort idx_sort = reinterpret_cast + z3::ast _idx_sort (marshal (e->left (), ctx, cache, seen)); + z3::ast _val_sort (marshal (e->right (), ctx, cache, seen)); + Z3_sort idx_sort = reinterpret_cast (static_cast (_idx_sort)); - Z3_sort val_sort = reinterpret_cast + Z3_sort val_sort = reinterpret_cast (static_cast (_val_sort)); - res = reinterpret_cast - (Z3_mk_array_sort (ctx, idx_sort, val_sort)); + res = reinterpret_cast + (Z3_mk_array_sort (ctx, idx_sort, val_sort)); } else if (isOpX (e)) res = reinterpret_cast (Z3_mk_bv_sort (ctx, bv::width (e))); - + else if (isOpX(e)) { z3::sort sort (ctx, @@ -138,7 +138,7 @@ namespace ufo { z3::sort sort (ctx, Z3_mk_bv_sort (ctx, bv::width (e->arg (1)))); const MPZ& num = dynamic_cast (e->arg (0)->op ()); - + std::string val = boost::lexical_cast (num.get ()); res = Z3_mk_numeral (ctx, val.c_str (), sort); } @@ -195,7 +195,7 @@ namespace ufo for (size_t i = 0; i < bind::domainSz (e); ++i) { - z3::ast a (marshal (bind::domainTy (e, i), ctx, cache, seen, adts, adts_seen, constructors)); + z3::ast a (marshal (bind::domainTy (e, i), ctx, cache, seen)); pinned.push_back (a); domain [i] = reinterpret_cast (static_cast(a)); } @@ -204,7 +204,7 @@ namespace ufo z3::sort range (ctx, reinterpret_cast (static_cast - (marshal (bind::rangeTy (e), ctx, cache, seen, adts, adts_seen, constructors)))); + (marshal (bind::rangeTy (e), ctx, cache, seen)))); Expr fname = bind::fname (e); @@ -230,7 +230,7 @@ namespace ufo z3::func_decl zfdecl (ctx, reinterpret_cast (static_cast - (marshal (bind::fname (e), ctx, cache, seen, adts, adts_seen, constructors)))); + (marshal (bind::fname (e), ctx, cache, seen)))); // -- marshall all arguments except for the first one // -- (which is the fdecl) std::vector args (e->arity ()); @@ -241,7 +241,7 @@ namespace ufo for (ENode::args_iterator it = ++ (e->args_begin ()), end = e->args_end (); it != end; ++it) { - z3::ast a (marshal (*it, ctx, cache, seen, adts, adts_seen, constructors)); + z3::ast a (marshal (*it, ctx, cache, seen)); pinned_args.push_back (a); args [pos++] = a; } @@ -256,11 +256,11 @@ namespace ufo for (int i = 0; i < e->arity() - 1; i++) vars.push_back(bind::fapp(e->arg(i))); - z3::ast ast (marshal (e->last(), ctx, cache, seen, adts, adts_seen, constructors)); //z3.toAst (e->last())); + z3::ast ast (marshal (e->last(), ctx, cache, seen)); //z3.toAst (e->last())); std::vector bound; bound.reserve (boost::size (vars)); for (const Expr &v : vars) - bound.push_back (Z3_to_app (ctx, marshal (v, ctx, cache, seen, adts, adts_seen, constructors))); + bound.push_back (Z3_to_app (ctx, marshal (v, ctx, cache, seen))); if (isOpX (e)) res = Z3_mk_forall_const (ctx, 0, @@ -289,49 +289,49 @@ namespace ufo // -- then it's a NEG or UN_MINUS if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); return z3::ast (ctx, Z3_mk_unary_minus(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); return z3::ast (ctx, Z3_mk_not(ctx, arg)); } if (isOpX (e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); return z3::ast (ctx, Z3_mk_array_default (ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); return z3::ast (ctx, Z3_mk_bvnot(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); return z3::ast (ctx, Z3_mk_bvneg(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); return z3::ast (ctx, Z3_mk_bvredand(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); return z3::ast (ctx, Z3_mk_bvredor(ctx, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); //TODO: SECOND NUMBER IS THE AMOUNT OF BITS IN THE BV ENCODING return z3::ast (ctx, Z3_mk_int2bv(ctx, 64, arg)); } if (isOpX(e)) { - z3::ast arg = marshal (e->left(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast arg = marshal (e->left(), ctx, cache, seen); //TODO: BOOL DESCRIBES IF NUMBER IS UNSIGNED OR NOT return z3::ast (ctx, Z3_mk_bv2int(ctx, arg, true)); } @@ -340,8 +340,8 @@ namespace ufo } else if (arity == 2) { - z3::ast t1 = marshal(e->left(), ctx, cache, seen, adts, adts_seen, constructors); - z3::ast t2 = marshal(e->right(), ctx, cache, seen, adts, adts_seen, constructors); + z3::ast t1 = marshal(e->left(), ctx, cache, seen); + z3::ast t2 = marshal(e->right(), ctx, cache, seen); Z3_ast args [2] = {t1, t2}; @@ -390,13 +390,13 @@ namespace ufo else if (isOpX