* 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>
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
* Added 64-bit "1" counting
