From b343dcb341ea707891a4161043225ec79fcba415 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 29 Apr 2015 12:41:36 -0700 Subject: [PATCH 1/4] better recovery from incompleteness and interp failure in duality --- src/duality/duality.h | 3 +++ src/duality/duality_rpfp.cpp | 18 ++++++++++++++---- src/duality/duality_solver.cpp | 4 ++++ src/interp/iz3proof_itp.cpp | 5 ++++- 4 files changed, 25 insertions(+), 5 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index cde703617..72d72ac6b 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -782,6 +782,9 @@ namespace Duality { struct ReallyBad { }; + // throw when greedy reduction fails + struct greedy_reduce_failed {}; + /** 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 897bc521f..9da720ccc 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2870,10 +2870,10 @@ namespace Duality { lits = assumps; std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); - for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something! + for(int k = 0; k < 4; k++) // keep trying, maybe MBQI will do something! if((res = CheckCore(lits,full_core)) == unsat) goto is_unsat; - throw "should be unsat"; + throw greedy_reduce_failed(); } is_unsat: FilterCore(core,full_core); @@ -3084,8 +3084,18 @@ namespace Duality { } } // AddToProofCore(*core); - SolveSingleNode(root,node); - + + try { + SolveSingleNode(root,node); + } + catch (char const *msg){ + // This happens if interpolation fails + Pop(1); + is.pop(1); + delete core; + timer_stop("InterpolateByCases"); + throw msg; + } { expr itp = GetAnnotation(node); dualModel = is.get_model(); // TODO: what does this mean? diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 4568ea913..d935c2655 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2295,6 +2295,10 @@ namespace Duality { reporter->Message(std::string("interpolation failure:") + msg); throw DoRestart(); } + catch(const RPFP::greedy_reduce_failed &){ + // if we couldn't reduce, just continue (maybe should restart?) + reporter->Message("interpolant verification failed"); + } if(RecordUpdate(node)){ update_count++; total_updates++; diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 046b0b7f1..507096340 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -562,7 +562,10 @@ class iz3proof_itp_impl : public iz3proof_itp { else res = clone(e,args); } catch (const cannot_simplify &){ - res = clone(e,args); + if(g == sum) + res = clone(e,args); + else + throw "interpolation failure"; } } return res; From 357a92dfef8b2b3aafad0763c588bf153709764b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Oct 2015 18:11:31 -0700 Subject: [PATCH 2/4] n/a Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index bad141e94..96133b88e 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1451,6 +1451,11 @@ namespace smt { normalize_gain(min_gain.get_rational(), max_gain); } + if (is_int(x_i) && !max_gain.is_rational()) { + max_gain = inf_numeral(floor(max_gain)); + normalize_gain(min_gain.get_rational(), max_gain); + } + if (!max_inc.is_minus_one()) { if (is_int(x_i)) { TRACE("opt", From 589053fc102e9a7a38c497defc75a96f782489d2 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 27 Oct 2015 18:27:25 -0700 Subject: [PATCH 3/4] interp: fix gomory cut rule with non-local conclusion (issue #200) --- src/interp/iz3translate.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 51084f809..5bb91a49e 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1201,9 +1201,12 @@ public: ast t = arg(my_con,0); ast c = arg(my_con,1); ast d = gcd_of_coefficients(t); + /* t = z3_simplify(mk_idiv(t,d)); c = z3_simplify(mk_idiv(c,d)); ast cut_con = make(op(my_con),t,c); + */ + ast cut_con = con; return iproof->make_cut_rule(my_con,d,cut_con,res); } From b197e590a4a9d816be3dbb2f72ddc4308056e3eb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Oct 2015 19:25:38 -0700 Subject: [PATCH 4/4] fix coercion regression. Issue #263 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 8713c4fdb..0622f03ff 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1602,6 +1602,7 @@ namespace smt { TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n"; tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";); + if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) { has_shared = false;