3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Commit graph

17208 commits

Author SHA1 Message Date
Nikolaj Bjorner de9368bab0 Update expr_replacer.h 2022-11-04 11:25:39 -07:00
Nikolaj Bjorner 28668c6efc set up model reconstruction trail 2022-11-04 11:25:39 -07:00
Nikolaj Bjorner 84af521514 fixes #6439 #6436 2022-11-04 09:36:06 -07:00
Nikolaj Bjorner 626380b3c7 fixing build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-03 22:08:21 -07:00
Nikolaj Bjorner e8112a6564 add initial stubs for model reconstruction trail 2022-11-03 21:35:07 -07:00
Nikolaj Bjorner 9007bdf780 move horn_subsume_model_converter to ast/converters 2022-11-03 20:26:02 -07:00
Nikolaj Bjorner 25bb935793 move more converters 2022-11-03 20:18:21 -07:00
Nikolaj Bjorner 06eb460c75 move tactic_params to params 2022-11-03 05:50:46 -07:00
Nikolaj Bjorner 203652da74 add converters module to python build 2022-11-03 05:26:06 -07:00
Nikolaj Bjorner ba6b21d7d4 Create solve_eqs2_tactic.h 2022-11-03 05:23:38 -07:00
Nikolaj Bjorner 1dca6402fb move model and proof converters to self-contained module 2022-11-03 05:23:01 -07:00
Nikolaj Bjorner 7b12a5c5a8 build fix 2022-11-03 04:49:20 -07:00
Nikolaj Bjorner 90490cb22f make visited_helper independent of literals
re-introduce shorthands in sat::solver for visited and have them convert literals to unsigned.
2022-11-03 03:54:39 -07:00
Nikolaj Bjorner 070c5c624a wip - converting the equation solver as a simplifier 2022-11-03 03:35:30 -07:00
Nikolaj Bjorner 6841ba3e57 Update .gitignore 2022-11-03 03:35:30 -07:00
Nikolaj Bjorner c0f483528d working on solve_eqs 2022-11-03 03:35:29 -07:00
Nikolaj Bjorner e141759768 init solve_eqs 2022-11-03 03:35:29 -07:00
Clemens Eisenhofer 6790f18132
Added limit to "visit" to allow detecting multiple visits (#6435)
* 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 limit to "visit" to allow detecting multiple visits

* Putting visit in a separate class
(Reason: We will probably need two of them in the sat::solver)

* Bugfix
2022-11-03 03:34:52 -07:00
Nikolaj Bjorner e0bbe8dfc0 Merge branch 'master' of https://github.com/z3prover/z3 2022-11-02 17:32:32 -07:00
Nikolaj Bjorner df71e83428 remove incorrect assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-02 17:32:09 -07:00
Clemens Eisenhofer ae707ffff7
Added 64-bit "1" counting (#6434)
* 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
2022-11-02 10:02:29 -07:00
Nikolaj Bjorner 0d97d2214c adding virtual destructor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-11-02 09:37:55 -07:00
Nikolaj Bjorner 41b87b4c42 Create bv_slice_tactic.cpp
missing file
2022-11-02 08:51:43 -07:00
Nikolaj Bjorner e57674490f adding simplifiers layer
simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.

- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.

The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.
2022-11-02 08:51:30 -07:00
Nikolaj Bjorner 1646a41b2f minor fixes
- ensure mk_extract performs simplification to distribute over extract and removing extract if the range is the entire bit-vector
- ensure bool_rewriter simplifeis disjunctions when applicable.
2022-11-02 08:44:55 -07:00
Nikolaj Bjorner 9fc4015c46 remove ternary clause optimization
Removing ternary clause optimization from sat_solver simplifies special case handling of ternary clauses throughout the sat solver and dependent solvers (pb_solver). Benchmarking on QF_BV suggests the ternary clause optimization does not have any effect. While removing ternary clause optimization two bugs in unit propagation were also uncovered: it missed propagations when the only a single undef literal remained in the non-watched literals and it did not update blocked literals in cases where it could in the watch list. These performance bugs were for general clauses, ternary clause propagation did not miss propagations (and don't use blocked literals), but fixing these issues for general clauses appear to have made ternary clause optimization irrelevant based on what was measured.
2022-10-30 03:57:39 -07:00
Nikolaj Bjorner 0da0fa2b27 #6429 2022-10-29 13:43:07 -07:00
Nikolaj Bjorner 0e651eee04 #6421 2022-10-28 14:12:28 -07:00
Facundo Domínguez 91cdc082c4
Optimize calls to Z3_eval_smtlib2_string (#6422)
* Allow reseting the stream of smt2::scanner

* Put the parser of parse_smt2_commands in the cmd_context

* Move parser streams to cmd_context

* Move parser fields from cmd_context to api::context

* Move forward declarations from cmd_context.h to api_context.h

* Change parse_smt2_commands_with_parser to use *& instead of **

* Add tests for Z3_eval_smtlib2_string

* Don't reuse the streams in Z3_eval_smtlib2_string

* Fix indentation

* Add back unnecessary deleted line

Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
2022-10-28 13:57:22 -07:00
Nikolaj Bjorner a409a4a677 enforce flat within QF_BV tactic, cap in-processing var-elim loops 2022-10-27 20:10:55 -07:00
Nikolaj Bjorner 1fae3aa152 rename set-flat to set-flat-and-or to allow to differentiate parameters 2022-10-27 11:22:57 -07:00
Nikolaj Bjorner fe1b4bf5ce disable ternary, fixes to propagation, make bv_rewrites for multiplier n-ary 2022-10-26 23:44:38 -07:00
Nikolaj Bjorner 5352a0106d fix #6426 2022-10-26 12:20:55 -07:00
Nikolaj Bjorner 2258b9b9b6 #6423 2022-10-26 12:06:11 -07:00
Nuno Lopes 1720addc4e remove a bunch of string copies in the API
thanks to C++20
2022-10-26 18:22:55 +01:00
Nikolaj Bjorner a4ece21461 toggle enable-ternary to true 2022-10-25 10:44:23 -07:00
Nikolaj Bjorner 154fed7783 introduce globally visible macro for controlling use of ternary, turn them off 2022-10-25 10:30:18 -07:00
Nikolaj Bjorner c62c5e9d23 add opportunistic, missing, bv rewrites
- x >> x logical = 0
- ~x = -1 -x
- x * (y << z) = (x * y) << z
2022-10-25 10:29:48 -07:00
Nikolaj Bjorner 09a2ba4931 remove artificial usage of function, it causes another compiler warning to refer to a function without arguments. 2022-10-25 10:28:25 -07:00
Nikolaj Bjorner c672c3a250 fix regression introduced in #6143 2022-10-25 09:39:11 -07:00
Nikolaj Bjorner e1a00f4917 remove unused experimental feature - diff 2022-10-24 16:13:24 -07:00
Nikolaj Bjorner 280887cc5a remove deprecated theory aware drat functionality
it is handled by the on-clause callback that is owned by the smt solver.
2022-10-24 08:32:10 -07:00
Nuno Lopes cb3c86736c fix build 2022-10-24 10:23:50 +01:00
Nuno Lopes 4431fd17ce memory_manager: add support for MacOS & Windows to the new size tracking system 2022-10-24 10:09:56 +01:00
Nikolaj Bjorner a24b5a64e1 #6364 proviso for ignore int 2022-10-24 00:48:57 -07:00
Nikolaj Bjorner 5c7eaec566 #6364 - remove option of redundant clauses from internalization
gc-ing definitions leads to unsoundness when they are not replayed.
Instead of attempting to replay definitions theory internalization is irredundant by default.
This is also the old solver behavior where TH_LEMMA is essentially never used, but is valid for top-level theory lemmas.
2022-10-24 00:38:31 -07:00
Nikolaj Bjorner c8e1e180ea prefix Boolean variables in log with b 2022-10-23 11:05:50 -07:00
Nikolaj Bjorner 6393ed78d7 remove useless log 2022-10-23 11:05:33 -07:00
Nikolaj Bjorner ddbca68270 minor formatting update 2022-10-23 11:05:09 -07:00
Nikolaj Bjorner 4a1d76cf49 #6418 - add best-effort for nested and/or (from ite literals) 2022-10-23 11:03:51 -07:00