mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Code Activity
17236 commits 23 branches 48 tags 156 MiB
Commit graph

17236 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 4d86d73942 disable also tests for Windows x86, does not work with CI pipeline 2022-11-08 17:15:59 -08:00
Nikolaj Bjorner ff68df3451 update output of z3 doc 2022-11-08 16:10:50 -08:00
Nikolaj Bjorner 254f7b97ef cleanup state to clear model trail during calls. 2022-11-08 15:56:10 -08:00
Nikolaj Bjorner 823cd23ecc building x64 windows tests during ci is too slow, skipping tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-08 15:37:56 -08:00
Nikolaj Bjorner 3faca52c40 re-enable new solve_eqs with bug fixes 2022-11-08 14:17:17 -08:00
Nikolaj Bjorner 9ef78fcfa7 revert new solve-eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-08 13:57:58 -08:00
Nikolaj Bjorner 3a37cfca30 switch to solve_eqs2 tactic 2022-11-08 12:23:36 -08:00
Nikolaj Bjorner f769e2f1f6 have bool rewriter use flat_and_or, and integrate hoist rewriter 2022-11-08 12:21:50 -08:00
Nikolaj Bjorner 238ea0a264 add shorthands for concatentation 2022-11-08 12:21:25 -08:00
Nikolaj Bjorner 3a4b8e2334 add rewrite rules to bv-rewriter 2022-11-08 12:20:51 -08:00
Nikolaj Bjorner a34701471f clean up hoist rewriter 2022-11-08 12:20:25 -08:00
Nikolaj Bjorner ab36f86843 add handler for reporting statistics 2022-11-08 12:19:48 -08:00
Nikolaj Bjorner 8afec86fe8 add option for flat_and_or 2022-11-08 12:19:27 -08:00
Nikolaj Bjorner 10fb71cf93 better error description for configuring restart 2022-11-08 12:18:45 -08:00
Nikolaj Bjorner cbc5b1f4f6 have theory_recfun use recursive function discriminator to control when it is enabled 2022-11-06 12:09:45 -08:00
Nikolaj Bjorner f004478565 produce tseitin justification for clause proofs when a clause is a "gate". 2022-11-06 12:00:25 -08:00
Nikolaj Bjorner 53b6059276 bypass built-in proof objects for clause trail 
the build-in proof constructors are not flexible when it comes to allowing alternation of justified lemmas and lemmas without justifications.
 2022-11-06 11:59:56 -08:00
Nikolaj Bjorner 8ff1e44a95 add discriminator to whether context contains recursive functions to avoid enabling recursive function solver when there are just macros 2022-11-06 11:58:21 -08:00
Nikolaj Bjorner a4c2a2b22c use ast_util::mk_not to avoid redundant double negations during nff 2022-11-06 11:57:46 -08:00
Nikolaj Bjorner 78f9e6b31a extend error type message with more information - display the arguments that are passed 2022-11-06 11:57:21 -08:00
Nikolaj Bjorner 4c1a3fab64 fix #6442 2022-11-05 23:15:03 -07:00
Nikolaj Bjorner d8133a47c2 Update solve_eqs.cpp 2022-11-05 22:47:46 -07:00
Nikolaj Bjorner 6c12aaad74 wip - testing solve-eqs2, added as tactic 2022-11-05 22:42:59 -07:00
Nikolaj Bjorner 4d8860c0bc wip - adding context equation solver 
the solve_eqs_tactic is to be replaced by a re-implementation that uses solve_eqs in the simplifiers directory.
The re-implementation should address efficiency issues with the previous code.
At this point it punts on low level proofs. The plan is to use coarser
dependency tracking instead of low level proofs for pre-processing. Dependencies can be converted into a proof hint representation that can be checked using a stronger checker.
 2022-11-05 10:34:57 -07:00
Nikolaj Bjorner ae2672f132 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-04 14:11:24 -07:00
Nikolaj Bjorner 154b09309b fixing build, wip on model reconstruction integration into dependent-expr-state 2022-11-04 14:04:44 -07:00
Nikolaj Bjorner 7bb962d934 add ad-hoc any-of for cross compatibility and simplifying interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-04 12:49:55 -07:00
Nikolaj Bjorner 49d1490454 add ad-hoc any-of for cross compatibility and simplifying interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-11-04 12:48:30 -07:00
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