From a6f58bdd173f7d8b4ee55c710c4158f59a76b8cb Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 30 Oct 2014 17:22:34 -0700 Subject: [PATCH 01/15] fixes and performance improvements for interp and duality --- src/duality/duality.h | 4 ++ src/duality/duality_rpfp.cpp | 108 ++++++++++++++++++++------------- src/duality/duality_solver.cpp | 12 ++++ src/interp/iz3mgr.cpp | 6 +- src/interp/iz3mgr.h | 3 +- 5 files changed, 88 insertions(+), 45 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index edd89d78f..04527450c 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -778,6 +778,10 @@ protected: struct Bad { }; + // thrown on more serious internal error + struct ReallyBad { + }; + /** Pop a scope (see Push). Note, you cannot pop axioms. */ void Pop(int num_scopes); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index f2824c9b0..cdc8fb3b2 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2643,6 +2643,10 @@ namespace Duality { GetGroundLitsUnderQuants(memo,f.body(),res,1); return; } + if(f.is_var()){ + // std::cout << "foo!\n"; + return; + } if(under && f.is_ground()) res.push_back(f); } @@ -3065,10 +3069,14 @@ namespace Duality { node->Annotation.SetEmpty(); hash_set *core = new hash_set; core->insert(node->Outgoing->dual); + expr prev_annot = ctx.bool_val(false); + expr prev_impl = ctx.bool_val(false); + int repeated_case_count = 0; while(1){ by_case_counter++; is.push(); expr annot = !GetAnnotation(node); + Transformer old_annot = node->Annotation; is.add(annot); if(is.check() == unsat){ is.pop(1); @@ -3076,56 +3084,70 @@ namespace Duality { } is.pop(1); Push(); - ConstrainEdgeLocalized(node->Outgoing,is.get_implicant()); + expr the_impl = is.get_implicant(); + if(eq(the_impl,prev_impl)){ + // std::cout << "got old implicant\n"; + repeated_case_count++; + } + prev_impl = the_impl; + ConstrainEdgeLocalized(node->Outgoing,the_impl); ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this? - check_result foo = Check(root); - if(foo != unsat){ - slvr().print("should_be_unsat.smt2"); - throw "should be unsat"; - } - std::vector assumps, axioms_to_add; - slvr().get_proof().get_assumptions(assumps); - for(unsigned i = 0; i < assumps.size(); i++){ - (*core).insert(assumps[i]); - if(axioms_needed.find(assumps[i]) != axioms_needed.end()){ - axioms_to_add.push_back(assumps[i]); - axioms_needed.erase(assumps[i]); - } - } - // AddToProofCore(*core); - Transformer old_annot = node->Annotation; - SolveSingleNode(root,node); - - { - expr itp = GetAnnotation(node); - dualModel = is.get_model(); // TODO: what does this mean? - std::vector case_lits; - itp = StrengthenFormulaByCaseSplitting(itp, case_lits); - SetAnnotation(node,itp); - node->Annotation.Formula = node->Annotation.Formula.simplify(); - } - - for(unsigned i = 0; i < axioms_to_add.size(); i++) - is.add(axioms_to_add[i]); -#define TEST_BAD -#ifdef TEST_BAD { - static int bad_count = 0, num_bads = 1; - if(bad_count >= num_bads){ - bad_count = 0; - num_bads = num_bads * 2; + check_result foo = Check(root); + if(foo != unsat){ Pop(1); is.pop(1); delete core; timer_stop("InterpolateByCases"); - throw Bad(); + throw ReallyBad(); + // slvr().print("should_be_unsat.smt2"); + // throw "should be unsat"; } - bad_count++; - } -#endif + std::vector assumps, axioms_to_add; + slvr().get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++){ + (*core).insert(assumps[i]); + if(axioms_needed.find(assumps[i]) != axioms_needed.end()){ + axioms_to_add.push_back(assumps[i]); + axioms_needed.erase(assumps[i]); + } + } + // AddToProofCore(*core); + SolveSingleNode(root,node); - if(node->Annotation.IsEmpty()){ + { + expr itp = GetAnnotation(node); + dualModel = is.get_model(); // TODO: what does this mean? + std::vector case_lits; + itp = StrengthenFormulaByCaseSplitting(itp, case_lits); + SetAnnotation(node,itp); + node->Annotation.Formula = node->Annotation.Formula.simplify(); + } + + for(unsigned i = 0; i < axioms_to_add.size(); i++) + is.add(axioms_to_add[i]); + +#define TEST_BAD +#ifdef TEST_BAD + { + static int bad_count = 0, num_bads = 1; + if(bad_count >= num_bads){ + bad_count = 0; + num_bads = num_bads * 2; + Pop(1); + is.pop(1); + delete core; + timer_stop("InterpolateByCases"); + throw Bad(); + } + bad_count++; + } +#endif + } + + if(node->Annotation.IsEmpty() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){ + looks_bad: if(!axioms_added){ // add the axioms in the off chance they are useful const std::vector &theory = ls->get_axioms(); @@ -3134,6 +3156,7 @@ namespace Duality { axioms_added = true; } else { + //#define KILL_ON_BAD_INTERPOLANT #ifdef KILL_ON_BAD_INTERPOLANT std::cout << "bad in InterpolateByCase -- core:\n"; #if 0 @@ -3175,10 +3198,11 @@ namespace Duality { is.pop(1); delete core; timer_stop("InterpolateByCases"); - throw Bad(); + throw ReallyBad(); } } Pop(1); + prev_annot = node->Annotation.Formula; node->Annotation.UnionWith(old_annot); } if(proof_core) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 69759f9bb..b40ab9370 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2279,6 +2279,18 @@ namespace Duality { // bad interpolants can get us here throw DoRestart(); } + catch(const RPFP::ReallyBad &){ + // this could be caused by incompleteness + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + node->map->Annotation.SetFull(); + std::vector &chs = node->map->Outgoing->Children; + for(unsigned j = 0; j < chs.size(); j++) + chs[j]->Annotation.SetFull(); + reporter->Message("incompleteness: cleared annotation and child annotations"); + } + throw DoRestart(); + } catch(char const *msg){ // bad interpolants can get us here reporter->Message(std::string("interpolation failure:") + msg); diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index a39065922..e3ac59dfd 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -778,6 +778,8 @@ int iz3mgr::occurs_in(ast var, ast e){ bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){ + if(occurs_in(v,y)) + return false; if(op(x) == Plus){ int n = num_args(x); for(int i = 0; i < n; i++){ @@ -801,8 +803,8 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, as return ast(); cont_eq_memo.insert(e); if(!truth && op(e) == Equal){ - if(arg(e,0) == v) return(arg(e,1)); - if(arg(e,1) == v) return(arg(e,0)); + if(arg(e,0) == v && !occurs_in(v,arg(e,1))) return(arg(e,1)); + if(arg(e,1) == v && !occurs_in(v,arg(e,0))) return(arg(e,0)); ast res; if(solve_arith(v,arg(e,0),arg(e,1),res)) return res; if(solve_arith(v,arg(e,1),arg(e,0),res)) return res; diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 3ec2c42d1..7f66bb2d8 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -278,7 +278,8 @@ class iz3mgr { } symb sym(ast t){ - return to_app(t.raw())->get_decl(); + raw_ast *_ast = t.raw(); + return is_app(_ast) ? to_app(_ast)->get_decl() : 0; } std::string string_of_symbol(symb s){ From adeae184718a40e008823a0405bc679a5842a91b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Nov 2014 13:09:25 +0100 Subject: [PATCH 02/15] delay initializing internal manager so that parser does not choke on proper SMT-LIB logics. Reported by Venkateshan Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 8 ++++++++ src/cmd_context/cmd_context.cpp | 33 ++++++++++++++++++++------------- src/cmd_context/cmd_context.h | 1 + 3 files changed, 29 insertions(+), 13 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 248d2161e..71a6dde2b 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3988,6 +3988,12 @@ END_MLAPI_EXCLUDE /** \brief Return a unique identifier for \c t. + The identifier is unique up to structural equality. Thus, two ast nodes + created by the same context and having the same children and same function symbols + have the same identifiers. Ast nodes created in the same context, but having + different children or different functions have different identifiers. + Variables and quantifiers are also assigned different identifiers according to + their structure. \mlonly \remark Implicitly used by [Pervasives.compare] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly def_API('Z3_get_ast_id', UINT, (_in(CONTEXT), _in(AST))) @@ -3996,6 +4002,8 @@ END_MLAPI_EXCLUDE /** \brief Return a hash code for the given AST. + The hash code is structural. You can use Z3_get_ast_id interchangably with + this function. \mlonly \remark Implicitly used by [Hashtbl.hash] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST))) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 731608524..7fa2dc53f 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -314,8 +314,9 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_numeral_as_real(false), m_ignore_check(false), m_exit_on_error(false), - m_manager(m), + m_manager(m), m_own_manager(m == 0), + m_manager_initialized(false), m_pmanager(0), m_sexpr_manager(0), m_regular("stdout", std::cout), @@ -326,8 +327,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): install_core_tactic_cmds(*this); install_interpolant_cmds(*this); SASSERT(m != 0 || !has_manager()); - if (m) - init_external_manager(); if (m_main_ctx) { set_verbose_stream(diagnostic_stream()); } @@ -620,12 +619,22 @@ void cmd_context::init_manager_core(bool new_manager) { } void cmd_context::init_manager() { - SASSERT(m_manager == 0); - SASSERT(m_pmanager == 0); - m_check_sat_result = 0; - m_manager = m_params.mk_ast_manager(); - m_pmanager = alloc(pdecl_manager, *m_manager); - init_manager_core(true); + if (m_manager_initialized) { + // no-op + } + else if (m_manager) { + SASSERT(!m_own_manager); + init_external_manager(); + m_manager_initialized = true; + } + else { + SASSERT(m_pmanager == 0); + m_check_sat_result = 0; + m_manager = m_params.mk_ast_manager(); + m_pmanager = alloc(pdecl_manager, *m_manager); + init_manager_core(true); + m_manager_initialized = true; + } } void cmd_context::init_external_manager() { @@ -1211,8 +1220,7 @@ void cmd_context::assert_expr(symbol const & name, expr * t) { void cmd_context::push() { m_check_sat_result = 0; - if (!has_manager()) - init_manager(); + init_manager(); m_scopes.push_back(scope()); scope & s = m_scopes.back(); s.m_func_decls_stack_lim = m_func_decls_stack.size(); @@ -1332,8 +1340,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions return; IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;); TRACE("before_check_sat", dump_assertions(tout);); - if (!has_manager()) - init_manager(); + init_manager(); if (m_solver) { m_check_sat_result = m_solver.get(); // solver itself stores the result. m_solver->set_progress_callback(this); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 8ad07e8cc..7c42f41cf 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -149,6 +149,7 @@ protected: ast_manager * m_manager; bool m_own_manager; + bool m_manager_initialized; pdecl_manager * m_pmanager; sexpr_manager * m_sexpr_manager; check_logic m_check_logic; From 23bc982ad24e27feb6ad0635f23fce0a6b8ad8be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Nov 2014 16:53:51 +0100 Subject: [PATCH 03/15] move initialization to support more sort usage scenarios Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 4 ++-- src/cmd_context/cmd_context.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 7fa2dc53f..5d24977b5 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -623,17 +623,17 @@ void cmd_context::init_manager() { // no-op } else if (m_manager) { + m_manager_initialized = true; SASSERT(!m_own_manager); init_external_manager(); - m_manager_initialized = true; } else { + m_manager_initialized = true; SASSERT(m_pmanager == 0); m_check_sat_result = 0; m_manager = m_params.mk_ast_manager(); m_pmanager = alloc(pdecl_manager, *m_manager); init_manager_core(true); - m_manager_initialized = true; } } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 7c42f41cf..c4aa34c61 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -294,7 +294,7 @@ public: std::string reason_unknown() const; bool has_manager() const { return m_manager != 0; } - ast_manager & m() const { if (!m_manager) const_cast(this)->init_manager(); return *m_manager; } + ast_manager & m() const { const_cast(this)->init_manager(); return *m_manager; } virtual ast_manager & get_ast_manager() { return m(); } pdecl_manager & pm() const { if (!m_pmanager) const_cast(this)->init_manager(); return *m_pmanager; } sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; } From ce7303b5e2713be2909a39d862c0fe2bba8659c5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Nov 2014 15:44:21 +0100 Subject: [PATCH 04/15] fix reset logic and load only logics admitted by context Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 30 ++++++++++++++++++++++++++---- src/cmd_context/cmd_context.h | 1 + 2 files changed, 27 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 5d24977b5..ee5437bd6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -470,6 +470,16 @@ void cmd_context::register_plugin(symbol const & name, decl_plugin * p, bool ins } } +void cmd_context::load_plugin(symbol const & name, bool install, svector& fids) { + family_id id = m_manager->get_family_id(name); + decl_plugin* p = m_manager->get_plugin(id); + if (install && p && fids.contains(id)) { + register_builtin_sorts(p); + register_builtin_ops(p); + } + fids.erase(id); +} + bool cmd_context::logic_has_arith_core(symbol const & s) const { return s == "QF_LRA" || @@ -586,17 +596,26 @@ void cmd_context::init_manager_core(bool new_manager) { register_builtin_sorts(basic); register_builtin_ops(basic); // the manager was created by the command context. - register_plugin(symbol("arith"), alloc(arith_decl_plugin), logic_has_arith()); - register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv()); - register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array()); + register_plugin(symbol("arith"), alloc(arith_decl_plugin), logic_has_arith()); + register_plugin(symbol("bv"), alloc(bv_decl_plugin), logic_has_bv()); + register_plugin(symbol("array"), alloc(array_decl_plugin), logic_has_array()); register_plugin(symbol("datatype"), alloc(datatype_decl_plugin), logic_has_datatype()); register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); register_plugin(symbol("float"), alloc(float_decl_plugin), logic_has_floats()); } else { - // the manager was created by an external module, we must register all plugins available in the manager. + // the manager was created by an external module + // we register all plugins available in the manager. + // unless the logic specifies otherwise. svector fids; m_manager->get_range(fids); + load_plugin(symbol("arith"), logic_has_arith(), fids); + load_plugin(symbol("bv"), logic_has_bv(), fids); + load_plugin(symbol("array"), logic_has_array(), fids); + load_plugin(symbol("datatype"), logic_has_datatype(), fids); + load_plugin(symbol("seq"), logic_has_seq(), fids); + load_plugin(symbol("float"), logic_has_floats(), fids); + svector::iterator it = fids.begin(); svector::iterator end = fids.end(); for (; it != end; ++it) { @@ -1174,12 +1193,15 @@ void cmd_context::reset(bool finalize) { if (m_own_manager) { dealloc(m_manager); m_manager = 0; + m_manager_initialized = false; } else { // doesn't own manager... so it cannot be deleted // reinit cmd_context if this is not a finalization step if (!finalize) init_external_manager(); + else + m_manager_initialized = false; } } if (m_sexpr_manager) { diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index c4aa34c61..1c8dba21a 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -214,6 +214,7 @@ protected: void register_builtin_sorts(decl_plugin * p); void register_builtin_ops(decl_plugin * p); void register_plugin(symbol const & name, decl_plugin * p, bool install_names); + void load_plugin(symbol const & name, bool install_names, svector& fids); void init_manager_core(bool new_manager); void init_manager(); void init_external_manager(); From cf8ad072d017aada57ed2d342fc6bec6ddd0929a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Nov 2014 16:03:27 +0100 Subject: [PATCH 05/15] remove unused variable Signed-off-by: Nikolaj Bjorner --- src/smt/theory_array_base.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index b2c17b4e0..b33e6b4e6 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -362,7 +362,6 @@ namespace smt { (store A i v) <--- v is used as an value */ bool theory_array_base::is_shared(theory_var v) const { - context & ctx = get_context(); enode * n = get_enode(v); enode * r = n->get_root(); bool is_array = false; From 005bb82a1751f3d70705bff9819acdec608d9f41 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Nov 2014 16:04:02 +0000 Subject: [PATCH 06/15] eliminated unused variables --- src/ast/fpa/fpa2bv_converter.cpp | 42 ++++++++++++++++---------------- src/interp/iz3base.h | 2 +- src/interp/iz3proof_itp.cpp | 3 ++- 3 files changed, 24 insertions(+), 23 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 5f92b4d94..c23de3bfa 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2155,15 +2155,15 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_parameter(0).is_int()); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - int width = f->get_parameter(0).get_int(); + //unsigned ebits = m_util.get_ebits(f->get_range()); + //unsigned sbits = m_util.get_sbits(f->get_range()); + //int width = f->get_parameter(0).get_int(); - expr * rm = args[0]; - expr * x = args[1]; + //expr * rm = args[0]; + //expr * x = args[1]; - expr * sgn, *s, *e; - split(x, sgn, s, e); + //expr * sgn, *s, *e; + //split(x, sgn, s, e); NOT_IMPLEMENTED_YET(); } @@ -2173,15 +2173,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg SASSERT(f->get_num_parameters() == 1); SASSERT(f->get_parameter(0).is_int()); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - int width = f->get_parameter(0).get_int(); + //unsigned ebits = m_util.get_ebits(f->get_range()); + //unsigned sbits = m_util.get_sbits(f->get_range()); + //int width = f->get_parameter(0).get_int(); - expr * rm = args[0]; - expr * x = args[1]; + //expr * rm = args[0]; + //expr * x = args[1]; - expr * sgn, *s, *e; - split(x, sgn, s, e); + //expr * sgn, *s, *e; + //split(x, sgn, s, e); NOT_IMPLEMENTED_YET(); } @@ -2189,15 +2189,15 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); - int width = f->get_parameter(0).get_int(); + //unsigned ebits = m_util.get_ebits(f->get_range()); + //unsigned sbits = m_util.get_sbits(f->get_range()); + //int width = f->get_parameter(0).get_int(); - expr * rm = args[0]; - expr * x = args[1]; + //expr * rm = args[0]; + //expr * x = args[1]; - expr * sgn, *s, *e; - split(x, sgn, s, e); + //expr * sgn, *s, *e; + //split(x, sgn, s, e); NOT_IMPLEMENTED_YET(); } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index bca9b8518..956191290 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -161,7 +161,7 @@ class iz3base : public iz3mgr, public scopes { stl_ext::hash_map simplify_memo; stl_ext::hash_map frame_map; // map assertions to frames - int frames; // number of frames + // int frames; // number of frames protected: void add_frame_range(int frame, ast t); diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 52ddcd64f..b487b2892 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2747,7 +2747,8 @@ class iz3proof_itp_impl : public iz3proof_itp { ast orig_e = e; pf = make_refl(e); // proof that e = e - prover::range erng = pv->ast_scope(e); + // prover::range erng = + pv->ast_scope(e); #if 0 if(!(erng.lo > erng.hi) && pv->ranges_intersect(pv->ast_scope(e),rng)){ return e; // this term occurs in range, so it's O.K. From a309dbfdc2b3ebca65946b6afe443e815a1f1cee Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 12 Nov 2014 20:28:11 -0800 Subject: [PATCH 07/15] coerce equality and ite upward instead of downward for int2real coercions. Fixes bug reported by Enric Carbonell Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 25 +++++++++++++++++++------ src/ast/ast.h | 3 ++- 2 files changed, 21 insertions(+), 7 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 68f7596ee..09965be85 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1013,6 +1013,17 @@ func_decl * basic_decl_plugin::mk_ite_decl(sort * s) { return m_ite_decls[id]; } +sort* basic_decl_plugin::join(sort* s1, sort* s2) { + if (s1 == s2) return s1; + if (s1->get_family_id() == m_manager->m_arith_family_id && + s2->get_family_id() == m_manager->m_arith_family_id) { + if (s1->get_decl_kind() == REAL_SORT) { + return s1; + } + } + return s2; +} + func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (static_cast(k)) { @@ -1025,10 +1036,10 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_IFF: return m_iff_decl; case OP_IMPLIES: return m_implies_decl; case OP_XOR: return m_xor_decl; - case OP_ITE: return arity == 3 ? mk_ite_decl(domain[1]) : 0; + case OP_ITE: return arity == 3 ? mk_ite_decl(join(domain[1], domain[2])) : 0; // eq and oeq must have at least two arguments, they can have more since they are chainable - case OP_EQ: return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, domain[0], m_eq_decls) : 0; - case OP_OEQ: return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, domain[0], m_oeq_decls) : 0; + case OP_EQ: return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, join(domain[0],domain[1]), m_eq_decls) : 0; + case OP_OEQ: return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(domain[0],domain[1]), m_oeq_decls) : 0; case OP_DISTINCT: { func_decl_info info(m_family_id, OP_DISTINCT); info.set_pairwise(); @@ -1061,10 +1072,12 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_IFF: return m_iff_decl; case OP_IMPLIES: return m_implies_decl; case OP_XOR: return m_xor_decl; - case OP_ITE: return num_args == 3 ? mk_ite_decl(m_manager->get_sort(args[1])): 0; + case OP_ITE: return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): 0; // eq and oeq must have at least two arguments, they can have more since they are chainable - case OP_EQ: return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, m_manager->get_sort(args[0]), m_eq_decls) : 0; - case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, m_manager->get_sort(args[0]), m_oeq_decls) : 0; + case OP_EQ: return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, join(m_manager->get_sort(args[0]), + m_manager->get_sort(args[1])), m_eq_decls) : 0; + case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(m_manager->get_sort(args[0]), + m_manager->get_sort(args[1])), m_oeq_decls) : 0; case OP_DISTINCT: return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range); default: diff --git a/src/ast/ast.h b/src/ast/ast.h index 68f08e1ac..944c089f3 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1100,6 +1100,7 @@ protected: virtual void set_manager(ast_manager * m, family_id id); func_decl * mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector & cache); func_decl * mk_ite_decl(sort * s); + sort* join(sort* s1, sort* s2); public: basic_decl_plugin(); @@ -1378,7 +1379,7 @@ enum proof_gen_mode { // ----------------------------------- class ast_manager { -protected: + friend basic_decl_plugin; protected: struct config { typedef ast_manager value_manager; From 4c5753f32144da6a4a8f244318a938e780d79dba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Nov 2014 18:08:24 -0800 Subject: [PATCH 08/15] be classy with your friends Signed-off-by: Nikolaj Bjorner --- src/ast/ast.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 944c089f3..93f456965 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1379,7 +1379,7 @@ enum proof_gen_mode { // ----------------------------------- class ast_manager { - friend basic_decl_plugin; + friend class basic_decl_plugin; protected: struct config { typedef ast_manager value_manager; From 213d816c0a418bafc8fe57acb4b10aeea5b1f5b2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 24 Nov 2014 18:10:54 +0000 Subject: [PATCH 09/15] Bugfix for bv_size_reduction. Thanks to user rsas for reporting this isse! Signed-off-by: Christoph M. Wintersteiger --- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index e149afc75..14a2fb28d 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -229,7 +229,7 @@ struct bv_size_reduction_tactic::imp { else { // l < u if (l.is_neg()) { - unsigned i_nb = (u - l).get_num_bits(); + unsigned i_nb = (u - l).get_num_bits() + 1; unsigned v_nb = m_util.get_bv_size(v); if (i_nb < v_nb) { new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb)); From 53cfa472141fc9dd5c6f07e62a1786243636f846 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Nov 2014 14:22:50 +0000 Subject: [PATCH 10/15] bugfix for bv_size_reduction Signed-off-by: Christoph M. Wintersteiger --- src/tactic/bv/bv_size_reduction_tactic.cpp | 26 ++++++++++++++++++---- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 14a2fb28d..5e32bf6c4 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -229,17 +229,35 @@ struct bv_size_reduction_tactic::imp { else { // l < u if (l.is_neg()) { - unsigned i_nb = (u - l).get_num_bits() + 1; + unsigned l_nb = (-l).get_num_bits(); unsigned v_nb = m_util.get_bv_size(v); - if (i_nb < v_nb) { - new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb)); - new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const); + + if (u.is_neg()) + { + // l <= v <= u <= 0 + unsigned i_nb = l_nb; + TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";); + if (i_nb < v_nb) { + new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb)); + new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const); + } + } + else { + // l <= v <= 0 <= u + unsigned u_nb = u.get_num_bits(); + unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1; + TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";); + if (i_nb < v_nb) { + new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb)); + new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const); + } } } else { // 0 <= l <= v <= u unsigned u_nb = u.get_num_bits(); unsigned v_nb = m_util.get_bv_size(v); + TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";); if (u_nb < v_nb) { new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb)); new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const); From 59dfd2abe451b9f0c5cb0218f53699f8bdf49a37 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 25 Nov 2014 14:54:47 +0000 Subject: [PATCH 11/15] fixed problem with Python 3.4.x complainging of inconsistent use of spaces/tabs. Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 42 +++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index e58e47640..851e8e243 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -298,8 +298,8 @@ class AstRef(Z3PPObject): return self.ast def get_id(self): - """Return unique identifier for object. It can be used for hash-tables and maps.""" - return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + """Return unique identifier for object. It can be used for hash-tables and maps.""" + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) def ctx_ref(self): @@ -453,7 +453,7 @@ class SortRef(AstRef): return Z3_sort_to_ast(self.ctx_ref(), self.ast) def get_id(self): - return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) def kind(self): @@ -595,7 +595,7 @@ class FuncDeclRef(AstRef): return Z3_func_decl_to_ast(self.ctx_ref(), self.ast) def get_id(self): - return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) def as_func_decl(self): return self.ast @@ -743,7 +743,7 @@ class ExprRef(AstRef): return self.ast def get_id(self): - return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) def sort(self): """Return the sort of expression `self`. @@ -1540,7 +1540,7 @@ class PatternRef(ExprRef): return Z3_pattern_to_ast(self.ctx_ref(), self.ast) def get_id(self): - return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) def is_pattern(a): """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. @@ -1605,7 +1605,7 @@ class QuantifierRef(BoolRef): return self.ast def get_id(self): - return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) + return Z3_get_ast_id(self.ctx_ref(), self.as_ast()) def sort(self): """Return the Boolean sort.""" @@ -6033,20 +6033,20 @@ class Solver(Z3PPObject): return Z3_solver_to_string(self.ctx.ref(), self.solver) def to_smt2(self): - """return SMTLIB2 formatted benchmark for solver's assertions""" - es = self.assertions() - sz = len(es) - sz1 = sz - if sz1 > 0: - sz1 -= 1 - v = (Ast * sz1)() - for i in range(sz1): - v[i] = es[i].as_ast() - if sz > 0: - e = es[sz1].as_ast() - else: - e = BoolVal(True, self.ctx).as_ast() - return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e) + """return SMTLIB2 formatted benchmark for solver's assertions""" + es = self.assertions() + sz = len(es) + sz1 = sz + if sz1 > 0: + sz1 -= 1 + v = (Ast * sz1)() + for i in range(sz1): + v[i] = es[i].as_ast() + if sz > 0: + e = es[sz1].as_ast() + else: + e = BoolVal(True, self.ctx).as_ast() + return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e) From 1a396b0bd2eebe4f3ad7826cfec1fd8cbb7574cf Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 25 Nov 2014 18:13:24 +0000 Subject: [PATCH 12/15] [BV size reduction] fix bug in detection of signed upperbound Signed-off-by: Nuno Lopes --- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 5e32bf6c4..707a9284b 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -151,7 +151,7 @@ struct bv_size_reduction_tactic::imp { // bound is infeasible. } else { - update_signed_upper(to_app(lhs), val); + update_signed_upper(to_app(rhs), val); } } else update_signed_lower(to_app(rhs), val); From c88b2f6b5ebbaf34ab5a610008d054cee8da869a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Dec 2014 14:35:15 +0000 Subject: [PATCH 13/15] .NET API: Added build instructions for .NET 3.5 Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Readme.NET35 | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 src/api/dotnet/Readme.NET35 diff --git a/src/api/dotnet/Readme.NET35 b/src/api/dotnet/Readme.NET35 new file mode 100644 index 000000000..73743fd15 --- /dev/null +++ b/src/api/dotnet/Readme.NET35 @@ -0,0 +1,9 @@ +The default Z3 bindings for .NET are built for the .NET framework version 4. +Should the need arise, it is also possible to build them for .NET 3.5; the +instructions are as follows: + +In the project properties of Microsoft.Z3.csproj: +- Under 'Application': Change Target framework to .NET Framework 3.5 +- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols +- Remove the reference to System.Numerics +- Install the NuGet Package "Microsoft Code Contracts for Net3.5" From 45755bbd140231ad08fcbc487d60fc00a2eee78f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Dec 2014 08:55:14 +0900 Subject: [PATCH 14/15] fix context sensitivity. Codeplex issue 148, thanks to clockish Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 851e8e243..db629cd2d 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -6166,7 +6166,7 @@ class Fixedpoint(Z3PPObject): Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name) else: body = _get_args(body) - f = self.abstract(Implies(And(body),head)) + f = self.abstract(Implies(And(body, self.ctx),head)) Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) def rule(self, head, body = None, name = None): @@ -6194,7 +6194,7 @@ class Fixedpoint(Z3PPObject): if sz == 1: query = query[0] else: - query = And(query) + query = And(query, self.ctx) query = self.abstract(query, False) r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast()) return CheckSatResult(r) @@ -6213,7 +6213,7 @@ class Fixedpoint(Z3PPObject): name = "" name = to_symbol(name, self.ctx) body = _get_args(body) - f = self.abstract(Implies(And(body),head)) + f = self.abstract(Implies(And(body, self.ctx),head)) Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name) def get_answer(self): From 8181b15a1bc86123a4f2c15de2f9cabe8bdbc481 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 8 Dec 2014 15:46:55 -0800 Subject: [PATCH 15/15] attempted interp fixes --- src/interp/iz3proof_itp.cpp | 2 +- src/interp/iz3translate.cpp | 12 ++++++++++-- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 52ddcd64f..df436d206 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -1027,7 +1027,7 @@ class iz3proof_itp_impl : public iz3proof_itp { linear_comb(Aineqs,coeff,make(Leq,make_int(rational(0)),make(Sub,term2,term1))); } else { - ast pf = extract_rewrites(make(concat,mk_true(),rest),p1); + ast pf = extract_rewrites(make(concat,mk_true(),last),p1); ast new_normal = fix_normal(term1,term2,pf); normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves); } diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 26786d57a..f65ec72d4 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1712,11 +1712,17 @@ public: std::cout << "foo!\n"; // no idea why this shows up - if(dk == PR_MODUS_PONENS_OEQ) + if(dk == PR_MODUS_PONENS_OEQ){ if(conc(prem(proof,0)) == con){ res = translate_main(prem(proof,0),expect_clause); return res; } + if(expect_clause && op(con) == Or){ // skolemization does this + Iproof::node clause = translate_main(prem(proof,0),true); + res = RewriteClause(clause,prem(proof,1)); + return res; + } + } #if 0 if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){ @@ -1800,7 +1806,9 @@ public: } break; } - case PR_MONOTONICITY: { + case PR_QUANT_INTRO: + case PR_MONOTONICITY: + { std::vector eqs; eqs.resize(args.size()); for(unsigned i = 0; i < args.size(); i++) eqs[i] = conc(prem(proof,i));