mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-10 13:53:23 +00:00
Code Activity
16601 commits 57 branches 53 tags 190 MiB
Commit graph

394 commits

Author SHA1 Message Date
Nikolaj Bjorner
bfb26ecc6d fix #3793 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 16:59:36 -07:00
Nikolaj Bjorner
dff5071598 compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 17:03:26 -07:00
Nikolaj Bjorner
550852bc62 fix #3765 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 13:49:26 -07:00
Nikolaj Bjorner
e246f6649e tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 13:31:48 -07:00
Nikolaj Bjorner
b889b110ee bool_vector, some spacer tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 12:59:04 -07:00
Nikolaj Bjorner
39ffc4ece7 fix #3759 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 11:19:23 -07:00
Nikolaj Bjorner
426e4cc75c fix #3557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 16:37:59 -07:00
Nikolaj Bjorner
896a1b2048 fix #3679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 15:04:56 -07:00
Arie Gurfinkel
dcc8a29a05 [spacer] fix ugly bug in ground refutation generation (i.e., cex) 2020-03-31 12:39:31 -04:00
Arie Gurfinkel
2ec00cb81d Replace is_null with is_non_empty_string in spacer params 2020-03-31 11:21:05 -04:00
Arie Gurfinkel
cfe96fe92e [spacer] fixedpoint.get_answer() returns ground refutation for SAT 2020-03-31 10:13:37 -04:00
Arie Gurfinkel
6180a5276d
Logging facility for spacer plus minor improvements (#3368) 
* [spacer] logging solver events

New option fp.spacer.trace_file='file.log' enables logging solving events
into a file.

These events are useful for debugging the solver, but also for visualizing
the solving process in a variety of ways

* [spacer] allow setting logic for solvers used by spacer

* [spacer] option to set arithmetic solver explicitly

* [spacer] improve of dumping solver_pool state for debugging

* fix propagate_ineqs to handle strict inequality

Co-authored-by: Nham Van Le <nv3le@precious3.eng.uwaterloo.ca>
 2020-03-16 20:31:44 -07:00
Nikolaj Bjorner
2d0d527fe1 preserve model order to avoid clobbering regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 16:56:49 -07:00
Nikolaj Bjorner
541658fe02 move to abstract symbols 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:14:13 -08:00
Nikolaj Bjorner
b76dee7a7a na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-06 18:47:06 +01:00
Nikolaj Bjorner
1e0c1cefd6 add definitions for under-specified cases of arithmetic operators #2663 #2676 #2679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-06 18:24:22 +01:00
Nikolaj Bjorner
67c4777514 fix #2548 fix #2530 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:03:04 +02:00
Arie Gurfinkel
1b83c677ea spacer: fixes lim_num_generalizer 
Must check that newly constructed generalization blocks
the proof obligation.

Was only checking that generalization is entailed by the transition system!
 2019-09-13 14:22:57 +02:00
Arie Gurfinkel
0d3fed9a6a spacer: lemma generalizer for small numbers 
Attempts to reduce denominators in coefficients of farkas lemmas
 2019-09-09 20:32:13 +02:00
Nikolaj Bjorner
000e485794 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-01 12:17:19 -07:00
Arie Gurfinkel
375c0ff9a9 Implement get_proof() in bmc and spacer engines 2019-08-12 10:29:01 -07:00
Nikolaj Bjorner
fc41a61b6e expose strategic solver factory prototype at level of solver module 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-09 15:52:12 -07:00
Arie Gurfinkel
92db639caf Use refutation to compute ground sat answer 2019-07-25 15:22:37 -04:00
Nuno Lopes
1827f98851 more fixes for mutexes in shell 2019-06-19 16:42:00 +01:00
Nikolaj Bjorner
e0d8cefde4 remove cooperate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:15:46 -07:00
Nikolaj Bjorner
8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner
f00697cf95 fix #2155 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 22:33:28 -08:00
Nikolaj Bjorner
26921d1c9c fix #2155 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 22:32:50 -08:00
Nikolaj Bjorner
7aa8b4ac2a restrict idiv-bound checks to bounded terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 19:11:22 -08:00
Nikolaj Bjorner
89bf2d4368 add API for setting variable activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-15 12:05:24 -08:00
Nikolaj Bjorner
a76107e50d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-01 18:44:52 -08:00
Nikolaj Bjorner
8d20310758 adding trail/levels 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-29 14:45:51 -08:00
Nikolaj Bjorner
498864c582 adding dump facility for cancelation #2095, easing dimacs in/out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 12:21:23 -08:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07:00
Nikolaj Bjorner
72400f1869 fix #1927 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-12 03:43:04 -08:00
Arie Gurfinkel
d4e476d764 Work around unexpected behaviour in generalizer 2018-11-11 09:06:36 -05:00
Arie Gurfinkel
6cc6ffcde2 Fix display_certificate in spacer 
This is expected to work now
(query q1 :print-certificate true)
 2018-11-11 09:06:22 -05:00
Arie Gurfinkel
58d93d8907 Fix add external lemmas to solver even if use_bg_invs=false 
spacer.use_bg_invs controls how user-supplied invariants are used.
However, the user expects them to be used independent of the option.
 2018-11-11 08:41:22 -05:00
Nikolaj Bjorner
d7ecaa2ebb add stub for certificate #1926 2018-11-10 09:56:44 -08:00
Florian Pigorsch
326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Michał Janiszewski
cfd0486582 Catch exceptions by const-reference 
Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
 2018-10-16 19:16:07 +02:00
Nikolaj Bjorner
6704a4be02
Revert "Made Z3 compile for C++17 with MSVC" 2018-10-15 12:52:19 -07:00
Matthew Parkinson
01005a46f6 Made it more legal C++17 2018-10-15 17:25:34 +01:00
Bruce Mitchener
373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Arie Gurfinkel
f67346d16e Fix is_infty_level to treat 2^16-1 as infinity 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
5d2f682f7a Enable proof mode in add_cover 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
0035d9b8cb Background external invariants 
Background external invariants are constraints that are assumed to be
true of the system. This commit introduces a mode in which
background invariants are used only duing inductive generalization
and lemma pushing, but not during predecessor computation.

It is believed that this will be more efficient used of background
external invariants since they will not be able to disturb how
predecessors are generalized and computed.

Based on a patch by Jorge Navas
 2018-09-04 21:49:59 -04:00
Arie Gurfinkel
533e9c5837 Expand equality literals when eq_prop is disabled 
When equality propagation is disabled for arithmetic,
equality atoms are expanded into inequality for potentially
better generalization with interpolation
 2018-09-04 21:49:59 -04:00
Nikolaj Bjorner
84c7df75d6 record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 16:21:27 -07:00