mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 21:33:39 +00:00
Code Activity
19367 commits 31 branches 50 tags 166 MiB
Commit graph

214 commits

Author SHA1 Message Date
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
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
07dd1065db added API to monitor clause inferences 
See RELEASE_NOTES for more information
examples pending.
 2022-10-19 08:34:55 -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
7a55bd5687 beta redex check is used in array theory to filter out safe as-arrays 2022-09-11 05:44:11 -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
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
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
51ed13f96a update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-08 06:28:24 -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
Clemens Eisenhofer
412b05076c
User-functions fix (#5868) 2022-02-26 09:21:01 -08:00
Nikolaj Bjorner
2e00f2f32d
Propagator (#5845) 
* user propagator without ids

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

* user propagator without ids

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

* fix signature

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

* references #5818

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

* fix c++ build

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

* switch to vs 2022

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

* switch 2022

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

* Update propagator example (I) (#5835)

* fix #5829

* na

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

* switch to vs 2022

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

* Adapted the example to the changes in the propagator

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* context goes out of scope in stack allocation, so can't used scoped context when passing objects around

* parameter check

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

* add rewriter

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

* Fixed bug in user-propagator "created" (#5843)

Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
 2022-02-17 09:21:41 +02: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
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
f0740bdf60 move user propagte declare to context level 
declaration of user propagate functions are declared at context level instead of at solver scope.
 2021-12-18 10:56:42 -08:00
Nikolaj Bjorner
4856581b68 na 2021-12-17 16:40:19 -08:00
Nikolaj Bjorner
9c8800bdde adding a new toy for Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 10:45:59 -08:00
Nikolaj Bjorner
6cc9aa3562 prepare user propagator declared functions for likely Clemens use case 2021-12-16 19:37:30 -08:00
Nikolaj Bjorner
959f4c9440 rename files to theory_user_propagator 2021-11-29 19:44:58 -08:00
Nikolaj Bjorner
5857236f2f introducing base namespace for user propagator 2021-11-29 19:41:30 -08:00
Nikolaj Bjorner
13da6a02a6 add handling of quantifiers #5612 2021-10-20 12:27:56 -04:00
Nikolaj Bjorner
c15968aa9e fix #4901 2021-10-12 17:10:04 -07:00
Nikolaj Bjorner
749d1ab305 remove dependencies on stale component 2021-08-16 17:52:36 -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
ab0735fde2 separate component for asserted_formulas to break dependency cycles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-03-17 15:51:38 -07:00
Nikolaj Bjorner
ddbcd08d46 move asserted_formulas to solver scope 2021-03-17 15:02:16 -07:00
Nikolaj Bjorner
026065ff71 streamline pb solver interface and naming after removal of xor 2021-02-28 12:32:04 -08:00
Nikolaj Bjorner
a152bb1e80 remove template Context dependency in every trail object 2021-02-08 15:41:57 -08:00
Nikolaj Bjorner
8f577d3943 remove ast_manager get_sort method entirely 2021-02-02 13:57:01 -08:00
Nikolaj Bjorner
e3d634807b move common routines for quantifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-28 13:23:40 -08:00
Nikolaj Bjorner
ac4bcb9034 update logging for lemmas 2020-10-29 15:09:23 -07:00
Nikolaj Bjorner
e962deb557 remove also second hash-table for ALIVE_OPT #4747 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-27 00:12:34 -07:00
Nikolaj Bjorner
367e5fdd52
delay internalize (#4714) 
* adding array solver

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

* use default in model construction

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

* debug delay internalization

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

* bv

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

* arrays

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

* get rid of implied values and bounds

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

* redo egraph

* remove out

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

* remove files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-28 19:24:16 -07:00
Nikolaj Bjorner
65e6d942ac euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 01:55:13 -07:00
Nikolaj Bjorner
96f10b8c1c user propagator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-22 19:01:04 -07:00
Nikolaj Bjorner
2d5b749745 extend solver callbacks with methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 19:24:59 -07:00
Nikolaj Bjorner
080be7a2af merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-21 12:14:28 -07:00
Nikolaj Bjorner
ecb43ccca2 update smt logging format to follow SAT solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-20 20:00:20 -07:00
Nikolaj Bjorner
4857d60c99 user propagator over the API 2020-08-18 21:53:02 -07:00
Nikolaj Bjorner
0c93c7aa08 adding user propagation to API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-18 10:30:10 -07:00
Nikolaj Bjorner
152c95f72a adding user-propagator ability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-17 22:39:55 -07:00
Nikolaj Bjorner
558233dd8e build fixes, add lazy push/pop state to avoid overhead on unused theories 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-17 00:13:46 -07:00
Nikolaj Bjorner
ca3ec22b7a handle better cancellation for parallel, switch between cube mode and base level mode in smt.threads, expose parameters to control theory_bv and phase caching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-16 23:29:24 -07:00
Nikolaj Bjorner
c63ad2e834 enable ranges for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 10:53:37 -07:00