From 49c72abb2ddf9621e4a209397b6b82bf1698fac2 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 5 Nov 2013 12:17:09 -0800 Subject: [PATCH] new interpolation fixes; re-added fixedpoint-push/pop --- src/ast/ast.cpp | 2 +- src/interp/iz3checker.cpp | 17 +++++ src/interp/iz3checker.h | 8 +++ src/interp/iz3interp.cpp | 1 + src/interp/iz3mgr.cpp | 15 +++++ src/interp/iz3proof_itp.cpp | 83 +++++++++++++++++++----- src/interp/iz3translate.cpp | 6 +- src/muz/base/dl_context.cpp | 4 ++ src/muz/duality/duality_dl_interface.cpp | 1 + src/muz/fp/dl_cmds.cpp | 40 +++++++++++- 10 files changed, 156 insertions(+), 21 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 9de402082..36aeea9a0 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1307,7 +1307,7 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs): void ast_manager::init() { // TODO: the following is a HACK to enable proofs in the old smt solver // When we stop using that solver, this hack can be removed - m_proof_mode = PGM_FINE; + // m_proof_mode = PGM_FINE; m_int_real_coercions = true; m_debug_ref_count = false; diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index 7792c2401..b4e55af20 100755 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -170,6 +170,11 @@ struct iz3checker : iz3base { iz3checker(ast_manager &_m) : iz3base(_m) { } + + iz3checker(iz3mgr &_m) + : iz3base(_m) { + } + }; template @@ -193,6 +198,18 @@ bool iz3check(ast_manager &_m_manager, return chk.check(s,err,chk.cook(cnsts),to_std_vector(parents),chk.cook(interps),chk.cook(theory)); } +bool iz3check(iz3mgr &mgr, + solver *s, + std::ostream &err, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &interps, + const std::vector &theory) +{ + iz3checker chk(mgr); + return chk.check(s,err,cnsts,parents,interps,theory); +} + bool iz3check(ast_manager &_m_manager, solver *s, std::ostream &err, diff --git a/src/interp/iz3checker.h b/src/interp/iz3checker.h index 5402e4d68..d46ea0654 100644 --- a/src/interp/iz3checker.h +++ b/src/interp/iz3checker.h @@ -38,4 +38,12 @@ bool iz3check(ast_manager &_m_manager, ast *tree, const ptr_vector &interps); +bool iz3check(iz3mgr &mgr, + solver *s, + std::ostream &err, + const std::vector &cnsts, + const std::vector &parents, + const std::vector &interps, + const ptr_vector &theory); + #endif diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 2ef36f4e2..92afc5723 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -304,6 +304,7 @@ public: fr.fix_interpolants(interps_vec); interps = interps_vec; + } diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index bd82d235a..b9a3fd0b0 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -476,6 +476,15 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& coeffs){ } } +static void abs_rat(std::vector &rats){ + // check that they are all non-neg -- if neg, take abs val and warn! + for(unsigned i = 0; i < rats.size(); i++) + if(rats[i].is_neg()){ + // std::cout << "negative Farkas coeff!\n"; + rats[i] = -rats[i]; + } +} + void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& rats){ symb s = sym(proof); int numps = s->get_num_parameters(); @@ -494,12 +503,15 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& rats){ } rats[i-2] = r; } +#if 0 if(rats.size() != 0 && rats[0].is_neg()){ for(unsigned i = 0; i < rats.size(); i++){ assert(rats[i].is_neg()); rats[i] = -rats[i]; } } +#endif + abs_rat(rats); extract_lcd(rats); } @@ -536,6 +548,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r } rats[i-1] = r; } +#if 0 if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them for(unsigned i = 1; i < rats.size(); i++){ if(!rats[i].is_neg()) @@ -543,6 +556,8 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector& r rats[i] = -rats[i]; } } +#endif + abs_rat(rats); extract_lcd(rats); } diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 3bf4dd620..9d15912c2 100644 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -626,7 +626,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equa = sep_cond(arg(pf,0),cond); if(is_equivrel_chain(equa)){ ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove - ast ineqs= chain_ineqs(LitA,equa,lhs,rhs); // chain must be from lhs to rhs + ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs cond = my_and(cond,chain_conditions(LitA,equa)); ast Bconds = chain_conditions(LitB,equa); if(is_true(Bconds) && op(ineqs) != And) @@ -1313,7 +1313,7 @@ class iz3proof_itp_impl : public iz3proof_itp { } - ast chain_ineqs(LitType t, const ast &chain, const ast &lhs, const ast &rhs){ + ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){ if(is_true(chain)){ if(lhs != rhs) throw "bad ineq inference"; @@ -1322,9 +1322,12 @@ class iz3proof_itp_impl : public iz3proof_itp { ast last = chain_last(chain); ast rest = chain_rest(chain); ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last)); - ast cond = chain_ineqs(t,rest,lhs,mid); + ast cond = chain_ineqs(comp_op,t,rest,lhs,mid); if(is_rewrite_side(t,last)){ - ast foo = z3_simplify(make(Leq,make_int("0"),make(Sub,mid,rhs))); + ast diff; + if(comp_op == Leq) diff = make(Sub,rhs,mid); + else diff = make(Sub,mid,rhs); + ast foo = z3_simplify(make(Leq,make_int("0"),diff)); if(is_true(cond)) cond = foo; else { @@ -1351,6 +1354,8 @@ class iz3proof_itp_impl : public iz3proof_itp { std::swap(lhs,rhs); if(op(rhs) == Times){ rhs = arg(rhs,1); + if(op(ineq) == Leq) + std::swap(lhs,rhs); return; } } @@ -1368,16 +1373,31 @@ class iz3proof_itp_impl : public iz3proof_itp { /** Make an assumption node. The given clause is assumed in the given frame. */ virtual node make_assumption(int frame, const std::vector &assumption){ - if(pv->in_range(frame,rng)){ - std::vector itp_clause; - for(unsigned i = 0; i < assumption.size(); i++) - if(get_term_type(assumption[i]) != LitA) - itp_clause.push_back(assumption[i]); - ast res = my_or(itp_clause); - return res; + if(!weak){ + if(pv->in_range(frame,rng)){ + std::vector itp_clause; + for(unsigned i = 0; i < assumption.size(); i++) + if(get_term_type(assumption[i]) != LitA) + itp_clause.push_back(assumption[i]); + ast res = my_or(itp_clause); + return res; + } + else { + return mk_true(); + } } else { - return mk_true(); + if(pv->in_range(frame,rng)){ + return mk_false(); + } + else { + std::vector itp_clause; + for(unsigned i = 0; i < assumption.size(); i++) + if(get_term_type(assumption[i]) != LitB) + itp_clause.push_back(assumption[i]); + ast res = my_or(itp_clause); + return mk_not(res); + } } } @@ -1602,17 +1622,20 @@ class iz3proof_itp_impl : public iz3proof_itp { virtual node make_congruence(const ast &p, const ast &con, const ast &prem1){ ast x = arg(p,0), y = arg(p,1); ast itp; + LitType con_t = get_term_type(con); if(get_term_type(p) == LitA){ - if(get_term_type(con) == LitA) + if(con_t == LitA) itp = mk_false(); + else if(con_t == LitB) + itp = p; else itp = make_mixed_congruence(x, y, p, con, prem1); } else { - if(get_term_type(con) == LitA) + if(con_t == LitA) itp = mk_not(p); else{ - if(get_term_type(con) == LitB) + if(con_t == LitB) itp = mk_true(); else itp = make_mixed_congruence(x, y, p, con, prem1); @@ -2047,30 +2070,58 @@ public: { pv = p; rng = r; - weak = w; + weak = false ; //w; type boolintbooldom[3] = {bool_type(),int_type(),bool_type()}; type booldom[1] = {bool_type()}; type boolbooldom[2] = {bool_type(),bool_type()}; type boolboolbooldom[3] = {bool_type(),bool_type(),bool_type()}; type intbooldom[2] = {int_type(),bool_type()}; contra = function("@contra",2,boolbooldom,bool_type()); + m().inc_ref(contra); sum = function("@sum",3,boolintbooldom,bool_type()); + m().inc_ref(sum); rotate_sum = function("@rotsum",2,boolbooldom,bool_type()); + m().inc_ref(rotate_sum); leq2eq = function("@leq2eq",3,boolboolbooldom,bool_type()); + m().inc_ref(leq2eq); eq2leq = function("@eq2leq",2,boolbooldom,bool_type()); + m().inc_ref(eq2leq); cong = function("@cong",3,boolintbooldom,bool_type()); + m().inc_ref(cong); exmid = function("@exmid",3,boolboolbooldom,bool_type()); + m().inc_ref(exmid); symm = function("@symm",1,booldom,bool_type()); + m().inc_ref(symm); epsilon = make_var("@eps",int_type()); modpon = function("@mp",3,boolboolbooldom,bool_type()); + m().inc_ref(modpon); no_proof = make_var("@nop",bool_type()); concat = function("@concat",2,boolbooldom,bool_type()); + m().inc_ref(concat); top_pos = make_var("@top_pos",bool_type()); add_pos = function("@add_pos",2,intbooldom,bool_type()); + m().inc_ref(add_pos); rewrite_A = function("@rewrite_A",3,boolboolbooldom,bool_type()); + m().inc_ref(rewrite_A); rewrite_B = function("@rewrite_B",3,boolboolbooldom,bool_type()); + m().inc_ref(rewrite_B); } + ~iz3proof_itp_impl(){ + m().dec_ref(contra); + m().dec_ref(sum); + m().dec_ref(rotate_sum); + m().dec_ref(leq2eq); + m().dec_ref(eq2leq); + m().dec_ref(cong); + m().dec_ref(exmid); + m().dec_ref(symm); + m().dec_ref(modpon); + m().dec_ref(concat); + m().dec_ref(add_pos); + m().dec_ref(rewrite_A); + m().dec_ref(rewrite_B); + } }; iz3proof_itp *iz3proof_itp::create(prover *p, const prover::range &r, bool w){ diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index ff5d24228..04a9dd2c1 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -881,11 +881,11 @@ public: std::vector my_prems; std::vector my_coeffs; std::vector my_prem_cons; - for(unsigned i = 0; i < coeffs.size(); i++){ + for(unsigned i = pol ? 0 : 1; i < coeffs.size(); i+= 2){ rational &c = coeffs[i]; - if(pol ? c.is_pos() : c.is_neg()){ + if(c.is_pos()){ my_prems.push_back(prems[i]); - my_coeffs.push_back(pol ? make_int(c) : make_int(-c)); + my_coeffs.push_back(make_int(c)); my_prem_cons.push_back(conc(prem(proof,i))); } } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 89fb19569..e540f5aaf 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -187,6 +187,10 @@ namespace datalog { if (m_trail.get_num_scopes() == 0) { throw default_exception("there are no backtracking points to pop to"); } + if(m_engine.get()){ + if(get_engine() != DUALITY_ENGINE) + throw default_exception("operation is not supported by engine"); + } m_trail.pop_scope(1); } diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 7de8f54a0..eb74f797f 100644 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -82,6 +82,7 @@ dl_interface::dl_interface(datalog::context& dl_ctx) : { _d = 0; + dl_ctx.get_manager().toggle_proof_mode(PGM_FINE); } diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 612d319ad..827b90e60 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -454,6 +454,44 @@ public: } }; +/** + \brief fixedpoint-push command. +*/ +class dl_push_cmd : public cmd { + ref m_dl_ctx; +public: + dl_push_cmd(dl_context * dl_ctx): + cmd("fixedpoint-push"), + m_dl_ctx(dl_ctx) + {} + + virtual char const * get_usage() const { return ""; } + virtual char const * get_descr(cmd_context & ctx) const { return "push the fixedpoint context"; } + virtual unsigned get_arity() const { return 0; } + virtual void execute(cmd_context & ctx) { + m_dl_ctx->push(); + } +}; + +/** + \brief fixedpoint-pop command. +*/ +class dl_pop_cmd : public cmd { + ref m_dl_ctx; +public: + dl_pop_cmd(dl_context * dl_ctx): + cmd("fixedpoint-pop"), + m_dl_ctx(dl_ctx) + {} + + virtual char const * get_usage() const { return ""; } + virtual char const * get_descr(cmd_context & ctx) const { return "pop the fixedpoint context"; } + virtual unsigned get_arity() const { return 0; } + virtual void execute(cmd_context & ctx) { + m_dl_ctx->pop(); + } +}; + static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) { dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds); @@ -463,7 +501,7 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c ctx.insert(alloc(dl_declare_var_cmd, dl_ctx)); // #ifndef _EXTERNAL_RELEASE // TODO: we need these! -#if 0 +#if 1 ctx.insert(alloc(dl_push_cmd, dl_ctx)); // not exposed to keep command-extensions simple. ctx.insert(alloc(dl_pop_cmd, dl_ctx)); #endif