sergiotarxz/termux-packages
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

z3: update to 4.8.14 (#8984)

Browse Source
This commit is contained in:
YAKSH BARIYA 2022-02-09 11:30:42 +00:00 committed by GitHub
parent dec84a59a4
commit 8b15720788
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 2 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
packages/z3/build.sh
View File

@ -2,14 +2,12 @@ TERMUX_PKG_HOMEPAGE=https://github.com/Z3Prover/z3
TERMUX_PKG_DESCRIPTION="Z3 is a theorem prover from Microsoft Research."
TERMUX_PKG_LICENSE="MIT"
TERMUX_PKG_MAINTAINER="@termux"
TERMUX_PKG_VERSION=4.8.12
TERMUX_PKG_REVISION=2
TERMUX_PKG_VERSION=4.8.14
TERMUX_PKG_SRCURL=https://github.com/Z3Prover/z3/archive/z3-$TERMUX_PKG_VERSION.tar.gz
TERMUX_PKG_SHA256=e3aaefde68b839299cbc988178529535e66048398f7d083b40c69fe0da55f8b7
TERMUX_PKG_SHA256=96a1f49a7701120cc38bfa63c02ff93be4d64c7926cea41977dedec7d87a1364
TERMUX_PKG_AUTO_UPDATE=true
TERMUX_PKG_AUTO_UPDATE_TAG_REGEXP="\d+\.\d+\.\d+"
TERMUX_PKG_BUILD_IN_SRC=true
TERMUX_MAKE_PROCESSES=1
termux_step_configure() {
_PYTHON_VERSION=$(source $TERMUX_SCRIPTDIR/packages/python/build.sh; echo $_MAJOR_VERSION)

11
packages/z3/sat-smt-euf_solver.cpp.patch
View File

@ -1,11 +0,0 @@
--- ./src/sat/smt/euf_solver.cpp 2021-07-13 18:55:23.000000000 +0530
+++ ./src/sat/smt/euf_solver.cpp.mod 2021-07-26 10:59:51.900088232 +0530
@@ -836,7 +836,7 @@
::solver::push_eh_t& push_eh,
::solver::pop_eh_t& pop_eh,
::solver::fresh_eh_t& fresh_eh) {
- m_user_propagator = alloc(user::solver, *this);
+ m_user_propagator = alloc(z3_user::solver, *this);
m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
for (unsigned i = m_scopes.size(); i-- > 0; )
m_user_propagator->push();

11
packages/z3/sat-smt-euf_solver.h.patch
View File

@ -1,11 +0,0 @@
--- ./src/sat/smt/euf_solver.h 2021-07-26 09:42:33.123349945 +0530
+++ ./src/sat/smt/euf_solver.h.mod 2021-07-26 09:42:55.080018799 +0530
@@ -101,7 +101,7 @@
sat::sat_internalizer* m_to_si;
scoped_ptr<euf::ackerman> m_ackerman;
scoped_ptr<sat::dual_solver> m_dual_solver;
- user::solver* m_user_propagator{ nullptr };
+ z3_user::solver* m_user_propagator{ nullptr };
th_solver* m_qsolver { nullptr };
unsigned m_generation { 0 };
mutable ptr_vector<expr> m_todo;

11
packages/z3/sat-smt-user_solver.cpp.patch
View File

@ -1,11 +0,0 @@
--- ./src/sat/smt/user_solver.cpp 2021-07-26 07:42:52.185967924 +0530
+++ ./src/sat/smt/user_solver.cpp.mod 2021-07-26 07:43:11.439303175 +0530
@@ -18,7 +18,7 @@
#include "sat/smt/user_solver.h"
#include "sat/smt/euf_solver.h"
-namespace user {
+namespace z3_user {
solver::solver(euf::solver& ctx) :
th_euf_solver(ctx, symbol("user"), ctx.get_manager().mk_family_id("user"))

11
packages/z3/sat-smt-user_solver.h.patch
View File

@ -1,11 +0,0 @@
--- ./src/sat/smt/user_solver.h 2021-07-26 09:41:09.413341606 +0530
+++ ./src/sat/smt/user_solver.h.mod 2021-07-26 09:41:19.996675994 +0530
@@ -23,7 +23,7 @@
#include "solver/solver.h"
-namespace user {
+namespace z3_user {
class solver : public euf::th_euf_solver, public ::solver::propagate_callback {