mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity
19575 commits 22 branches 48 tags 155 MiB
Commit graph

1827 commits

Author SHA1 Message Date
Nikolaj Bjorner fa5a50c4f9 fix #7295 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-12 11:43:31 -07:00
Nikolaj Bjorner 021e8558df update minor version to 14.2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-10 19:08:34 -07:00
Nikolaj Bjorner 3c0d786e6e install setup tools for python packaging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-10 15:50:08 -07:00
Nikolaj Bjorner e05f75d74c switch to ubuntu 24 for python packaging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-09 20:53:36 -07:00
Nikolaj Bjorner 8df45b442b try ubuntu 24 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-05 13:58:39 -08:00
Nikolaj Bjorner b47ec2074b try version 75 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-05 11:26:12 -08:00
Nikolaj Bjorner 3e7f4839d1 68 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-04 17:14:10 -08:00
Nikolaj Bjorner dedfe9019d remove downlevel setup in nightly.yaml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-04 07:38:28 -08:00
Nikolaj Bjorner f698dea2b0 downlevel setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 18:25:20 -08:00
Nikolaj Bjorner e6855bb299 disable setup tool install 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 16:01:45 -08:00
Nikolaj Bjorner d714f1b6c5 update path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 14:23:33 -08:00
Nikolaj Bjorner 7eb401b891 extract paths within zip file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-03 07:15:29 -08:00
Nikolaj Bjorner 476c5ee110 improve diagnostics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 19:36:47 -08:00
Nikolaj Bjorner f74d8460f6 use single thread for win-dist 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 19:23:19 -08:00
Nikolaj Bjorner 14390eeac2 fix typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 18:44:04 -08:00
Nikolaj Bjorner 62616cf37c fixup nuget task 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-03-02 17:13:03 -08:00
Nikolaj Bjorner a97e5fcf0e fix error in mk_nuget_task.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-28 18:18:51 -08:00
Nikolaj Bjorner cd95c7e72a add diagnostics to extraction of Microsoft.pdb/xml/dll 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-28 13:55:44 -08:00
Nikolaj Bjorner fb6ec7d5e7 increase version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 15:00:26 -08:00
Nikolaj Bjorner 30dba9bde7 use down-level setup tools on hosted machines to avoid https://stackoverflow.com/questions/79252233/canonicalize-versionversion-strip-trailing-zero-false-while-doing-colcon-buil 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 14:36:16 -08:00
Nikolaj Bjorner 3c47fd96cf bump timeout for jobs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-02-18 13:41:31 -08:00
Nikolaj Bjorner 2e008a9745 Update release.yml for Azure Pipelines 2025-02-18 13:39:41 -08:00
Nikolaj Bjorner d1575af5d2 Update nightly.yaml for Azure Pipelines 
update timeout to 90
 2025-02-17 21:45:10 -08:00
Nikolaj Bjorner 0ef26983fc release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-31 17:31:37 -08:00
Nikolaj Bjorner d6dcc515eb rehearse release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-31 09:49:42 -08:00
Nikolaj Bjorner 8ae24e2b38 update release version 2025-01-31 09:29:28 -08:00
Nikolaj Bjorner decaee83f3 move from justified_expr to dependent_expr by aligning datatypes 2025-01-22 11:46:10 -08:00
Nuno Lopes 3aacc62229 api: hint the compiler that logging enabled is unlikely 2024-12-28 09:52:36 +00:00
Nuno Lopes bd8c870bbe api: avoid some string copies when using mk_external_string 2024-12-28 09:42:54 +00:00
Nikolaj Bjorner 4f7b6c794e always copy Microsoft.Z3.xml into package directory #7482 2024-12-21 13:10:05 +01:00
Nikolaj Bjorner a6e59ea45e fix build flags for release.yaml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-16 04:41:29 +01:00
Nikolaj Bjorner a97ad76bb6 publish pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-15 13:00:50 -08:00
Nikolaj Bjorner e40972b7f7 Update release.yml 
disable publish to pypi during release dry-runs
 2024-12-15 05:55:48 -08:00
