1654 commits

Author	SHA1	Message	Date
Lev Nachmanson	a5dd59fdfb	fix the build	2025-02-11 12:23:00 -10:00
Lev Nachmanson	a1a01b9da6	move some functionality from int_solver to int_solver::imp	2025-02-11 12:23:00 -10:00
Lev Nachmanson	889292472e	fix the build	2025-02-11 12:23:00 -10:00
Lev Nachmanson	3d6cc64e2e	prepare for calling diophantine equations	2025-02-11 12:23:00 -10:00
Lev Nachmanson	097a25ebfe	add parameter to control calling diophantine equations ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-02-11 12:23:00 -10:00
Nikolaj Bjorner	648cf9602e	fix uninitialized variable warnings	2025-01-14 13:54:05 -08:00
Lev Nachmanson	27cc928631	try m_fixed_var_eh ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2025-01-14 07:11:53 -10:00
Nikolaj Bjorner	89ed4d6c8b	use monomial variable, not the fixed variable	2025-01-14 07:27:59 -08:00
Nikolaj Bjorner	c01336553e	move fixed variable propagation to nla_core/monomial_bounds	2025-01-13 18:18:53 -08:00
Nikolaj Bjorner	8d2b9b41fd	fix compiler warnings	2025-01-12 13:39:13 -08:00
Nikolaj Bjorner	85356c5548	enable propagation when there are changed columns ... - to fix bug reported by Nikhil Swamy/F* - deal with some compiler warnings by adding annotations	2025-01-12 13:30:31 -08:00
Nikolaj Bjorner	9a237d55ca	fix misc build warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2025-01-11 17:41:24 -08:00
Nikolaj Bjorner	270c127407	sketch fixed variable callback mechanism	2025-01-08 12:50:46 -08:00
Nikolaj Bjorner	87f7a20e14	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 ... Add API solve_for(vars). It takes a list of variables and returns a triangular solved form for the variables. Currently for arithmetic. The solved form is a list with elements of the form (var, term, guard). Variables solved in the tail of the list do not occur before in the list. For example it can return a solution [(x, z, True), (y, x + z, True)] because first x was solved to be z, then y was solved to be x + z which is the same as 2z. Add congruent_explain that retuns an explanation for congruent terms. Terms congruent in the final state after calling SimpleSolver().check() can be queried for an explanation, i.e., a list of literals that collectively entail the equality under congruence closure. The literals are asserted in the final state of search. Adjust smt_context cancellation for the smt.qi.max_instantiations parameter. It gets checked when qi-queue elements are consumed. Prior it was checked on insertion time, which didn't allow for processing as many instantations as there were in the queue. Moreover, it would not cancel the solver. So it would keep adding instantations to the queue when it was full / depleted the configuration limit.	2024-12-19 23:27:57 +01:00
Nikolaj Bjorner	8f5658b77d	add another baseline heuristic for string equalities, add cases for array axioms. ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-12-09 15:55:19 -08:00
Nikolaj Bjorner	1ab0962d43	partial fix to make computed term integer well-formed for solve_for functionality	2024-12-05 17:10:52 -08:00
Nikolaj Bjorner	05e053247d	add facility to solve for a linear term over API	2024-11-30 09:34:27 -08:00
Nikolaj Bjorner	92065462b4	use std::exception as base class to z3_exception ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-11-04 11:08:15 -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
Nuno Lopes	3586b613f7	remove default destructors	2024-10-02 22:20:12 +01:00
Nikolaj Bjorner	d686e92bfa	disambiguate ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-10-02 10:45:16 -07:00
Nikolaj Bjorner	93ff89bf98	add == for const_ref and ref to disambiguate equality.	2024-10-02 10:45:16 -07:00
Nikolaj Bjorner	551cc53a2f	fix un-intialized variable warnings	2024-09-30 15:08:33 -07:00
Nikolaj Bjorner	826835fd7c	fixes to build warnings	2024-09-30 08:23:31 -07:00
Nuno Lopes	499ed5d844	remove unneeded iterator functions	2024-09-23 12:59:04 +01:00
Nuno Lopes	737c2208fa	delete more default constructors ... reduces code size by 0.1%	2024-09-23 12:59:04 +01:00
Nuno Lopes	a62fede64b	remove a few default constructors	2024-09-23 08:17:58 +01:00
Lev Nachmanson	342dccdc02	correctly process cancellation in gomory cuts ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2024-09-19 14:11:27 -07:00
Nikolaj Bjorner	48712b4f60	Add initial value setting for variables in Z3 API, solver, and optimize modules	2024-09-18 16:13:15 +03:00
David Seifert	2ce89e5f49	Gcc 15 two phase (#7313) ... * Fix `-Wclass-memaccess` * Fix for GCC 15 two-phase lookup * GCC 15 is more aggressive about checking dependent names: https://gcc.gnu.org/git/?p=gcc.git;a=commitdiff;h=r15-2117-g313afcfdabeab3 Bug: https://bugs.gentoo.org/936634	2024-07-29 11:07:10 -07:00
Lev Nachmanson	e4b3df2189	remove unused column_info.h ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2024-06-17 12:58:16 -07:00
Nikolaj Bjorner	35c1cacf44	fix #7248	2024-06-12 14:26:35 -07:00
Bruce Mitchener	904a50fe49	Fix compilation error in column_info (#7235) ... Reference to `m_low_bound` should be `m_lower_bound`.	2024-05-27 09:19:29 +04:00
Nikolaj Bjorner	8fe357f1f2	Nlsat simplify (#7227) ... * dev branch for simplification Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * bug fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * bugfixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix factorization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * separate out simplification functionality * reorder initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * reorder initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Update README.md * initial warppers for seq-map/seq-fold Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * expose fold as well Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add C++ bindings for sequence operations Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add abs function to API Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add parameter validation to ternary and 4-ary functions for API #7219 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add pre-processing and reorder Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add pre-processing and reorder Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-05-14 22:19:33 -07:00
Nikolaj Bjorner	04c55c34e5	fix unsoundness bug ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-05-01 14:45:15 -07:00
Nikolaj Bjorner	39dc8861ee	expose comparisons with polynomials, incremental way to extract variables	2024-04-30 16:59:50 -07:00
Nikolaj Bjorner	bc577b93ae	refine precision before taking closest integral value.	2024-04-30 16:58:22 -07:00
Nikolaj Bjorner	bebcd94703	enable logging nla lemmas ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-04-25 10:29:34 -04:00
Nikolaj Bjorner	974ea7b68d	maintain ownership of dependency	2024-04-10 17:57:14 -07:00
Nikolaj Bjorner	7b8980f82d	fix regression introduced when testing ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-04-09 11:17:03 -07:00
Nikolaj Bjorner	8d0e66b3e3	fix regression introduced when testing ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-04-09 11:16:34 -07:00
Nikolaj Bjorner	9a681b1a37	reorg sls ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-04-09 10:44:53 -07:00
Nikolaj Bjorner	361e04a18e	port fixes to intblast ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-03-09 10:27:12 -08:00
Nikolaj Bjorner	bc70282a18	mute some compiler warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-02-03 15:42:06 -08:00
Nikolaj Bjorner	5cac9b84e4	fix build warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-02-01 09:36:52 -08:00
Nikolaj Bjorner	bdb9106f99	Api (#7097) ... * rename ul_pair to column Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * t Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * simple test passed * remove an assert * relax an assertion * remove an obsolete function Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * access a term by the term column * remove the column index from colunm.h * remove an unused method * remove debug code * fix the build of lp_tst Signed-off-by: Lev Nachmanson <levnach@hotmail.com> --------- Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com>	2024-01-24 16:05:18 -08:00
Nikolaj Bjorner	be7856c57d	fix #7027 ... TODO: review old nlsat bugs for effect of this fix.	2024-01-23 14:56:15 -08:00
Nikolaj Bjorner	125a82bea5	improved diagnostics	2024-01-22 16:23:55 -08:00
Nikolaj Bjorner	839b7101ae	add ability to multiply term	2024-01-22 15:48:45 -08:00
Nikolaj Bjorner	910b3023c2	free memory the clean way ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2024-01-20 14:01:01 -08:00