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

z3: update to 4.8.12 (#7187)

Browse Source
This commit is contained in:
YAKSH BARIYA 2021-07-26 15:19:03 +05:30 committed by GitHub
parent 302321b066
commit 697202f15f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 51 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
packages/z3/build.sh
View File

@ -2,9 +2,9 @@ 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.9
TERMUX_PKG_VERSION=4.8.12
TERMUX_PKG_SRCURL=https://github.com/Z3Prover/z3/archive/z3-$TERMUX_PKG_VERSION.tar.gz
TERMUX_PKG_SHA256=c9fd04b9b33be74fffaac3ec2bc2c320d1a4cc32e395203c55126b12a14ff3f4
TERMUX_PKG_SHA256=e3aaefde68b839299cbc988178529535e66048398f7d083b40c69fe0da55f8b7
TERMUX_PKG_BUILD_IN_SRC=true
TERMUX_MAKE_PROCESSES=1
@ -13,6 +13,10 @@ termux_step_configure() {
chmod +x scripts/mk_make.py
CXX="$CXX" CC="$CC" python${_PYTHON_VERSION} scripts/mk_make.py --prefix=$TERMUX_PREFIX --build=$TERMUX_PKG_BUILDDIR
sed 's%../../../../../%%g' -i Makefile
if $TERMUX_ON_DEVICE_BUILD; then
sed 's%../../../../../../../../%%g' -i Makefile
else
sed 's%../../../../../%%g' -i Makefile
fi
sed 's/\-lpthread//g' -i config.mk
}

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

@ -0,0 +1,11 @@
--- ./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 Normal file
View File

@ -0,0 +1,11 @@
--- ./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 Normal file
View File

@ -0,0 +1,11 @@
--- ./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 Normal file
View File

@ -0,0 +1,11 @@
--- ./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 {