mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 23:14:40 +00:00
Code Activity
20402 commits 50 branches 58 tags 179 MiB
Commit graph

49 commits

Author SHA1 Message Date
Nikolaj Bjorner
62b3668beb remove set cardinality operators from array theory. Make final-check use priority levels 
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
 2025-11-26 15:35:19 -08:00
Nikolaj Bjorner
e91e432496 add option to propagation quotients 
for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.
 2025-08-31 14:41:23 -07:00
Lev Nachmanson
5caa7f1a29 throttle lemmas in nla_solver untested 2025-06-26 16:33:16 -07:00
Lev Nachmanson
20fb830682 filter out empty lemmas from nla_solver on consumption 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-06-26 16:33:16 -07: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
41a3196c89 fix #7024 2023-11-29 13:35:30 -08:00
Nikolaj Bjorner
49a071988c remove temporary algebraic numbers from upper layers, move to owner module 2023-11-01 03:52:20 -07:00
Nikolaj Bjorner
bd8e5eee4b add simplification experiment (disabled) for tracking, some reshuffling of equation/fixed_equation structs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-29 10:21:31 -07:00
Nikolaj Bjorner
50654f1f46 add theory propagation to linear monomial propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-30 08:52:09 +09:00
Nikolaj Bjorner
7207f0ff9c sketch of internal propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-27 20:40:55 -07:00
Nikolaj Bjorner
ec2937e2de port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-26 20:08:30 -07:00
Nikolaj Bjorner
38b131386d add stubs for monomial unit propagation 2023-08-30 17:21:48 -07:00
Lev Nachmanson
610313946d split free vars in nla 2023-08-18 12:36:14 -07:00
Lev Nachmanson
252a30e727
use param_ref in nla_solver (#6862) 
* use param_ref in nla_solver

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

* add parameters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add parameters

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* replace nla_setting by command line parameters

* delete nla_setting.h

---------

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 18:44:27 -07:00
Lev Nachmanson
e091a2e775 remove the line with clang-format off 2023-07-10 12:05:59 -07:00
Lev Nachmanson
5ed2a82893
set clang format off for lp files (#6795) 
* adding // clang-format off

* set clang-format off at the beginning of  lp files

* set clang-format off

* remove dead code
 2023-07-03 17:35:16 -07:00
Nikolaj Bjorner
304b316314 move bounded division lemmas to nla solver/ nla_divisions. 2023-01-30 11:11:04 -08:00
Nikolaj Bjorner
8e37e2f913 handle non-linear division axioms, consolidate backtracking state in nla_core 
this update enables new incremental linear axioms based on division terms.
It also consolidates some of the backtracking state in nla_core / emons to use stack traces instead of custom backtracking state.
 2023-01-29 17:22:57 -08:00
Nikolaj Bjorner
8ea49eed8e convert reduce-args to a simplifier 
- convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed.
- bug fixes in model_reconstruction trail
  - allow multiple defs to be added with same pool of removed formulas
  - fix tracking of function symbols instead of expressions to filter replay
- add nla_divisions to track (cheap) divisibility lemmas.
-
 2023-01-28 20:12:14 -08:00
Nikolaj Bjorner
e41dd91893 add module for handling axioms for powers 2023-01-25 13:34:13 -08:00
Nikolaj Bjorner
2ae476416c initial outline of exponentiation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-23 17:38:34 -08:00
Lev Nachmanson
01279582ff move nla stats to nla_core 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 12:58:34 -07:00
Lev Nachmanson
6b28973799
nla review (#4321) 
* simplify the nla_solver interface

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

* more simplifications

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

* init m_use_nra_model

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

* work on NSB comments

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

* work on NSB comments

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

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 13:52:42 -07:00
Lev Nachmanson
b2dc21b107
simplify the nla_solver interface (#4312) 
* simplify the nla_solver interface

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

* more simplifications

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

* init m_use_nra_model

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

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 19:34:03 -07:00
Nikolaj Bjorner
be1a1dd7c2 add stubs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 17:36:46 -07:00
Nikolaj Bjorner
32055a31db pass resource limits by reference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 10:49:16 -07:00
Nikolaj Bjorner
bea0d45e6a disable new nlsat connection from master until debugged 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 09:38:17 -07:00
Lev Nachmanson
a14c2a3051 enable nlsat solver call from nla 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Lev Nachmanson
6b433b54e2 disable the call to nlsat from nla_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Lev Nachmanson
3e4a4c6df2 rebase with master branch 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Lev Nachmanson
279d55a2c7 nra to nla 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Lev Nachmanson
e32a6714a5 call nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Lev Nachmanson
7a79397769 nra to nla 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Nikolaj Bjorner
30de76b529 add occurs check to other nla_basic lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-09 20:50:27 -07:00
Nikolaj Bjorner
79fefe5fb3 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson
06173aa4d7 do not use nl variables in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-02-04 11:51:37 -08:00
Lev Nachmanson
a0bdb8135d rename monomial to monic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
130995a3db print terms as monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
8955509023 disable interval lemmas 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f24bd352e1 throttle intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
999ca2ed70 no intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
3f6ecfb3b6 generate lemmas from nla_intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9a71ed87d9 rebase with z3prover and fix term indices in monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f0cebd69fc get bounds from interval multiplication 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
f22252112e remove lar_solver from nla_intervals fields 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9ce2733105 unresolved in nla_intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
a4ad71bf33 hook up nla_intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
9c18ede687 hook up nla_solver it lp bound propagation 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson
33cbd29ed0 mv util/lp to math/lp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Renamed from src/util/lp/nla_solver.cpp (Browse further)