3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 01:46:39 +00:00
Commit graph

394 commits

Author SHA1 Message Date
Nikolaj Bjorner
acad9fa62c
Update smt_context.cpp 2023-09-23 16:25:46 -07:00
Nikolaj Bjorner
940775d12d indentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-09-22 16:48:40 -07:00
Nuno Lopes
3b546b2348 smt_context: we can't assert that the resource limits were exceeded on cancel_exception
It happens sometimes that e.g. the internalizer goes above the soft memory limit
But since it's only by a small amount, when the exception propagates back to the context, some stuff
has been freed already and we are not longer above the memory threshold
Just delete these asserts
2023-08-20 10:34:28 +01:00
Nikolaj Bjorner
4637339091 update model validate to include arithmetic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-03 15:51:29 -07:00
Nikolaj Bjorner
adad468cd7 allow copy within a user scope #6827
this will allow copying the solver state within a scope.
The new solver state has its state at level 0. It is not possible to pop scopes from the new solver (you can still pop scopes from the original solver). The reason for this semantics is the relative difficulty of implementing (getting it right) of a state copy that preserves scopes.
2023-07-31 19:46:08 -07:00
Nikolaj Bjorner
4a9c4ca2ce initialize poly solver in incremental mode
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-07-13 14:12:29 -07:00
Nikolaj Bjorner
df77541aae #6758
check-assumptions with compound formulas create fresh proxy variables both during compilation to internal format and for the assumptions. These fresh variables may occur in lemmas that are created during search. The lemmas are garbage for future check-sats, but the solver needs to be allowed to invoke GC. Adding a GC call before a check-sat with assumptions allows removing some lemmas every time a new assumptions are used. Eager GC when using assumptions is used elsewhere, for example in cube&conquer scenarios where lemmas learned from one set of assumptions are less likely to be useful for other assumptions.

With the GC invocation memory grows at a lesser pace. However, it is not entirely free of memory increases. To avoid memory bloat, have the solver pre-compile the assumptions by defining them as propositional variables, add assertions that the propositional variables are equivalent to the compound formulas and use the propositional variables as assumptions. The same propositional variables come with no extra overhead when invoking check-assumptions. The lemmas are then over the same fixed vocabulary. It is generally a good idea to recycle useful lemmas during the enumeration pass.
2023-06-18 16:21:41 -07:00
Clemens Eisenhofer
82667bd86b
Fix UP's decide callback (#6707)
* Query Boolean Assignment in the UP

* UP's decide ref arguments => next_split

* Fixed wrapper

* More fixes
2023-06-02 09:52:54 +02:00
Nikolaj Bjorner
5e1869d8eb fix #6734
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-26 09:48:58 +01:00
Nikolaj Bjorner
7368f9f7d3 increase build version, better propagation in euf-egraph, handle assumptions in sat.smt
- increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86
- move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing)
- fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen.
2023-01-17 14:07:07 -08:00
Nuno Lopes
47324af210 be nicer when memout is reached in SMT internalize: return undef rather than crashing 2022-12-29 11:08:57 +00:00
Nikolaj Bjorner
fe8034731d fix #6501 2022-12-19 21:02:55 -08:00
Nikolaj Bjorner
0a28bacd0f remove debug out 2022-11-23 16:42:36 +07:00
Nikolaj Bjorner
6188c536ef add logging of propagations to smt core
log theory propagations with annotation "smt".
It allows tracking theory propagations (when used in conflicts) in the clause logs similar to the new core.
2022-11-23 11:37:23 +07:00
Nikolaj Bjorner
93e1db0b0b fix #6398 2022-10-13 11:16:14 +02:00
Nuno Lopes
16ef89905d fix infinite loop in internalize 2022-09-14 11:50:53 +01:00
Nikolaj Bjorner
34969b71ee #6340 again - reduce new assertions in fresh iteration
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-13 19:58:32 -07:00
Nikolaj Bjorner
fd5448d26b fix #6340 - again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-13 17:01:51 -07:00
Nikolaj Bjorner
63f48f8fd4 add options for logging learned lemmas and theory axioms
- add solver.axioms2files
  - prints negated theory axioms to files. Each file should be unsat
- add solver.lemmas2console
  - prints lemmas to the console.
- remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
2022-08-08 11:18:56 +03:00
Nikolaj Bjorner
5c2c0ae900 force-push on new_eq, new_diseq in user propagator, other fixes to Python bindings for user propagator
This update allows the python bindings for user-propagator to handle functions that are declared to be registered with the user propagator plugin. It fixes a bug in UserPropagateBase.add to allow registering terms dynamically during search.
It also fixes a bug in theory_user_propagate as scopes were not fully pushed when the solver gets the callbacks for new equalities and new disequalities.
It also adds equality and disequality interfaces to the sat/smt solver version (which isn't being exercised in earnest yet)
2022-07-25 03:42:29 +02:00
Clemens Eisenhofer
2fa60aa43c
Added function to select the next variable to split on (User-Propagator) (#6096)
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int
2022-06-19 10:49:25 -07:00
Nuno Lopes
73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places
It's harmful to have iostream everywhere as it injects functions in the compiled files
2022-06-17 14:10:19 +01:00
Nikolaj Bjorner
8efa3c8ade introduce notion of beta redex to deal with lambdas in non-extensional positions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-10 17:35:01 -07:00
Nikolaj Bjorner
5db133f875 add a way to supress lambdas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-06-10 14:35:20 -07:00
Nikolaj Bjorner
ca2497eecb na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-15 12:00:41 -07:00
Clemens Eisenhofer
e11496bc65
Added decide-callback to user-propagator (#5978)
* Fixed registering expressions in push/pop

* Reused existing function

* Reverted reusing can_propagate

* Added decide-callback to user-propagator

* Refactoring

* Fixed index
2022-04-15 20:07:17 +02:00
Nikolaj Bjorner
3cc9d7f443 improve pre-processing 2022-04-15 12:55:26 +02:00
Clemens Eisenhofer
7bb969ab52
Fixed problem with registering bitvector functions (#5923) 2022-03-26 16:36:15 -10:00
Nikolaj Bjorner
d790523c59 #5917
Add model.user_functions (default true) to control whether user functions are added to the model.
2022-03-23 09:49:44 -07:00
Clemens Eisenhofer
412b05076c
User-functions fix (#5868) 2022-02-26 09:21:01 -08:00
Nikolaj Bjorner
7b4f1ed530 missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-02-23 04:49:42 -08:00
Nikolaj Bjorner
3f3d058567 extract also units from search state 2022-02-07 06:16:22 +02:00
Nikolaj Bjorner
a326ad4cd9 flag incomplete on lambdas #5803 2022-01-31 11:54:06 -08:00
Nikolaj Bjorner
c00591daaf finish is-fixed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-19 16:28:34 +01:00
Nikolaj Bjorner
0f03ef4ab0 for Clemens: ensure fixed values are propagated after registration
Also allow to register expressions that the rewriter changes to ensure they get picked up.
2022-01-19 14:38:11 +01:00
Nikolaj Bjorner
5857236f2f introducing base namespace for user propagator 2021-11-29 19:41:30 -08:00
Nikolaj Bjorner
96e117d78c Update smt_context.cpp 2021-10-12 17:10:12 -07:00
Nikolaj Bjorner
c15968aa9e fix #4901 2021-10-12 17:10:04 -07:00
Nikolaj Bjorner
9790a8aa43 #5507
can't use auto-config if there are no assertions. Auto-config only works properly for one-shot mode since theories aren't loaded on demand in this solver.
2021-08-27 09:42:40 -07:00
Nikolaj Bjorner
e75b5e9513 don't copy "true" 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner
749d1ab305 remove dependencies on stale component 2021-08-16 17:52:36 -07:00
Nikolaj Bjorner
b1606487f0 fix #5289 2021-05-30 10:32:30 -07:00
Nikolaj Bjorner
8ba0fb5b58 rounding mode sort removed for incompatibility
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-05-21 16:18:43 -07:00
Nikolaj Bjorner
03d2c5f3d0 consolidate literals 2021-05-20 12:58:27 -07:00
Nikolaj Bjorner
4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner
15a7621e27 remove template dependency for trail objects 2021-03-19 11:15:05 -07:00
Nikolaj Bjorner
ea181fe8b2 more useful trace 2021-03-05 15:01:40 -08:00
Nikolaj Bjorner
026065ff71 streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
Nikolaj Bjorner
830f314a3f fixes to dt_solver and related 2021-02-27 11:03:20 -08:00
Nikolaj Bjorner
a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00