mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 22:35:35 +00:00
Code Activity
15908 commits 23 branches 48 tags 157 MiB
Commit graph

13456 commits

Author SHA1 Message Date
Nikolaj Bjorner 68b072e7f1 only use setup_and_check if there is no user propagator set. 2021-12-04 09:22:25 -08:00
Nikolaj Bjorner 1618c970df adding checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 13:17:48 -08:00
Nikolaj Bjorner 970347e797 infeas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 13:00:52 -08:00
Nikolaj Bjorner 0077ddf33c try delay init for user propagator in smt_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-03 09:45:07 -08:00
Nikolaj Bjorner 41aa7d7b60 stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-02 09:00:51 -08:00
Nikolaj Bjorner bfd61fec00 enable user propagation on tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-02 08:28:52 -08:00
Nikolaj Bjorner 71cbb160d2 fix regression from today, see #5676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 14:29:53 -08:00
Nikolaj Bjorner 87aec8819f fix #5687 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 10:08:29 -08:00
Nikolaj Bjorner c6a5aa0cc4 try th_lemma, update documentation of api functions for creating strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 09:21:02 -08:00
Nikolaj Bjorner 3b4f976118 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 19:15:03 -08:00
Nikolaj Bjorner 4daba290b1 change user propagation to apply scheme similar to theory_recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 19:12:15 -08:00
Nikolaj Bjorner 3c1aedf219 fixing #5473 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-30 17:08:28 -08:00
Nikolaj Bjorner 9e51691285 add virtual destructor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-29 20:02:12 -08:00
Nikolaj Bjorner b5efb87118 base -> core 2021-11-29 19:55:10 -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 c083aa82ee add debug information in user-propagate #5687 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-29 08:59:53 -08:00
Nikolaj Bjorner 1e9e52a58f #5641 2021-11-29 08:59:53 -08:00
Lev Nachmanson d50c4bfcc1 remove an unused var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2021-11-28 09:44:50 -08:00
Nikolaj Bjorner d50bfc6a50 #5641 2021-11-25 18:01:35 +01:00
Nikolaj Bjorner 833dd62623 fix #5681 2021-11-24 13:24:31 +01:00
Nikolaj Bjorner e8f5a29c31 fix #5679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-22 19:37:10 +01:00
Nikolaj Bjorner fee4821106 include thread 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 21:06:07 +01:00
Nikolaj Bjorner a7d24788c3 wasm build issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 20:45:36 +01:00
Nikolaj Bjorner 741c5f43f4 Merge branch 'master' of https://github.com/z3prover/z3 2021-11-19 11:03:08 -08:00
Nikolaj Bjorner ca2c2bb802 ensure smt2log works with multi-threaded consumers, ease scenarios around #5655 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 11:02:50 -08:00
Nikolaj Bjorner 4928c28e63 fix #5675 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 08:42:32 -08:00
Nikolaj Bjorner 99d5215956 revert use of f format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-19 00:01:19 -08:00
Nikolaj Bjorner f83367a11e mac builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 22:39:30 -08:00
Nikolaj Bjorner 518ef9f916 fix #5674 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-18 21:14:50 -08:00
Nikolaj Bjorner c826b64e35 prepare release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-16 09:41:51 -08:00
Nikolaj Bjorner b6f7deacf4 fix #5663 2021-11-12 11:36:42 -08:00
Nikolaj Bjorner 3c16edc8d3 check for v1 == v2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-12 09:11:17 -08:00
Nikolaj Bjorner 63ac2ee0d1 #5614 turn on / off options to get better performance. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-11 17:54:46 -08:00
Nikolaj Bjorner b28a8013fe #5653 
fix performance bottleneck in static features
 2021-11-11 13:30:38 -08:00
Nikolaj Bjorner 3a9656bc59 fixing issues with user propagator from python 
"fresh" remains broken (not working yet).
 2021-11-07 17:04:11 -08:00
Nikolaj Bjorner f2fcbc7cb7 capture values not reference 2021-11-07 13:43:56 -08:00
Nikolaj Bjorner af2cc460a9 #5646 2021-11-03 08:53:48 -07:00
Nikolaj Bjorner dd1e0fc561 #5643 2021-11-03 08:53:48 -07:00
Clemens Eisenhofer 091079e58c
Added user propagator example (#5625) 
* Added user propagator example

* User propagator example code refactoring
(+ removed unused parameter warning)

* Moved user-propagator example to its own directory
 2021-11-02 15:03:02 -07:00
Nikolaj Bjorner 87d4ce2659 working on #5614 
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
   - it resets row checks after backtracking even though they could still propagate
   - it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.

FYI @levnach
 2021-11-02 14:55:39 -07:00
Nikolaj Bjorner a94e2e62af build warnings 2021-11-02 14:55:38 -07:00
Henrich Lauko 96671cfc73
Add and fix a few general compiler warnings. (#5628) 
* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings
 2021-10-29 15:42:32 +02:00
Alexander Traud 1d45a33163
fix one typo and two misunderstandings for doxygen (#5633) 2021-10-29 15:35:05 +02:00
Alexander Traud d1592c6abf
fix misspelled \brief for doxygen (#5632) 2021-10-29 15:34:28 +02:00
Nikolaj Bjorner 4dad414161 fix performance regression after adding user declared functions to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-28 05:49:15 +02:00
Alexander Traud f5f35f87d0
fix grouping for latest doxygen (#5626) 
Since doxygen 1.8.16, opening and closing a group must not be done as
C comment but as doxygen command. In other words, not one but two
asterisk characters are required so that doxygen finds a group.
 2021-10-27 23:46:31 +02:00
Nikolaj Bjorner 125eae06bd #4869 load datatype parsing for HORN logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-26 11:54:29 +02:00
Nikolaj Bjorner 61eb8d1908 add ref for regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-26 11:39:13 +02:00
Nikolaj Bjorner aa5b4b8c77 strengthen contract for log_axiom_instantiation #5621 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-26 09:49:44 +02:00