Nightly

nightly build

Changes:

• af270da Fix complete_partial_func for finite domains (#7547)
• 0919844 Fixed bug in UP (#7545)
• 17d47ca fix #7493
• 99cbfa7 Add a sharp throttle to lia2card tactic to control overhead in default tactic mode
• fd2a8a5 disable small clause generation for propagation
• 0ef2698 release
• aea4490 throttle overhead with lia2card
• d465bdb include extensionality constraints for arrays
• d6dcc51 rehearse release
• edc5679 updated release notes

See More

• 8ae24e2 update release version
• 1d622a6 Bump docker/build-push-action from 6.12.0 to 6.13.0 (#7535)
• 9557e7c Minor (#7540)
• 1ce6e66 generalize logic detection to use sub-string matching
• eb82585 increase the log level on callbacks with bit-indices that get set
• c9ac4d6 pre-flatten use list before iterating over m_unsat
• e356628 fixes based on benchmarking UFDTLIA/NIA/BV
• f1e0950 fix several crashes exposed by QF_UFDTNIA benchmark sets
• bfe4673 this check is not an invariant in the first place
• 51357f6 Add selective filter on Ackerman axioms
• c2a0919 Removed no progress case in seq-sls (#7537)
• 6d3cfb6 add eval1 functionality for replace_all
• ab43d2d fix semantics of check-int64 div operation to align with smtlib semantics
• 30d72f7 remove verbose output of overflow
• 3379155 add check for root literal assignment
• fe5d17d handle exception internally, avoid passing rationals to integer operations
• 5b175c1 fix crashes in sls_datatype
• fe713eb disable quadratic moves for non-integers as sqrt isn't currently defined for rationals
• d843081 fix mixup between sync and sls managed variables
• fa60545 fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search
• 5c2a9d9 fix pickup of new constraints
• 1676378 skip last power
• 8a7d971 Update sls_bv_lookahead.h
• 2ebc647 skip update stack items that are not Bool/bv
• 632e2b5 fix initialization of mod terms
• fd5f5fe add cmake option to turn on asan
• a8279dd reset kv map consistently with egraph
• 57a5474 revert flat default
• 72ae161 compress store array before model-eval rewriter sees it
• fe1622b sls fixes for ABV. Axiomatization required as saturation can produce conflicts by congruence closure
• 2050fc3 Preserve fingerprint in trace (#7534)
• 2d8f024 Mark fixed_eq literals as relevant (#7533)
• 63f9fda fix build
• 15ee879 fix #7532
• b6e7b80 updates to handle bugs exposed by qf-abv for local search
• 7ffed86 fix bug with handling theory symbols of bit-vector type. Happens for data-type accessors. Reported by Clemens Eisenhofer
• 09e84e0 fix crash when accessing bool-info vars, reported by Clemens Eisenhofer
• f574950 fix #7521 (#7531)
• 5634dc5 fix model construction bug: ignore non-relevant expressions when building model
• d3bf25c throttle value smt -> sls
• d4100fc fixes to update propagation.
• 04d0e94 set log level of revert repair down to 3
• 55fc57b relax out of range restrictions to handle large intervals
• 4f2272d increase log level for 'set value failed'
• 7fb6497 fix return value when in external mode bool-flip
• d4f2de7 add smt_params dependency to sls in cmakelists
• 12e8082 consolidate functionality
• a701057 align use_list with number of variables during flatten, push clause and bool_vars_of addition into clause and atom creation time.
• 7fc59b6 add recursive updates to lookahead
• 57cb988 fix gcc build
• 60fb53a fix debug build
• ecc302b fix trace build
• d805322 create separate file for expression based lookahead solver
• f6e7dcf Fix crash exposed in QF_UFNIA
• 9e8dd68 disable lookahead on compound values (fixes bug reported by Clemens), bail to rationals when there are reals.
• 053349c remove incorrect calls to VERIFY in array solver
• 0e8969c deal with compiler warnings and include value exchange prior to final check.
• ce615ee avoid repeated clauses during scoring function
• b149d1f count every lookahead as activity
• 4d33f44 enable value import in parallel mode
• e32f685 disable backoff on smt->sls value export
• beb9d2e update restart next
• ec39152 modify backoff mechanisms and theory exchange
• 3a3e176 fix build for tests
• 6893e78 add cases for new parameters for ts build
• bd566f1 Expose PARAMETER_INTERNAL and PARAMETER_ZSTRING in case API users access these #7522
• ef275ab fix #7523
• 4fce314 improve diagnostics for flips
• 72c7a9c fix re-entrancy bug between ddfw and theory solvers.
• 071c9ab Update macro_finder.cpp
• decaee8 move from justified_expr to dependent_expr by aligning datatypes
• fc9ff94 use cmake from PyPI only when system executable is not available (#7514)
• 45ff1f4 Bump docker/build-push-action from 6.10.0 to 6.12.0 (#7516)
• d944779 move away from sets and into vectors for data associated with Boolean variables
• 92ad285 use vector instead of indexed uint set for Boolean var occurrences
• eebff13 don't store full use list of clauses to avoid space overhead
• fb0eb02 use lifted bool
• 1553bae Performance improvements for seq-sls (#7519)
• 3cdcd83 fix build breaks
• a3f7541 fix #7517
• fb58342 fix unit tests, add subsampling mode for false literals
• 22e4054 add clausal lookahead to arithmetic solver as part of portfolio
• a941f5a reset m_conflict indicator on sls model
• 557c01a fix #7499 - add another way to avoid adding user-defined functions to models if user don't want it
• a5e1e7f set lookahead mode to default
• 158dea5 add case for ite
• eed3fa6 add case for ite
• f422e26 add case for ite
• 5365952 fix #7510
• a84130e prepare update stack for Boolean lookaheads
• 498c9a6 throw exceptions where sls lacks support
• 5fec07a fix unit test
• 878fd48 fix compiler warning
• 11909cf allow a plateau mode
• 076d3db fix assertion violation in the code path where the simplifier throws a memout exception
• 31d4ba0 re-introduce option to dump arithmetic lemmas to std-out
• 8515ceb add plateau option
• 648cf96 fix uninitialized variable warnings
• 27cc928 try m_fixed_var_eh
• 8c5abdf Can's fix to relevancy propagation
• 89ed4d6 use monomial variable, not the fixed variable
• a08a3ee align reslimit with ddfw
• 3c5b8bd Update parray.h
• c013365 move fixed variable propagation to nla_core/monomial_bounds
• f3e7c8c include QF_SNIA
• 943d881 fixes to hybrid mode
• 9770c00 adjust heuristic in random-inc-dec for finite domains
• 97acf71 fixup registration with new terms during internalization
• d3183fa remove binspr experiment
• 8d2b9b4 fix compiler warnings
• 85356c5 enable propagation when there are changed columns
• 558758f another stab at fixing substring interval extraction combinatorics
• fa22b64 address some build warnings.
• b780b54 optimization of sls-arith and fix build warnings
• 49dba33 fix ubuntu clang build
• 17faabe Update msvc-static-build-clang-cl.yml
• c6f58c8 updates to some_string_in_re per code review comments
• c572fc2 Regex membership (#7506)
• 9a237d5 fix misc build warnings
• d97bd48 adding lookahead mode to arithmetic sls solver
• 847278f adding global lookahead variant to sls arith solver
• f9ce41b Update theory_lra.cpp
• 270c127 sketch fixed variable callback mechanism
• c1a62d3 add missing return
• 1cb126f remove assertion that doesn't build
• 2dd4faf sketch expr_inverter approach for eliminating unconstrained regex containment.
• c7dfb61 Minor tweaks in README.md (#7504)
• ab9ea4e Add outline of elimination for regex membership constraints
• b6c0e6f Update README.md
• af0113f Disable the Code Coverage workflow
• 5c60c66 Small seq-sls fixes (#7503)
• e133a29 change score for comparisons to use hamming distance
• f77f259 fix build
• b6f45bc limit lookahead count to 20
• aed0ad3 limit lookahead count to 10
• 59fad2b shave off bv test
• e3e650a optimzie
• 6787d87 hoist update stack creation
• 5a5570e remove type check in insert_update
• 67827bf restore nyi trace
• a8b88b1 fish for nyi
• e45f186 make ite evaluation sensitive to using temporary Boolean assignment
• be5a16c fixup scoring function for sle and ule
• b3e410b fixup tabu checks to revised representation
• 71a4801 add shortcuts to convert to python objects in cases of numerals and strings
• cd41b21 fix #7501
• f6e3c5a re-enable fixed tabu
• 6b17862 bug-fixes to root-literal sls
• bed0859 bugfixes to bv-sls
• 710f757 fixup parameter handling for enabling bv-lookahead
• 05f166f add py_value to selected classes in python bindings, add mode for input-assertion based lookahead solving
• 7e4681d enable rotation
• 5a57636 use native sdiv
• bfcd755 update test file
• 1131d8d update test file
• e9c6567 throttle costly flips by reset and random
• 70f7fea flip tabu on predicate being repaired, add model rotation code
• f67e1b8 only allow flip if it doesn't increase unsat score
• 814d7f4 block flips to units
• cb61af0 fix restart counters
• 0128a1e check for bit-vector
• b12e72e extend lookhaead to work over nested terms with predicates
• 234bd40 take 1 on flip conditions
• b415b82 take 1 on flip conditions
• a511b8b disable unit tests relying on changed functionality
• 3433b14 separate fixed from bits to allow updates that break tabu
• 9837632 temper verbose output on tabu updates
• 8167892 take into account for empty vars
• 27cb81e Several changes to make sls terminate more often with length/extract operations (#7498)
• 4773bec check for null before debug assertions
• d8741b4 have apply-update check can_set instead of caller
• bcf66f2 code cleanup, add comments
• 322dcec Add 2 new API functions to get depth & groundness of exprs (#7479)
• f99e1ee Support BitVectors in the TypeScript Optimize API (#7480)
• 19c95f8 Add new string repair heuristic (#7496)
• e002c57 Fixed range regex (#7497)
• d81de1a align updated version of lookahead with legacy heuristics
• 6ea6831 fix stack overflow regression in bool_rewriter
• 3526d03 remove VERIFY output
• f41134d h
• a5bc5ed try uneven lookahead skew
• 3aacc62 api: hint the compiler that logging enabled is unlikely
• bd8c870 api: avoid some string copies when using mk_external_string
• 0b9ed92 try dual phase lookahead
• 1f55ec5 fix random update to a legal one
• c82518c include cmath to define std::pow
• b0eee16 fix double override bug in bv_lookahead, integrate with bv_eval
• 8de0005 Bugfix seq-eq sls (#7495)
• 5eb71c3 integrate lookahead v1 into repair loop
• c581714 remove dead code
• d3a6521 rely on is_sat fallback for failed repair-up, add separate file for WIP on lookahead.
• 13dcfd2 remove debug out
• c9cae77 update regex membership to be slightly better tuned
• f4ed432 try a basic heuristic that finds some string that belongs to re.
• 09825ed remove compute depth in favor of already existing get_depth
• e332904 cosmetic updates
• 85d3041 avoid platform non-reproducibility due to argument evaluation ordering
• 23c4728 remove some platform specific behavior
• 5541918 remove platform dependent print
• 4f4cafb start update with expr-inverter to handle PB
• b592ce4 reserve space in heap to avoid debug check in elim_unconstrained
• 97c70ba remove some uneeded constructors
• fb5bbb8 read laziness parameter modulo relvancy to avoid race conditions with setting relevancy = 0
• a214dc3 add some comments, fix nyis
• 65b678d use bail_out instead of early return to ensure marks are cleared
• 78ce6c1 revert relevancy override
• 3b2315d remove verbose output
• 578804a fix #7460
• 2044fb4 fix #7490
• 8dec841 add lia2card tactic as default #7483
• 4f7b6c7 always copy Microsoft.Z3.xml into package directory #7482
• 07b1ee5 mask regression on fpa by not auto-setting relevancy=0
• da6a5fa revert change to setup_context that delays it until there are assertions
• db9f45d set relevancy = 0 in auto-config mode when there are bit-vectors and no quantifiers, #7484
• 114cae5 update gcm script
• 87f7a20 Add (updated and general) solve_for functionality for arithmetic, add congruence_explain to API to retrieve explanation for why two terms are congruent Tweak handling of smt.qi.max_instantations
• e4ab294 Optimize expr_safe_replace for quantifiers when all source patterns are vars (#7481)
• c33bc2c expr_abstract: save 1 hashtable lookup per app argument
• 2f5c0a6 remove 2 unneeded lambda captures

This list of changes was auto generated.