Spellcheck and small fixes #165
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
@microsoft-github-policy-service agree |
NikolajBjorner
added a commit
to Z3Prover/z3
that referenced
this pull request
Jan 12, 2024
spellcheck from microsoft/z3guide#165
NikolajBjorner
added a commit
to Z3Prover/z3
that referenced
this pull request
Jan 12, 2024
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
| @@ -127,7 +127,7 @@ cut.redundancies | bool | integrate redundancy checking of cuts | true | |||
| cut.xor | bool | extract xors from clauses for cut simplification | false | |||
| ddfw.init_clause_weight | unsigned int | initial clause weight for DDFW local search | 8 | |||
| ddfw.reinit_base | unsigned int | increment basis for geometric backoff scheme of re-initialization of weights | 10000 | |||
| ddfw.restart_base | unsigned int | number of flips used a starting point for hessitant restart backoff | 100000 | |||
There was a problem hiding this comment.
these strings are extracted from z3 source. Spell check fixes are ported to master.
Z3Prover/z3@3381fd2
|
probably remove yarn.lock from pr |
clrpackages
pushed a commit
to clearlinux-pkgs/Z3
that referenced
this pull request
May 6, 2024
Bruce Mitchener (10):
tptr.h: Include `<cstdint>` once rather than twice. (#7051)
Use `override` more. (#7059)
Use `noexcept` more. (#7058)
Fix some typos. (#7075)
Fix some typos. (#7115)
ci: Update `microsoft/setup-msbuild` to `v2` from `v1.3`. (#7119)
Fix some typos in identifiers. (#7118)
Fix typos. (#7137)
ci: Stop using deprecated `::set-output`. (#7136)
ci: Really fix set-output. (#7138)
Cal Jacobson (1):
conditionally depend on importlib_resources (#7116)
Christoph M. Wintersteiger (4):
Disable Python compilation cache during build (#7052)
Disable Python compilation cache during build (#7057)
Fix bug in fp.round_to_integral (#7060)
Add Z3_get_estimated_alloc_size to OCaml API (#7068)
Jakob Rath (3):
tptr: add pointer tagging templates (#7067)
Vector updates from polysat branch (#7066)
Merge shared parts from polysat branch (#7063)
John Fleisher (2):
Update nightly.yaml for Azure Pipelines (#7139)
convert formatting tabs to spaces (#7140)
Lev Nachmanson (29):
a simple version of choosing a column for gomory cut
remove unnecessary assignments
change some TRACE statements
remove an empty line
refactor: move gomory functionaly from int_solver to gomory
revert smt_enode
fix the build
adding the polarity bound
create bounds for gomory cuts with big numbers
use vector instead of unordered_map in gomory
add parameter lp_settings.m_gomory_simplify
cleanup
bug fix in gomory polarity
move a TRACE statement
return conflict on an empty term in Gomory cuts
remove simplify_inequality from gomory.cpp
fix a bug in polarity
take the coefficient from cut_result, not lia
do not delay update for the polar case
remove a blank line
address Nikolaj's comments in Gomory cut
add explanations and fix polarity
avoid duplicate explanations
fix dependencies for Gomory polarity
remove an unused declaration
change the definition of Gomory row
force int bound on int columns, call term_is_int() after subst
take care of strategy undecided, Nikolaj's comments
replace DEBUG_CODE by #ifdef Z3DEBUG in nlsat
Nikolaj Bjorner (234):
update minor version number
fix divergence reported by Guido Martinez
kludge to fixup osver in python for Mac
fix #7049
try fix suggested in #7041
try add name to project
add version
follow error message to put dependencies in setup args
import updates to rational from polysat
port updates from poly/polysat
try adding readme again
add readme under content
nuget spec: does this work?
fix character
remove readme reference, add arm64 build to nightly
nightly
fix #7053
Revert "Disable Python compilation cache during build (#7052)" (#7054)
fiddle with what gets added to win-arm64
port updated pdd from polysat
Add intblast solver
revert to standard solver
add rewriters for and
intblast with lazy expansion of shl, ashr, lshr
remove windowsArm64 from nightly
fix bugs in elim-unconstr2 and fix bugs in intblast_solver
fixes to intblast encoding and more arithmetic rewriters
port Jakob's update to union_find from polysat branch
port Jakob's update to bv_internalize
fix typos
fixes
pin expressions to fix unsound behavior
add ability to log selected bv rewrites
reset model converter between rounds to elim-unconstrained.
Create Windows.yml
Update Windows.yml
Update Windows.yml
Update Windows.yml
Update Windows.yml
Update Windows.yml
Update Windows.yml
gc expressions in the scope of updates, not old expressions
Update Windows.yml
Update Windows.yml
Update Windows.yml
fix string
fix string
add path n prefix
remove reference to matrix bindings to see if it works
remove reference to matrix bindings to see if it works
Update Windows.yml
rudimentary bin cover solver using the user propagator
improve add bin/item functions
bugfix on slack
move sls core functionality to be independent of tactic
missing cmake list
add missing dependencies
remove reference to tactic.h
add sub and super-slice functionality directory to euf-bv-plugin
Add branch and bound solver, for fun
readd big cuts
port improvements to arith rewriter
fix
add validation option for debugging regressions
import updates from poly branch
update Julia versions
try to remove version spec
try to remove version spec
create as_bin as_hex wrappers for display
Update sat_params.pyg
spell check from microsoft/z3guide#165
deleted parameter
fix #7084
fix #7085
fix #7081
Update z3_api.h
pin expression passed to validate_eq
remove unused code
encapsulate mpz a bit more
add explicit move constructor to deal with unit test regression test-z3 algebraic on Windows/debug -
encapsulate anum functionality
free memory the clean way
free memory the clean way
add Windows build
add status badge for windows build, remove windows build from Azure pipelines
prepare for release
track quantifier instantiation method in proof hint #7080
update release scripts and notes
use assignment
prepare for printing more cases of root objects in SMT
add ability to multiply term
add diagnostics option to new arithmetic solver
improved diagnostics
fix #7027
use while (true) in do loops with continue
prepare for handling integer intervals
prepare for integer intervals
fix build
update minor version number
Api (#7097)
attempting to build ARM
update cmake build
Update mk_win_dist_cmake.py
update java install/build
update java install/build
updating java cmake scrip
fix #7102
fix #7103
fix #7101
update win-dist
special purpose dotnet copy
update path for win distributions
adapt paths to new distribution
move installation directories to under bin
add download stage for arm64
build Julia for x64
build Julia for x64
remove optional Julia build
update release scripts
fix #7105
porting unix distribution script to cmake
fix #7098
add warning messages for #7100
move nightly builds of Unixes to use cmake
install ninja
add line continuations to nightly.yaml
cd to dist in nightly.yaml
update nightly
update nightly
fix #7107
Update nightly.yaml for Azure Pipelines
Update nightly.yaml for Azure Pipelines
Update nightly.yaml for Azure Pipelines
Update nightly.yaml
update ubuntu builds
update ubuntu builds
Update nightly.yaml
remove explicit option for shared build, set to Release mode. .so artifacts take 800MB in distribution
fix build warnings
move to use release.yml version for windows build
disable arm64 nightly
update folder names to align with mk_win_dist_cmake
update folder names to align with mk_win_dist_cmake
rename
remove period
include variable ReleaseVersion in Nightly
include variable ReleaseVersion in Nightly
add 'dist' to folder path
add back legacy build-win-signed
add back legacy build-win-signed
fixing paths and re-add arm64
move windows builds to use mk_win_dist_cmake in nightly
move windows builds to use mk_win_dist_cmake in nightly
update mk-win-dist-cmake
update mk-win-dist-cmake
update build-win-signed-cmake
update build-win-signed-cmake
fix typo
port updates to egraph from poly
port remaining egraph update
mute some compiler warnings
copy over dotnet files
update assembly names
update assembly names
add option to persist clauses #7109
bypass replaying new clause within propagation
add clause persistence to sat/smt solver
move libz3.so from lib to bin, remove lib from distribution
update self-validator to handle root expressions
add note that the encoding is a first approximation
distinguish vs-arch from arch identifier
typo
add todo note, and log more lemmas
finish encoding of n'th root
improve logging
include debug output
move files from lib and java directory to bin
allow callbacks to be nested
#7117
fix #7121
fix generic example
throttle squash-store #7134
prepare for 12.6
Update coverage.yml
enable release publish
update versions
detect arm64 for manylinux setup
Revert "For many linux build, use aarch64 instead of arm64 (#7147)" (#7148)
initial stab at new bv-sls based on repair actions
save
updates
add tests for evaluation
n/a
na
fixes based on unit tests
na
use tuned gcd to compute mult inverse
bugfixes
fixes and checks
bugfixes
fix alias bug
bugfixes
bugfixes, adding plugin solver
prepare for sls experiment
include thread
update python build dependencies
move to hide bits
move to hide bits
reorg to use datatypes
na
na
fb
move to single path mode for search
remove bw setting
na
na
updates to multiplication
add eval field to sls-valuation to track temporary values.
bugfixes
na
na
na
na
na
updates
fix test
na
fix alias bug
na
add aacrhc
remove test
update release notes
update release notes
add download of Arm64 to python packaging
Nuno Lopes (11):
remove a few string copies
remove a few string copies
shrink ast's app by 8 bytes on 64-bit platforms when number of args > 0
tmp_enode: don't heap allocate an app. store it inline instead.
fix debug build
revert last two commits; MSVC doesn't like to statically allocate flexible arrays
reduce memory allocs in params
some code simplifications in mpn
remove unnecessary parameter copies
fix test build
fix #7143: type punning in test
Steven Moy (7):
Add arm64 for linux python wheels to nightly (#7145)
For many linux build, use aarch64 instead of arm64 (#7147)
Put in workaround to rename manylinux_arm64 to manylinux_aarch64 (#7149)
Handle cross compile within manylinux (#7150)
Add LinuxBuildsArm64 ci azure-pipelines for testing (#7152)
Downgrade arm cross compile toolchain to glibc 2.34 (#7153)
Add LinuxBuildsArm64 to python wheels in release (#7155)
Thomas Haas (2):
Fixes in Java's User Propagator (#7088)
Improved Java phantom references (#7131)
Yisu Remy Wang (2):
Expose forall and exists to Julia (#7099)
Improve instructions for working with the Julia API (#7108)
dependabot[bot] (3):
Bump actions/upload-artifact from 3 to 4 (#7065)
Bump microsoft/setup-msbuild from 1.1 to 1.3 (#7071)
Bump mymindstorm/setup-emsdk from 13 to 14 (#7095)
zapashcanon (1):
some code cleaning and complexity improvements (#7133)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Greetings! Going through the guide; here are some small updates and spelling fixes.