mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-14 08:26:39 +00:00
Code Activity
12122 commits 42 branches 51 tags 169 MiB
Commit graph

200 commits

Author SHA1 Message Date
Nikolaj Bjorner
4fabaf95aa remove deprecated and bind1st and unused warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-08 13:26:50 -08: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
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
Bruce Mitchener
e2122c0d3d Fix whitespace issues in *.pyg. 2019-08-15 10:19:33 -07:00
Nikolaj Bjorner
e0a44894cf purge smt.timeout, use timeout instead to control solver timing #2354 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 16:56:24 +02:00
Nikolaj Bjorner
11a8ced769 fix #2353 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 10:47:56 +02:00
Nikolaj Bjorner
89e8a1392c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 10:40:35 +02: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
7bfb730fee fix traffic jam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-10 17:45:55 -07:00
Nikolaj Bjorner
01f6489892 fix #2310 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 16:22:49 -07:00
Nikolaj Bjorner
5c67c9d907 print certificate for #2202, enable CTL-C for API fix #2203 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 17:09:02 -07:00
Bruce Mitchener
44bc00f13d Fix typos. 2018-12-23 21:58:57 -05:00
Bruce Mitchener
e570940662 Prefer using empty rather than size comparisons. 2018-11-27 21:42:04 +07: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
58682c20be dl_util: Use an unsigned to match other values. 2018-10-13 07:58:27 +07:00
Arie Gurfinkel
3a01fd791b Replace rule API 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
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
Nikolaj Bjorner
e041ebbe80 bmc improvements, move fd_solver to self-contained directory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-05 10:00:49 -07:00
Arie Gurfinkel
5d1149adb2 Transformation to eliminate term-ite expressions from DL rules 2018-07-02 17:09:56 -04:00
Arie Gurfinkel
6d75c31468 First draft of elim_term_ite xform. Not working. 2018-07-02 17:09:56 -04:00
Arie Gurfinkel
5e87d7c4a3 Formatting: move q3 parameters closer together 2018-06-28 15:38:51 -04:00
Arie Gurfinkel
c00c6b4285 Pobs are always managed 
Removed options to allow unmanaged pobs.
Other minor cleanups.
 2018-06-27 22:49:35 -04:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-26 07:23:04 -07:00
Arie Gurfinkel
9109968e55 Cleanup fixedpoint options 
Replace pdr options with spacer
Repace fixedpoint module with fp
 2018-06-14 16:08:52 -07:00
Arie Gurfinkel
d38879e478 Renamed spacer options 2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
6adaed718f remove pdr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
521392a8f1 First partially working pdr strategy in spacer 2018-06-14 16:08:51 -07:00
Arie Gurfinkel
ada548b5ae Removed unused options 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
e2e1411707 Option to dump SMT queries as benchmarks during Spacer run 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
fb52c36210 spacer: switch to new IUC as default 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
723e96175b spacer: prepare to use incremental clause smt_solver interface 2018-06-14 16:08:50 -07:00
Arie Gurfinkel
55126692c9 spacer: counterexample to pushing (ctp) 
Enable using fixedpoint.spacer.ctp=true

For each lemma L currently at level k, keep a model M that justifies
why L cannot be pushed to (k+1). L is not pushed while the model M
remains valid.
 2018-06-14 16:08:49 -07:00
Nikolaj Bjorner
ff0f257102 remove iff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel
5d3b515a50 Cleanup option names and default values 2018-06-14 16:08:48 -07:00
Bernhard Gleiss
85c58e344c Add option to use old_hyp_reducer 2018-06-14 16:08:48 -07:00
Matteo Marescotti
a4e67b8bb6 Wire JSON printing into Spacer 2018-06-14 16:08:48 -07:00
Matteo Marescotti
28ef9ab9d1 User option to enable starting spacer from a given level 2018-06-14 16:08:48 -07:00
Matteo
65885f7eba add_constraint API 2018-06-14 16:08:48 -07:00
Matteo
3c7165780c Extend spacer with callback events 
Callback events allow the client of spacer to
get events during exection. The events include
new lemmas and unfolding.
 2018-06-14 16:08:48 -07:00
Arie Gurfinkel
04a778f2fd Option to enable cube normalization in quic generalizer 2018-06-14 16:08:48 -07:00
Yakir Vizel
23a8e59493 Initial commit of QGen 
Controlled by fixedpoint.spacer.use_quanti_generalizer

measure cumulative time, number of invocations, and number of failed
SMT calls

Relaxing equality in a pattern: if a variable equals a numeral, relax with GE

pob::get_skolems() returns all skolems that might appear in the pob.
New skolems must be added above the largest index in that map,
even if they are not used in the pob itself.

pattern generalization should be done before the pattern is skolemized and
added into the new cube.
 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
25fad153d1 added option fixedpoint.spacer.iuc.debug_proof to debug proof which is used for generation of iuc 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
00a99f01b4 improved options for IUC computation 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
fba995294d refactored options regarding farkas lemma handling 2018-06-14 16:08:47 -07:00
Bernhard Gleiss
56fcb8e6fd added option fixedpoint.spacer.print_farkas_stats to print number of Farkas lemmas in each proof 2018-06-14 16:08:47 -07:00