mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-13 04:13:01 +00:00
Code Activity
z3/src/test
History
Lev Nachmanson 63f05ff6e6
Merge with branch lws (#8498) 
* t0

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

* t1

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

* t2

* scaffoldin

* scaffolding

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

* closer to the paper

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

* more scaffolding

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

* define symbolic_interval

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

* t

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

* use std::map instead of std::unordered_map

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

* more accurate init of the relation between polynomial properties

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

* t

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

* pass anum_manager to levelwise, crash on sign

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

* pass pmanager

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

* create free function display functions

* use new display functions

* pass nlsat::solver to levelwise

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

* add trace tag for levelwise

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

* refactor

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

* refactor

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

* define indexed root expression

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

* refact lws

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

* refact lws

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

* refactor lws

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

* trying to figure out right indices

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

* rename explain::main_operator to compute_conflict_explanation

* preprocess the input of levelwise to drop a level

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

* ttt

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

* renaming

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

* rename

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

* work on seed_properties

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

* work on seed_properties

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

* work on seed_properties

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

* move a comment

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* simplify

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

* simplify

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

* debug

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

* refactor and assert _irreducible

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

* add a display method

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* simplify

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

* simplify

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

* remove erase_from_Q

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

* ignore holds properties

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* t

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

* got a section

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

* t

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

* introdure mk_prop

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

* t

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

* t

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

* remove a parameter

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

* t

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

* t

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

* t

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

* t

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

* add parameter to suppress/enable levelwise

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

* t

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

* comment

* t

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

* fixing factoring and hitting NOT_IMPLEMENTED on ir_ord

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

* adding ir_ord

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

* produce more literals but creating sat lemmas

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

* t

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

* try iterative factoring

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

* new file

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

* create irreducible polynomials on init

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

* add a guard on m_fail

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

* t

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

* process level 0 as well

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

* remove a warning

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

* debug

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

* t

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

* prepare to fill the relation

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

* filling the relation

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

* separate the lower and upper bound root functions

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

* fix an assert statement

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

* create a better queue on properties

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

* normalize before pushing

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

* relax an assert

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

* rebase with master

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

* add stats to track levelwise calls

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

* catch and fail on an exception

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

* fix a bug in Rule 4.2

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

* remove debug instruction

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

* call levelwise on a correct set of polynomials

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

* cosmetics

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

* use polynomial_ref instead of poly*

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

* do not refactor again multivariate polynomials

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

* canonicalize polinomals in todo_set

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

* t

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

* t

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

* canonicalize polynomials in nlsat

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

* t

* normalize polynomials

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

* try not to fail in add_sgn_inv_leading_coeff_for

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

* use the cache consistently

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

* unsound state

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

* unsound state

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

* handle the zero case in add_ord_inv_resultant

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

* optimizations by using cached psc

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

* t

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

* make normalize optional

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

* Revert "make normalize optional"

This reverts commit c80cfb0b8e.

* t

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

* cleanup and more caching

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

* t

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

* better sort of root functions

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

* index bug

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

* with resultant calculation ignore one of p and q with a common root

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

* fix the duplicate bug

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

* t

* simplify by removing back propagation

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

* t

* t

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

* t

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

* hook up different relation build strategies for lws

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

* introduce isolate_root_closest

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

* fix a bug with non-adding ldcf

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

* simple choice of non-vanishing

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

* restore choose_non_zero_coeff

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

* efficient sort of root functions

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

* avoid ldcf with the projective theorem

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

* omit some disc

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

* use std_vector more

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

* avoid a compare call

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

* try optimizing build_interval_and_relation

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

* discard a discriminant only in the section case

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

* refactor

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

* refactor

* refactor

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

* cache the polynomial roots

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

* Revert "cache the polynomial roots"

This reverts commit aefcd16aaa.

* ignore const non-null witnesses

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

* toward more like SMT-RAT split

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

* align with SMT-RAT

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

* t

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

* disables some heuristics in section

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

* Implement chain noLdcf optimization matching SMT-RAT

Add find_partition_boundary() helper to locate the boundary between
lower and upper root partitions in m_rfunc.

Implement compute_omit_lc_sector_chain() and compute_omit_lc_section_chain()
following SMT-RAT's OneCellCAD.h logic:
- Omit ldcf for extreme of lower chain (index 0) if it appears on upper side
- Omit ldcf for extreme of upper chain (last index) if it appears on lower side

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Restrict noDisc optimization to section_lowest_degree only

Match SMT-RAT behavior: noDisc (discriminant omission for leaves
connected only to section polynomial) is only applied for
sectionHeuristic == 3 (lowest_degree), not for biggest_cell or chain.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Cache partition boundary to avoid repeated algebraic number comparisons

Store the partition boundary (index of first root > sample) in
relation_E after sorting root functions. Use this cached value
in compute_omit_lc_sector_chain() and compute_omit_lc_section_chain()
instead of recomputing via algebraic number comparisons.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Refactor levelwise: consolidate partition indices into m_l_rf/m_u_rf

Replace scattered local l_index/u_index parameters and m_partition_boundary
with two impl members:
- m_l_rf: position of lower bound in m_rel.m_rfunc
- m_u_rf: position of upper bound in m_rel.m_rfunc (UINT_MAX in section case)

This simplifies the code by:
- Removing parameter passing through multiple function calls
- Removing redundant m_partition_boundary from relation_E
- Making the partition state explicit in impl

Also clean up nlsat_explain.cpp to trust root_function_interval invariants:
- Section case: assert l and l_index are valid instead of defensive check
- Sector bounds: !l_inf()/!u_inf() implies valid polynomial and index

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Refactor levelwise: use member variables for per-level state

Replace local variables and function parameters with member variables:
- m_level_ps: polynomials at current level (owned)
- m_level_tags: tags for each polynomial (owned)
- m_witnesses: non-zero coefficient witnesses
- m_poly_has_roots: which polynomials have roots
- m_todo: pointer to todo_set

Functions now use these member variables directly:
- extract_max_tagged() fills m_level_ps/m_level_tags and sets m_level
- process_level() and process_top_level() are now parameterless
- All helper functions use member variables instead of parameters

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Refactor levelwise: change m_todo from pointer to member

- Change m_todo from todo_set* to todo_set
- Initialize m_todo in constructor initializer list
- Use m_todo.reset() in single_cell_work instead of creating local todo_set
- Replace pointer access (m_todo->) with member access (m_todo.)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* Add dynamic heuristic selection for levelwise projection

Implement weight-based dynamic selection of projection heuristics in
levelwise CAD. The weight function w(p, level) = deg(p, level) estimates
projection complexity, with w(res(a,b)) ≈ w(a) + w(b).

At each level, all three heuristics (biggest_cell, chain, lowest_degree)
are evaluated and the one with minimum estimated resultant weight is
selected. When fewer than 2 root functions exist, the default heuristic
is used since all produce equivalent results.

Add parameter nlsat.lws_dynamic_heuristic (default: true) to enable or
disable dynamic selection. When disabled, the static heuristic from
lws_sector_rel_mode/lws_section_rel_mode is used.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

* local optimization

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

* call omit_lc only when both bounds are present

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

* use std_vector

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

* remove m_level_tags

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

* count added lcs in the heuriistic estimates

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

* add both side spanning tree heuristic

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

* Fix nlsat projection bug: ensure polynomials with assumptions are also projected

When polynomials are added as assumptions (via add_assumption or ensure_sign),
they must also be added to the projection set (m_todo) to ensure proper cell
construction. Previously, assumptions were added without corresponding projection,
leading to unsound lemmas.

Fixes:
1. In normalize(): collect lower-stage polynomials in m_lower_stage_polys and
   add them to m_ps in main() before projection.
2. In ensure_sign(): call insert_fresh_factors_in_todo(p) after adding assumption.
3. In project_cdcac(): when levelwise fails, use flet to set m_add_all_coeffs=true
   for the fallback projection.

* Remove deprecated project_original and cell_sample parameter

- Remove project_original() function from nlsat_explain.cpp
- Remove m_sample_cell_project member variable
- Simplify project() to just call project_cdcac()
- Remove cell_sample parameter from nlsat_params.pyg
- Update nlsat_solver.cpp to remove cell_sample() references
- Update nlsat_explain.h constructor signature

* Enforce bound polynomial LC protection in compute_omit_lc functions

Move the invariant that bound-defining polynomials must never have their
LC omitted from add_level_projections_sector() into the source functions:
- compute_omit_lc_both_sides()
- compute_omit_lc_chain_extremes()

This centralizes the protection and removes the redundant override check.

* fix the build

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

* bug fixes

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

* restore a deleted function

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

* remove sector/section stats

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

* Simplify levelwise: remove chain/lowest_degree heuristics, unify relation
   mode

     - Remove chain and lowest_degree heuristics, keep only biggest_cell and spanning_tree
     - Unify m_sector_relation_mode and m_section_relation_mode into single m_rel_mode
     - Remove lws_rel_mode, lws_sector_rel_mode, lws_section_rel_mode, lws_dynamic_heuristic params
     - lws_spt_threshold < 2 now disables spanning tree (single tuning parameter)
     - Restore noDisc optimization for spanning_tree leaves connected to boundary
     - Add noDisc for sector with same_boundary_poly (treat like section case)
     - Significant code reduction (~390 lines removed)

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

* fix bug with skipping too many discriminants

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

* t

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

* simplifications and bug fixes in lws, use static_tree only with sector + different bound polynomials, otherwise us biggest cell

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

* bug fixes and cleanup

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

* add the discriminant in degenerated case

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

* fix a bug with skipping a vanishing discriminant

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

* remove the unsound optimization

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

* fiddle with heuristics

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

* preserve random seed in nlsat_solver::check_lemma

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

* fix a typo in poly_has_roots

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

* add lc(p) and disc(p) for a rootless p in section case

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

* remove warnings

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

* untracking .beads

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

* fix the explosion in m_todo with lws.false

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

* fix issue 8397

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

* set default to nlsat.lws=false for the merge with master

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

* set nlsat.lws=true by default, enable levelwise

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

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
2026-02-04 09:52:02 -08:00
..
fuzzing fix test build 2023-12-22 16:19:28 +00:00
lp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
algebraic.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
algebraic_numbers.cpp Add comprehensive test coverage for math/lp and math/polynomial modules (#7877) 2025-09-14 14:57:21 -07:00
api.cpp Implement Z3_optimize_translate for context translation (#8072) 2025-12-13 05:12:08 +00:00
api_algebraic.cpp Add comprehensive tests for API algebraic number functions (#7888) 2025-09-16 15:32:23 -07:00
api_ast_map.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
api_bug.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
api_datalog.cpp fix bug in unit test 2025-09-20 00:44:49 -07:00
api_pb.cpp Daily Test Coverage Improver: Add comprehensive API pseudo-boolean constraint tests (#7898) 2025-09-17 20:45:43 -07:00
api_polynomial.cpp preserve the initial state of the solver with push/pop for multiple objectives (#8264) 2026-01-23 10:41:03 -08:00
api_special_relations.cpp Daily Test Coverage Improver: Add comprehensive API special relations tests (#7925) 2025-09-18 09:20:14 -07:00
arith_rewriter.cpp fix build of tests 2022-06-17 17:11:18 +01:00
arith_simplifier_plugin.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
ast.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
bdd.cpp Additional BDD operations; BDD vectors and finite domain abstraction 2022-08-01 18:37:11 +03:00
bit_blaster.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
bit_vector.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
bits.cpp [WIP] Update code base to use std::span (#8269) 2026-01-21 12:42:19 -08:00
buffer.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
chashtable.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
check_assumptions.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
CMakeLists.txt remove optional_benchmarks from CmakeLists 2026-01-11 19:52:07 -08:00
cnf_backbones.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
cube_clause.cpp fix build of tests 2022-06-17 17:11:18 +01:00
datalog_parser.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
ddnf.cpp disable tracing in test code 2025-06-08 08:08:10 -07:00
diff_logic.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
distribution.cpp add tests for distribution utility and fix loose ends 2023-04-13 11:19:06 -07:00
dl_context.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
dl_product_relation.cpp fix #6213 2022-07-31 18:40:59 +03:00
dl_query.cpp Adopt std::optional for try_get_value and try_get_size functions (#8268) 2026-01-21 12:41:50 -08:00
dl_relation.cpp unused variables 2022-10-20 09:09:06 -07:00
dl_table.cpp fix build of tests 2022-06-17 17:11:18 +01:00
dl_util.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
dlist.cpp Sls (#7439) 2024-11-02 12:32:48 -07:00
doc.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-01-22 13:21:22 -08:00
egraph.cpp disable tracing in test code 2025-06-08 08:08:10 -07:00
escaped.cpp fix build of tests 2022-06-17 17:11:18 +01:00
euf_arith_plugin.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
euf_bv_plugin.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
ex.cpp add noexcept for signature compatibility 2024-11-04 11:13:49 -08:00
expr_rand.cpp fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
expr_substitution.cpp Add std::initializer_list overloads for BV and arith operations (#8467) 2026-02-02 10:00:13 -08:00
ext_numeral.cpp fixes 2017-08-27 11:01:45 -07:00
f2n.cpp fix build of tests 2022-06-17 17:11:18 +01:00
factor_rewriter.cpp fix build of tests 2022-06-17 17:11:18 +01:00
finder.cpp consolidate literals 2021-05-20 12:58:27 -07:00
fixed_bit_vector.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
for_each_file.cpp remove dependency on ARRAYSIZE for issue #1616 2018-08-15 22:26:14 -07:00
for_each_file.h booyah 2020-07-04 15:56:30 -07:00
get_consequences.cpp fix build of tests 2022-06-17 17:11:18 +01:00
get_implied_equalities.cpp tune for unit test, delay initialize re-solver 2018-05-13 11:49:33 -07:00
hashtable.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
heap.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
heap_trie.cpp fix build of tests 2022-06-17 17:11:18 +01:00
hilbert_basis.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-01-22 13:21:22 -08:00
ho_matcher.cpp Refactor mk_and and mk_app to use std::span API (#8285) 2026-01-22 16:58:38 -08:00
horn_subsume_model_converter.cpp fixing build 2022-11-03 22:08:21 -07:00
horner.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
hwf.cpp fix #7143: type punning in test 2024-03-04 14:34:02 +00:00
im_float_config.h booyah 2020-07-04 15:56:30 -07:00
inf_rational.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
interval.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
karr.cpp fix build of tests 2022-06-17 17:11:18 +01:00
list.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
main.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
map.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
matcher.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
memory.cpp Enable more tests on non-Windows. (#6199) 2022-07-29 11:48:27 +02:00
model2expr.cpp fix build of tests 2022-06-17 17:11:18 +01:00
model_based_opt.cpp fix unit test 2025-02-17 20:36:38 -08:00
model_evaluator.cpp fix build of tests 2022-06-17 17:11:18 +01:00
model_retrieval.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
monomial_bounds.cpp Add comprehensive test coverage for math/lp and math/polynomial modules (#7877) 2025-09-14 14:57:21 -07:00
mpbq.cpp fix build of tests 2022-06-17 17:11:18 +01:00
mpf.cpp disable tracing in test code 2025-06-08 08:08:10 -07:00
mpff.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
mpfx.cpp fix build of tests 2022-06-17 17:11:18 +01:00
mpq.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
mpz.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
nla_intervals.cpp Add comprehensive test coverage for math/lp and math/polynomial modules (#7877) 2025-09-14 14:57:21 -07:00
nlarith_util.cpp fix build of tests 2022-06-17 17:11:18 +01:00
nlsat.cpp Merge with branch lws (#8498) 2026-02-04 09:52:02 -08:00
no_overflow.cpp Modernize C++ patterns: range-based for loops and nullptr (#8167) 2026-01-11 21:20:07 -08:00
object_allocator.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
old_interval.cpp fix build of tests 2022-06-17 17:11:18 +01:00
optional.cpp Adopt std::optional for try_get_value and try_get_size functions (#8268) 2026-01-21 12:41:50 -08:00
parametric_datatype.cpp trim parametric datatype test 2025-10-15 21:39:39 +02:00
parray.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
pb2bv.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
pdd.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
pdd_solver.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-01-22 13:21:22 -08:00
permutation.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
polynomial.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
polynomial_factorization.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
polynorm.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
prime_generator.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
proof_checker.cpp fix build of tests 2022-06-17 17:11:18 +01:00
qe_arith.cpp Refactor mk_and and mk_app to use std::span API (#8285) 2026-01-22 16:58:38 -08:00
quant_elim.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
quant_solve.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-01-22 13:21:22 -08:00
random.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
rational.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
rcf.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
region.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
sat_local_search.cpp Modernize C++ patterns: range-based for loops and nullptr (#8167) 2026-01-11 21:20:07 -08:00
sat_lookahead.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
sat_user_scope.cpp fix build of tests 2022-06-17 17:11:18 +01:00
scoped_timer.cpp fix build of tests 2022-06-17 17:11:18 +01:00
scoped_vector.cpp add scoped_vector invariants and unit tests (#7327) 2024-08-02 19:21:40 -07:00
simple_parser.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
simplex.cpp Spacer Global Guidance (#6026) 2022-08-30 15:47:00 -07:00
simplifier.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
sls_seq_plugin.cpp add unit test for incremental equation edit distance with repair 2024-12-15 05:53:28 -08:00
sls_test.cpp Expose timestamp method in sls_context (#8347) 2026-01-26 11:27:27 -08:00
small_object_allocator.cpp Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
smt2print_parse.cpp just use std::string 2023-10-30 17:56:44 -07:00
smt_context.cpp call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
solver_pool.cpp fix build of tests 2022-06-17 17:11:18 +01:00
sorting_network.cpp Refactor mk_and and mk_app to use std::span API (#8285) 2026-01-22 16:58:38 -08:00
stack.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
string_buffer.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
substitution.cpp move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
symbol.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
symbol_table.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
tbv.cpp Move tbv to util 2022-08-01 18:37:11 +03:00
test_util.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
theory_dl.cpp fix build of tests 2022-06-17 17:11:18 +01:00
theory_pb.cpp disable tracing in test code 2025-06-08 08:08:10 -07:00
timeout.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
total_order.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
totalizer.cpp add totalizer version of rc2 2022-06-29 23:10:42 -07:00
trigo.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
udoc_relation.cpp Refactor mk_and/mk_or call sites to use vector overloads (#8286) 2026-01-22 13:21:22 -08:00
uint_set.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
upolynomial.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
value_generator.cpp fix build of tests 2022-06-17 17:11:18 +01:00
value_sweep.cpp fix build of tests 2022-06-17 17:11:18 +01:00
var_subst.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
vector.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00
zstring.cpp Standardize for-loop increments to prefix form (++i) (#8199) 2026-01-14 19:55:31 -08:00