3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Commit graph

270 commits

Author SHA1 Message Date
Lev Nachmanson
899677e626 fix a warning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-06-26 16:33:16 -07:00
Lev Nachmanson
832cfb3c41 consolidate throttling 2025-06-26 16:33:16 -07:00
Lev Nachmanson
5caa7f1a29 throttle lemmas in nla_solver untested 2025-06-26 16:33:16 -07:00
Lev Nachmanson
4e33b44d27 add lemma.is_empty()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-06-26 16:33:16 -07:00
Lev Nachmanson
5bda42e104 rename new_lemma to lemma_builder
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-06-26 16:33:16 -07:00
Nikolaj Bjorner
7f5427b839 disable assertion that checks nl lemmas if using nra core 2025-05-30 14:47:31 +01:00
LeeYoungJoon
0a93ff515d
Centralize and document TRACE tags using X-macros (#7657)
* Introduce X-macro-based trace tag definition
- Created trace_tags.def to centralize TRACE tag definitions
- Each tag includes a symbolic name and description
- Set up enum class TraceTag for type-safe usage in TRACE macros

* Add script to generate Markdown documentation from trace_tags.def
- Python script parses trace_tags.def and outputs trace_tags.md

* Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled

* trace: improve trace tag handling system with hierarchical tagging

- Introduce hierarchical tag-class structure: enabling a tag class activates all child tags
- Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag
- Implement initial version of trace_tag.def using X(tag, tag_class, description)
  (class names and descriptions to be refined in a future update)

* trace: replace all string-based TRACE tags with enum TraceTag
- Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals

* trace : add cstring header

* trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py

* trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h.

* trace : Add TODO comment for future implementation of tag_class activation

* trace : Disable code related to tag_class until implementation is ready (#7663).
2025-05-28 14:31:25 +01:00
Nikolaj Bjorner
a39efbb008 fix #7607 2025-04-05 11:58:47 -07:00
Nikolaj Bjorner
551cc53a2f fix un-intialized variable warnings 2024-09-30 15:08:33 -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
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
2c55aa5466 remove unused code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-01-17 18:04:08 -08:00
Nikolaj Bjorner
4d1d067d42 fix divergence reported by Guido Martinez 2023-12-07 13:34:35 -08:00
Nikolaj Bjorner
25dd29907b refine no-effect predicate to include value of ret 2023-12-03 12:41:21 -08:00
Nikolaj Bjorner
4350bd77ac check cancel flag to avoid unsound conflicts 2023-11-19 11:43:52 -08:00
Lev Nachmanson
ca6cb0af95 add changes in lp with validate_bound and maximize_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-11-02 09:59:03 -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
5622fd1362 initialize delay bound
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-26 03:26:41 -07:00
Nikolaj Bjorner
20c54048f7 use cone of influence reduction before calling nlsat. 2023-10-25 16:19:23 -07:00
Nikolaj Bjorner
e2db2b864b add hook for in-processing simplification for NLA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 15:09:21 -07:00
Nikolaj Bjorner
55775bdc20 incremnet log level for debug output on cancelation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-10-25 13:15:15 -07:00
Nikolaj Bjorner
53ce18ef34 update backoff for bounded_nla 2023-10-21 19:57:06 -07:00
Nikolaj Bjorner
97058b0d5d allow for propagations the trigger make-feasible check 2023-10-19 16:08:44 -07:00
Nikolaj Bjorner
c9c5dbc347 #6523 2023-10-16 09:27:22 -07:00
Nikolaj Bjorner
4a870966ad add code to enable unit propagation of bounds
set UNIT_PROPAGATE_BOUNDS 1 to use the unit propagation version. It applies unit propagation eagerly (does not depend on checking LIA consistency before final check) and avoid creating new literals in most cases
2023-10-09 16:04:39 +09:00
Lev Nachmanson
edd1761ff3 restore the scheme of m_columns_with_changed_bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-10-04 11:06:24 -07:00
Lev Nachmanson
7de06c4350 merging master to unit_prop_on_monomials 2023-10-02 16:42:59 -07:00
Lev Nachmanson
a297a2b25c fixes in lar_solver around nl unit propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-10-01 11:39:58 -07:00
Lev Nachmanson
b64fdef41f better tracking changinc rows and monomials 2023-09-29 15:27:22 -07:00
Lev Nachmanson
f30a2c13be propagate only one non-fixed monomial intrernally
lar_solver
2023-09-28 17:24:34 -07:00
Lev Nachmanson
29b5c47a8d track changed monics efficiently
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-27 09:09:38 -07:00
Nikolaj Bjorner
e8fcc876c9
Merge branch 'master' into unit_prop_on_monomials 2023-09-26 20:14:06 -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
Lev Nachmanson
6ff4856e38 throttle monomial unit prop and and nl params 2023-09-25 16:47:34 -07:00
Nikolaj Bjorner
0a1ade6f95 move m_nla_lemma_vector to be internal to nla_core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-25 12:40:52 -07:00
Lev Nachmanson
26a9b776c6 clean m_nla_lemma_vector in nla_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-25 12:10:59 -07:00
Nikolaj Bjorner
886d3f4351 indentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 16:55:34 -07:00
Nikolaj Bjorner
eac54ba084 indentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 16:54:12 -07:00
Nikolaj Bjorner
940775d12d indentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 16:48:40 -07:00
Lev Nachmanson
caa929f01f do not use lemmase in monomial propagation 2023-09-22 14:27:26 -07:00
Lev Nachmanson
f423642e9b try the lemma scheme 2023-09-21 12:18:21 -07:00
Lev Nachmanson
e31cecf5db transfer propagate monomial bounds to nla_solver 2023-09-21 11:27:53 -07:00
Lev Nachmanson
c5cfd62e0a remove dead code related to nla unit propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-19 10:56:09 -07:00
Lev Nachmanson
c309d52283 runs a simple test 2023-09-13 08:12:00 -07:00
Lev Nachmanson
c050af922f fixing the bugs 2023-09-07 15:59:20 -07:00
Lev Nachmanson
47b64e689c restore the lemma scheme
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-07 11:33:14 -07:00
Lev Nachmanson
41f59cb1ed propagate monomial is nla 2023-09-05 18:49:59 -07:00
Lev Nachmanson
318d7d7564 fixes a bug 2023-09-01 11:32:26 -07:00