Index index by Group index by Distribution index by Vendor index by creation date index by Name Mirrors Help Search

z3-4.8.11-1.1 RPM for ppc64le

From OpenSuSE Ports Tumbleweed for ppc64le

Name: z3 Distribution: openSUSE Tumbleweed
Version: 4.8.11 Vendor: openSUSE
Release: 1.1 Build date: Fri Jun 11 22:57:09 2021
Group: Productivity/Scientific/Other Build host: obs-power9-07
Size: 19195358 Source RPM: z3-4.8.11-1.1.src.rpm
Packager: http://bugs.opensuse.org
Url: https://github.com/Z3Prover/z3/wiki
Summary: Theorem prover from Microsoft Research
Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates
several decision procedures: Linear real and integer arithmetic,
fixed-size bit vectors, uninterpreted functions, extensional arrays,
quantifiers and model generation.

Provides

Requires

License

MIT

Changelog

* Fri Jun 11 2021 Paolo Stivanin <info@paolostivanin.com>
  - update to 4.8.11:
    * fix soundness issues, invalid models, and crashes for options
    "tactic.default_tactic=smt sat.euf=true"
    * centos -> glibc
    * updated ref to esrp
    * undo cxx hoist
    * hoist c++ flags
* Fri Jan 29 2021 Dirk Müller <dmueller@suse.com>
  - update to 4.8.10:
    - rewritten arithmetic solver replacing legacy arithmetic solver and on by default
* Thu Sep 17 2020 Dirk Mueller <dmueller@suse.com>
  - update to 4.8.9:
    significant improvements to regular expression solving expose user theory
    plugin. It is a leaner user theory plugin that was once available.
    It allows for registering callbacks that react to when bit-vector and Boolean variables
    receive fixed values.
    - many
    - the new arithmetic theory is turned on by default. It _does_ introduce
    regressions on several scenarios, but has its own advantages. Users can
    turn on the old solver by setting smt.arith.solver=2.
    Depending on feedback, we may turn toggle this default setting again back to smt.arith.solver=2.
  - remove remove-timestamp.patch, 5a42a000e938a295feb1a7070dd74b192796db4e.patch (upstream)
* Fri Jul 17 2020 Mark Stopka <mstopka@opensuse.org>
  - Backport pkg-config support from upstream
    * add 5a42a000e938a295feb1a7070dd74b192796db4e.patch
* Thu Jul 16 2020 Guillaume GARDET <guillaume.gardet@opensuse.org>
  - Drop ExclusiveArch as it does build properly on other archs
* Tue May 26 2020 Martin Pluskal <mpluskal@suse.com>
  - Update to version 4.8.8:
    * Various small changes
  - Switch to released tarball from git snapshot
* Wed Apr 08 2020 Martin Pluskal <mpluskal@suse.com>
  - Update to version 4.8.7+git.20200407:
    * work on random_updates
    * fill columns to fill in random update as in theory_arith_aux.h
    * block selected configurations from HORN tactic
    * set arith.solver=6 by default
    * revert the default arith.solver=2
    * simplify patch_blocker()
    * redirect to the new solver
    * fix the patch of real vars
    * change lar_terms to use column indices
    * change lar_terms to use column indices
    * fix #3713: too much caching in dom-simplify for OR expressions
    * fix #3739 - dependencies may be valid even if they are null
    * [spacer] fix ugly bug in ground refutation generation (i.e., cex)
    * Replace is_null with is_non_empty_string in spacer params
    * [spacer] fixedpoint.get_answer() returns ground refutation for SAT
    * reduce_invertible: fix mk_diagonal for BV 0 switch from -x to ~x
    * minor code simplification in bv rewriter
    * reduce_invertible: recognize (* x -1) as the same as (- x)
    * roll back in maximize_term if the integrality is broken
    * remove output from normalize bounds
    * and plenty of other chanes
  - Use cmake_build macro
