From 8d9a631c5da252a31588d61fb50476b39666b80a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Jul 2019 16:21:03 +0100 Subject: [PATCH 1/6] try to copy artifacts Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 3 +++ src/tactic/arith/purify_arith_tactic.cpp | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index d8224b262..fd5fddce8 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -69,6 +69,9 @@ jobs: inputs: artifactName: 'Ubuntu' targetPath: tmp + - task: CopyFiles@2 + sourceFolder: $(Build.ArtifactStagingDirectory) + targetFilder: tmp # TBD: build NuGet package # TBD: this script should build a specific pre-specified tag - task: GitHubRelease@0 diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 611783077..0ef8adfbe 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -297,7 +297,7 @@ struct purify_arith_proc { EQ(u().mk_mul(y, k), x))); push_cnstr_pr(result_pr); rational r; - if (complete() && (!u().is_numeral(y, r) || r.is_zero())) { + if (complete() && (!u().is_numeral(y, r) || !r.is_zero())) { // y != 0 \/ k = div-0(x) push_cnstr(OR(NOT(EQ(y, mk_real_zero())), EQ(k, u().mk_div(x, mk_real_zero())))); From 77df8ebd12e903cd9326079a46e0d4452e494e36 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Jul 2019 16:23:02 +0100 Subject: [PATCH 2/6] try to copy artifacts Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/release.yml b/scripts/release.yml index fd5fddce8..79e94c6d1 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -70,6 +70,7 @@ jobs: artifactName: 'Ubuntu' targetPath: tmp - task: CopyFiles@2 + inputs: sourceFolder: $(Build.ArtifactStagingDirectory) targetFilder: tmp # TBD: build NuGet package From adb91ae93cd0b299a0aa1151020623a64c47da7c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jul 2019 09:07:18 +0100 Subject: [PATCH 3/6] compile 0 case regardless of numerical value Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 0ef8adfbe..18947787b 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -297,7 +297,7 @@ struct purify_arith_proc { EQ(u().mk_mul(y, k), x))); push_cnstr_pr(result_pr); rational r; - if (complete() && (!u().is_numeral(y, r) || !r.is_zero())) { + if (complete()) { // y != 0 \/ k = div-0(x) push_cnstr(OR(NOT(EQ(y, mk_real_zero())), EQ(k, u().mk_div(x, mk_real_zero())))); From 9474833c989797de64fe47faba4a726b8cdc8ea6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jul 2019 09:26:22 +0100 Subject: [PATCH 4/6] fix #2391 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/purify_arith_tactic.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 18947787b..3d993392c 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -181,6 +181,10 @@ struct purify_arith_proc { return true; } + struct div_def { + expr* x, *y, *d; + div_def(expr* x, expr* y, expr* d): x(x), y(y), d(d) {} + }; struct rw_cfg : public default_rewriter_cfg { purify_arith_proc & m_owner; @@ -189,6 +193,7 @@ struct purify_arith_proc { expr_ref_vector m_pinned; expr_ref_vector m_new_cnstrs; proof_ref_vector m_new_cnstr_prs; + svector m_divs; expr_ref m_subst; proof_ref m_subst_pr; expr_ref_vector m_new_vars; @@ -303,6 +308,7 @@ struct purify_arith_proc { EQ(k, u().mk_div(x, mk_real_zero())))); push_cnstr_pr(result_pr); } + m_divs.push_back(div_def(x, y, k)); } void process_idiv(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { @@ -768,6 +774,16 @@ struct purify_arith_proc { for (unsigned i = 0; i < sz; i++) { m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : nullptr, nullptr); } + auto const& divs = r.cfg().m_divs; + for (unsigned i = 0; i < divs.size(); ++i) { + auto const& p1 = divs[i]; + for (unsigned j = i + 1; j < divs.size(); ++j) { + auto const& p2 = divs[j]; + m_goal.assert_expr(m().mk_implies( + m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), + m().mk_eq(p1.d, p2.d))); + } + } // add generic_model_converter to eliminate auxiliary variables from model if (produce_models) { From c7fb1e4c9f21a5141881b19847343b85103fe1b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jul 2019 09:56:08 +0100 Subject: [PATCH 5/6] fix spelling of target folder Signed-off-by: Nikolaj Bjorner --- scripts/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/release.yml b/scripts/release.yml index 79e94c6d1..3e96bef86 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -72,7 +72,7 @@ jobs: - task: CopyFiles@2 inputs: sourceFolder: $(Build.ArtifactStagingDirectory) - targetFilder: tmp + targetFolder: tmp # TBD: build NuGet package # TBD: this script should build a specific pre-specified tag - task: GitHubRelease@0 From cfb4d289b8b2e210c1bf6d4ae07dbefe193ea363 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jul 2019 10:34:35 +0100 Subject: [PATCH 6/6] fix #2325 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_recfun.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index cc7ec0e36..d4f34f359 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -88,7 +88,11 @@ namespace smt { // the internalization of the arguments may have triggered the internalization of term. if (!ctx().e_internalized(term)) { ctx().mk_enode(term, false, false, true); + if (!ctx().relevancy() && u().is_defined(term)) { + push_case_expand(alloc(case_expansion, u(), term)); + } } + return true; } @@ -117,8 +121,8 @@ namespace smt { */ void theory_recfun::relevant_eh(app * n) { SASSERT(ctx().relevancy()); + TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); if (u().is_defined(n) && u().has_defs()) { - TRACEFN("relevant_eh: (defined) " << mk_pp(n, m)); push_case_expand(alloc(case_expansion, u(), n)); } }