Nikolaj Bjorner 91dc02d862
Sls (#7439) 
* reorg sls

* sls

* na

* split into base and plugin

* move sat_params to params directory, add op_def repair options

* move sat_ddfw to sls, initiate sls-bv-plugin

* porting bv-sls

* adding basic plugin

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add sls-sms solver

* bv updates

* updated dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* updated dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use portable ptr-initializer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move definitions to cpp

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use template<> syntax

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix compiler errors for gcc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Bump docker/build-push-action from 6.0.0 to 6.1.0 (#7265)

Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.0.0 to 6.1.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.0.0...v6.1.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

* set clean shutdown for local search and re-enable local search when it parallelizes with PB solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Bump docker/build-push-action from 6.1.0 to 6.2.0 (#7269)

Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.1.0 to 6.2.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.1.0...v6.2.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

* Fix a comment for Z3_solver_from_string (#7271)

Z3_solver_from_string accepts a string buffer with solver
assertions, not a string buffer with filename.

* trigger the build with a comment change

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove macro distinction #7270

* fix #7268

* kludge to address #7232, probably superseeded by planned revision to setup/pypi

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add new ema invariant (#7288)

* Bump docker/build-push-action from 6.2.0 to 6.3.0 (#7280)

Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.2.0 to 6.3.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.2.0...v6.3.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>

* merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix unit test build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove shared attribute

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove stale files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix build of unit test

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes and rename sls-cc to sls-euf-plugin

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* testing / debugging arithmetic

* updates to repair logic, mainly arithmetic

* fixes to sls

* evolve sls arith

* bugfixes in sls-arith

* fix typo

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* bug fixes

* Update sls_test.cpp

* fixes

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* refactor basic plugin and clause generation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes to ite and other

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* updates

* update

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix division by 0

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable fail restart

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable tabu when using reset moves

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* update sls_test

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add factoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes to semantics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* re-add tabu override

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* generalize factoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix bug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove restart

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable tabu in fallback modes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* localize impact of factoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* delay factoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* flatten products

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* perform lookahead update + nested mul

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable nested mul

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable nested mul, use non-lookahead

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* make reset updates recursive

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* include linear moves

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* include 5% reset probability

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* separate linear update

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* separate linear update remove 20% threshold

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove linear opt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* enable multiplier expansion, enable linear move

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use unit coefficients for muls

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable non-tabu version of find_nl_moves

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove coefficient from multiplication definition

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* reorg monomials

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add smt params to path

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid negative reward

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use reward as proxy for score

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use reward as proxy for score

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use exponential decay with breaks

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use std::pow

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes to bv

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes to fixed

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixup repairs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* reserve for multiplication

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixing repair

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* include bounds checks in set random

* na

* fixes to mul

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix mul inverse

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes to handling signed operators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* logging and fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* gcm

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* peli

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Add .env to gitignore to prevent environment files from being tracked

* Add m_num_pelis counter to stats in sls_context

* Remove m_num_pelis member from stats struct in sls_context

* Enhance bv_sls_eval with improved repair and logging, refine is_bv_predicate in sls_bv_plugin

* Remove verbose logging in register_term function of sls_basic_plugin and fix formatting in sls_context

* Rename source files for consistency in `src/ast/sls` directory

* Refactor bv_sls files to sls_bv with namespace and class name adjustments

* Remove typename from member declarations in bv_fixed class

* fixing conca

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Add initial implementation of bit-vector SLS evaluation module in bv_sls_eval.cpp

* Remove bv_sls_eval.cpp as part of code cleanup and refactoring

* Refactor alignment of member variables in bv_plugin of sls namespace

* Rename SLS engine related files to reflect their specific use for bit-vectors

* Refactor SLS engine and evaluator components for bit-vector specifics and adjust memory manager alignment

* Enhance bv_eval with use_current, lookahead strategies, and randomization improvements in SLS module

* Refactor verbose logging and fix logic in range adjustment functions in sls bv modules

* Remove commented verbose output in sls_bv_plugin.cpp during repair process

* Add early return after setting fixed subterms in sls_bv_fixed.cpp

* Remove redundant return statement in sls_bv_fixed.cpp

* fixes to new value propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Refactor sls bv evaluation and fix logic checks for bit operations

* Add array plugin support and update bv_eval in ast_sls module

* Add array, model value, and user sort plugins to SLS module with enhancements in array propagation logic

* Refactor array_plugin in sls to improve handling of select expressions with multiple arguments

* Enhance array plugin with early termination and propagation verification, and improve euf and user sort plugins with propagation adjustments and debugging enhancements

* Add support for handling 'distinct' expressions in SLS context and user sort plugin

* Remove model value and user sort plugins from SLS theory

* replace user plugin by euf plugin

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove extra file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Refactor handling of term registration and enhance distinct handling in sls_euf_plugin

* Add TODO list for enhancements in sls_euf_plugin.cpp

* add incremental mode

* updated package

* fix sls build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* break sls build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix build

* break build again

* fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixing incremental

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid units

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixup handling of disequality propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fx

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* recover shift-weight loop

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* alternate

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* throttle save model

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* allow for alternating

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix test for new signature of flip

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* bug fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* restore use of value_hash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adding dt plugin

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* dt updates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* added cycle detection

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* updated sls-datatype

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Refactor context management, improve datatype handling, and enhance logging in sls plugins.

* axiomatize dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add missing factory plugins to model

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixup finite domain search

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixup finite domain search

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* redo dfs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixing model construction for underspecified operators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes to occurs check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixup interpretation building

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* saturate worklist

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* delay distinct axiom

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* adding model-based sls for datatatypes

* update the interface in sls_solver to transfer phase between SAT and SLS

* add value transfer option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* rename aux functions

* Track shared variables using a unit set

* debugging parallel integration

* fix dirty flag setting

* update log level

* add plugin to smt_context, factor out sls_smt_plugin functionality.

* bug fixes

* fixes

* use common infrastructure for sls-smt

* fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove declaration of context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add virtual destructor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* reorder inclusion order to define smt_context before theory_sls

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* change namespace for single threaded

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* check delayed eqs before nla

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use independent completion flag for sls to avoid conflating with genuine cancelation

* validate sls-arith lemmas

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* bugfixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add intblast to legacy SMT solver

* fixup model generation for theory_intblast

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* mk_value needs to accept more cases where integer expression doesn't evalate

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use th-axioms to track origins of assertions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add missing operator handling for bitwise operators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add missing operator handling for bitwise operators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* normalizing inequality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add virtual destructor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* rework elim_unconstrained

* fix non-termination

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use glue as computed without adjustment

* update model generation to fix model bug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes to model construction

* remove package and package lock

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix build warning

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use original gai

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: dependabot[bot] <support@github.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
Co-authored-by: Sergey Bronnikov <estetus@gmail.com>
Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: LiviaSun <33578456+ChuyueSun@users.noreply.github.com>
 2024-11-02 12:32:48 -07:00
Nikolaj Bjorner 56b706ac55 fixes for #7420 #7405 2024-10-13 15:52:13 -07:00
Nikolaj Bjorner 7a0b58bcd5 increment minor version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-10 17:27:07 -07:00
Nikolaj Bjorner 6e3b99fb9e downgrade to macos13 in builds until fully supported by pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-10 14:19:23 -07:00
Nikolaj Bjorner 5dc1b1acd4 remove hard-wired osx=11.0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-09 13:01:27 -07:00
Nikolaj Bjorner 48aa2f6988 setup python dist to remove internal build suffix for macos 2024-10-09 12:47:17 -07:00
Nikolaj Bjorner 30b4fe69e4 2nd attempt to use uniform java library location under bin #7406 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 10:05:09 -07:00
Nikolaj Bjorner b65afd41ed attempt to use uniform java library location under bin #7406 2024-09-30 08:58:21 -07:00
Nikolaj Bjorner 2ac6f8bb06 increment minor revision number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 07:28:20 -07:00
Nikolaj Bjorner c2b2626e9b remove --java option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 07:27:15 -07:00
Nikolaj Bjorner 2123d38371 Update nightly.yaml for Azure Pipelines 2024-09-30 04:16:29 +01:00
Nikolaj Bjorner fc1c6b48ce try to build java on linux/arm nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-30 04:14:12 +01:00
Nikolaj Bjorner 9a8ff74924 update version number and release notes 2024-09-27 17:49:05 +01:00
Nikolaj Bjorner f4452a0348 pypi publish 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-26 21:34:55 +01:00
Nikolaj Bjorner 649c36aa03 align nightly and release yamls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-26 13:59:17 +01:00
Nikolaj Bjorner 8d831a1adf set to macos latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-26 11:22:18 +01:00
Nikolaj Bjorner b39bcd6a42 remove ubuntu20 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-26 11:20:54 +01:00