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

2.2 MiB

Raw History