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

2162 commits

Author SHA1 Message Date
Nikolaj Bjorner eb15f8249a fix backtrack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-19 21:01:25 -07:00
Nikolaj Bjorner 936312cfd2 fix location of research 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 18:15:35 -07:00
Nikolaj Bjorner 2d4a5e0a5e n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 18:07:04 -07:00
Nikolaj Bjorner c0556b2f64 iterative deepening per recursive function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 17:53:11 -07:00
Nikolaj Bjorner 35eb6eccd1 iterative deepening 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 17:14:10 -07:00
Nikolaj Bjorner d22a0d04ed n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 10:01:32 -07:00
Nikolaj Bjorner 2f5f546990 ctx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-18 09:02:20 -07:00
Nikolaj Bjorner bd53fa801e handle case input format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 21:42:18 -07:00
Nikolaj Bjorner 8a9837a8b5 more refinements for recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 10:02:56 -07:00
Nikolaj Bjorner 48cdd12a47 cleanup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 05:56:04 -07:00
Nikolaj Bjorner 9dd9d5e18a more integration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 05:22:43 -07:00
Nikolaj Bjorner c7d0d4e191 add c-cube's recursive function theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 04:56:58 -07:00
Nikolaj Bjorner e9d615e309 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 15:16:22 -07:00
Nikolaj Bjorner 44a0dbbc61 fix #1864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 08:06:51 -07:00
Nikolaj Bjorner a549e73b86 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 13:43:01 -07:00
Nikolaj Bjorner fd9fd52271 fixing #1847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-02 17:13:46 -07:00
Murphy Berzish b2f0051114 Merge remote-tracking branch 'upstream/master' into refactoring-arith 2018-10-02 12:38:40 -04:00
Murphy Berzish 39fbf1e174 Z3str3: don't use arith_value::get_value in get_arith_value 2018-10-02 12:28:53 -04:00
Kirill Bobyrev a376a8d343 [NFC] Cleanup arith_eq_solver.(cpp|h) 
Use for-range loops instead of for-index loops where possible, remove
trailing whitespaces.

This patch does not affect functionality.
 2018-10-02 16:14:01 +03:00
Nikolaj Bjorner 620c5d1d81
Merge pull request #1850 from Nils-Becker/master 
adding call to update_max_generation
 2018-10-01 21:49:14 -07:00
Nikolaj Bjorner 2cf6ada38e
Merge pull request #1856 from waywardmonkeys/minor-fixes 
Minor fixes
 2018-10-01 20:46:27 -07:00
Nikolaj Bjorner c84182b42a
Merge pull request #1859 from waywardmonkeys/for-range-copy 
Avoid unnecessary copies in for-range loops.
 2018-10-01 20:44:52 -07:00
Nikolaj Bjorner 7082d85115
Merge pull request #1860 from waywardmonkeys/modernize-use-override 
Use 'override' where possible.
 2018-10-01 20:43:56 -07:00
Bruce Mitchener 6d2936e5fc watch_list: Fix indentation. 2018-10-02 10:43:00 +07:00
Bruce Mitchener 1067a5363f theory_lra: Remove unused variable. 2018-10-02 10:42:54 +07:00
Bruce Mitchener 7bc283b84e Avoid unnecessary copies in for-range loops. 2018-10-02 10:38:41 +07:00
Bruce Mitchener 373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Nikolaj Bjorner 096a6c088d Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 19:32:52 -07:00
Nikolaj Bjorner bb979a194e remove unused return value of mk_enode following #1856 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 19:32:44 -07:00
Bruce Mitchener cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Murphy Berzish 03d9047490 Merge remote-tracking branch 'upstream/master' into refactoring-arith 2018-10-01 17:51:12 -04:00
Nikolaj Bjorner aaba1b9b15 fix sort retrieval for lambdas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 09:18:40 -07:00
nilsbecker c92c431570 adding call to update_max_generation 2018-10-01 16:32:04 +02:00
Nikolaj Bjorner af41255a9d fix regression in model generation for UFLRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-25 10:00:13 -07:00
Nikolaj Bjorner 38c6429184
Merge pull request #1838 from NikolajBjorner/master 
remove offsets from terms to fix cut generation
 2018-09-21 17:03:42 -07:00
Nuno Lopes 0b7918c52e remove spurious pragma 2018-09-21 09:37:36 +01:00
Nikolaj Bjorner d75b6fd9c1 remove offsets from terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-20 11:06:05 -07:00
Nikolaj Bjorner 3c553c17e8 fix dump utility for cuts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 14:32:56 -07:00
Nikolaj Bjorner ed19af4c4e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-19 09:02:37 -07:00
Lev ca3ce964ce work on Gomory cut 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-09-18 13:34:05 -07:00
Murphy Berzish 144b72244e clean up pragmas, Z3str3 refactoring 2018-09-18 16:11:47 -04:00
Murphy Berzish 7e419137b1 Z3str3: refactor regex automata to subroutine, use arith_value 2018-09-17 16:13:34 -04:00
Nikolaj Bjorner 1a3fe1edd3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-16 13:43:38 -07:00
Nikolaj Bjorner 286126dde9 fix #1828, add self-contained utility to extract arithmetical values for use in theory_seq and theory_str and other theories that access current values assigned to numeric variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-16 13:31:37 -07:00
Nikolaj Bjorner 78950fde17 initialize solver before parse is invoked. Fixes issue reported by Selsam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-13 19:05:45 -07:00
Nikolaj Bjorner 6ea4aff622 add validation code for cuts, fix missing unit propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-13 10:47:50 -07:00
Nikolaj Bjorner 4ffd860375 narrowing incorrect lemma generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-11 11:31:19 -07:00
Nikolaj Bjorner 3bf072557e disable branches when arguments are non-integral #1824 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-11 04:14:28 -07:00
Nikolaj Bjorner b1423e17a1 Merge branch 'master' of https://github.com/z3prover/z3 2018-09-11 03:14:41 -07:00
Nikolaj Bjorner 36a14a354a disable dotnet in ci script. It seems to get turned on even if dotnet bindings are not requested 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-11 03:14:31 -07:00