* Thu Jan 30 2020 jslaby@suse.com
  - Update to version 4.8.7+git.20200129:
    * change in the test lp.cpp and in a trace statement
    * Add explicit instantiation of update_inf_cost_for_column_tableau.
    * fix build
    * speed up freedom interval computation
    * return l_undef in get_phase() if lpvar is not available
    * add filter to gcd test
    * fix #2898
    * correct handling of int terms in theory_lra
    * fix the debug build
    * and much more
* Thu Oct 10 2019 jslaby@suse.com
  - Update to version 4.8.6+git.20191009:
    * fix assert-and-track semantics for smt2 logging
    * remove separate API for setting solver log, use parameter setting instead
    * make smt2 log scope aware
    * remove a few str copies when throwing exceptions
    * adding SMT2 log file for solver interaction #867
    * bit-vector overflow/underflow operators exposed over C++ API
    * use Z3_char_ptr
    * expose mk_divides over API. Corresponds to a = b (mod m), #723
    * and many more...
* Mon Feb 25 2019 jslaby@suse.com
  - Update to version 4.8.4+git.20190224:
    * integrate some self-contained fixes from #2147
    * fix #2149
    * fix -Wsign-compare (len can never become negative anyway)
    * remove debug code
    * Fix translation of FPA numerals in ast_smt_pp. Fixes #2145.
    * fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts
    * stopwatch: fix debug build crash in sat solver
    * fix VS build, take 2
    * stopwatches: fix a few places that would call start/stop multiple times
    * and more...
  - crop long changelogs
  - use ExclusiveArch to avoid broken builds on other archs
* Thu Nov 22 2018 Martin Pluskal <mpluskal@suse.com>
  - Update to version 4.8.3+git.20181121:
    * fix is-unit test in seq rewriter
    * fixing #1948
    * Improve intra-doc linking.
    * fix #1959
    * fix #1958
    * add rc2 sample
    * fix #1956
    * add macz3 status
    * and more...
* Fri Jun 15 2018 mimi.vx@gmail.com
  - Update to version 4.7.1+git.20180614:
    * fix memory leak in relation_manager, use for loops
    * fix #1665
    * remove trial with mfsr flag
    * enable non-expression bodies of quantifiers to fix #1667
    * fix bugs exposed by Nuno's PB example
    * z3.py: add overflow checks to PB API
    * gcc mode
    * int64_t
    * deal with shift exponent error
    * deal with shift exponent error
    * try flags to fix gcc build
    * int64_t
    * try new gcd
    * and more...
* Fri May 18 2018 mpluskal@suse.com
  - Use python3 exclusively
  - Do not call contrib/cmake/bootstrap.py - it is obsolete
* Thu Mar 22 2018 dimstar@opensuse.org
  - Fix python packaging: create python3-z3 on SLE/Leap 15.0 and
    Tumbleweed, and python-z3 on older distros.
* Tue Jan 16 2018 jslaby@suse.com
  - Update to version 4.6.0+git.20180112:
    * add missing interpreted tail during bottom-up simplification #1452
    * Added apply_result::as_expr to the C++ API. Requested here: https://stackoverflow.com/questions/48071840/get-result-of-tactics-application-as-an-expression-in-z3
    * to ascii or not to ascii #1447
    * fix build
    * avoid reset_error in dec_ref in bv_val #1443. Add BSD required template instance #1444
    * make linear search the default for theory_str
    * [CMake] Fix #1437.
    * Use noreturn attribute and __declspec version.
    * revert use of [[noreturn]]. It's not fully supported on compilers #1435
    * add noreturn attribute #1435
    * raise_exception: Annotate that this doesn't return.
    * and more...
* Mon Jan 15 2018 jslaby@suse.com
  - Look for python3_sitelib in tumbleweed

Files

/usr/bin/z3
/usr/share/doc/packages/z3
/usr/share/doc/packages/z3/README.md
/usr/share/doc/packages/z3/RELEASE_NOTES
/usr/share/licenses/z3
/usr/share/licenses/z3/LICENSE.txt


Generated by rpm2html 1.8.1

Fabrice Bellet, Sat Oct 9 11:20:14 2021