mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity
9654 commits 23 branches 48 tags 157 MiB
Commit graph

9654 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 8895ed7122 remove unintialized variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 18:34:02 -07:00
Nikolaj Bjorner b6054b8406 add has_value utility to retrieve value from solver state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 17:03:58 -07:00
Nikolaj Bjorner 13413d0529 update for int return value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 15:08:16 -07:00
Nikolaj Bjorner 593a6e5139 update smt_setup and default parameters to only use new solver consveratively 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 12:52:50 -07:00
Nikolaj Bjorner fad1e611aa build warnings, updates to reduce-invertible, change is_algebraic tester to use int return type 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 12:34:55 -07:00
Nikolaj Bjorner 5a2a8d7d5c
Merge pull request #1715 from levnach/master 
merge lar_solver/int_solver
 2018-07-01 12:20:02 -07:00
Nikolaj Bjorner b8b70c53fa update invertible tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-01 09:17:20 -07:00
Nikolaj Bjorner e027622886 updates to invertible tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 21:46:29 -07:00
Nikolaj Bjorner 76417fa3b6 fleshing out reduce-invertible tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 17:06:56 -07:00
Lev Nachmanson c554e1723b fixes in theory_lra by Nikolaj 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-30 13:53:45 -07:00
Nikolaj Bjorner ac014bef94 outline of invertible reduction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 13:46:29 -07:00
Nikolaj Bjorner cce3448fd5 workaround for heisenbug behavior with tester 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 11:56:01 -07:00
Nikolaj Bjorner c4d893dfad fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-30 06:10:09 -07:00
Nikolaj Bjorner 080bf79fe6
Merge pull request #1705 from trinhmt/master 
created pull from Trinh's seq solver
 2018-06-30 04:53:14 -07:00
Thai Trinh cd62017afd fixed failures with regression tests 2018-06-30 15:52:20 +08:00
Nikolaj Bjorner 3ad7d59f22 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 21:25:21 -07:00
Nikolaj Bjorner 797e576195 unreferenced variable in release mode, spaces 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 21:25:08 -07:00
Nikolaj Bjorner 33fc56f686 fix debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 18:36:43 -07:00
Nikolaj Bjorner f1d27cd487 workaround non-deterministic behavior of is_irrational_numeral test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 18:16:32 -07:00
Lev Nachmanson 16d4e2f5d1 regression fix 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 16:10:15 -07:00
Lev Nachmanson 4d88818560 fixes in get_lower,get_upper of theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 14:38:10 -07:00
Lev Nachmanson 342feeff03 implement get_lower, get_upper in theory_lra.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 14:17:13 -07:00
Lev Nachmanson da44ad7e6f added stubs for get_lower/get_upper required by theory_seq 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 13:43:23 -07:00
Lev Nachmanson f2e878047d avoid a crash in maximize_term when the term var has not been used 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 13:33:31 -07:00
Nikolaj Bjorner 481b177d47 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 10:39:25 -07:00
Nikolaj Bjorner c0694ae33a deal with memory leak during shutdown 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 10:39:07 -07:00
Nuno Lopes bc8cd7ff55 remove a few random mem allocs 2018-06-29 18:34:17 +01:00
Lev Nachmanson d80f6e3222 regression failures fixes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-29 09:57:29 -07:00
Nikolaj Bjorner cbc5aaad2c strengthen simplification of to_int such that #1608 is handled during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 09:44:54 -07:00
Nikolaj Bjorner 1e67717d75 log with unsigned characters to avoid malformed strings as in #1712 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 09:11:44 -07:00
Nikolaj Bjorner 7e29cc0b12 Merge branch 'master' of https://github.com/z3prover/z3 2018-06-29 08:52:44 -07:00
Nikolaj Bjorner c429455f10 visit parameters during occurs count 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-29 08:52:25 -07:00
Lev Nachmanson 4641d5f32d fixes to get z3test.py back on track etc 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 21:30:41 -07:00
Nikolaj Bjorner 3da8fe4136
Merge pull request #1710 from agurfinkel/deep_space 
Deep space
 2018-06-28 16:57:02 -07:00
Lev Nachmanson 40a363d249 Nikolaj's changes in rationals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 16:22:40 -07:00
Lev Nachmanson c2f3428373 name change 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 15:02:23 -07:00
Lev Nachmanson fd8f972cac grammar 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 13:53:38 -07:00
Arie Gurfinkel 9b578083f5 Avoid non-linear arithmetic in qgen 2018-06-28 16:50:43 -04:00
Lev Nachmanson c986dfe97b change in an SASSERT 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 13:41:59 -07:00
Arie Gurfinkel 5e87d7c4a3 Formatting: move q3 parameters closer together 2018-06-28 15:38:51 -04:00
Arie Gurfinkel bd63458778 Shuffle assumptions on every call 
Order of assumptions appears to make a huge difference on what lemmas
are discovered. Shuffling the assumptions ensures that the solver
is never stuck with any bad order.
 2018-06-28 15:38:51 -04:00
Arie Gurfinkel 6422fa3739 Fix arithmetic equality solver in qgen 2018-06-28 15:38:51 -04:00
Arie Gurfinkel 41a05e9d58 Add methods to print pob 2018-06-28 15:38:51 -04:00
Arie Gurfinkel a63e4b48ca Fix order of arguments when normalizing a conjunction 2018-06-28 15:38:51 -04:00
Arie Gurfinkel a8c9e3a837 Bug fix in qgen 2018-06-28 15:38:50 -04:00
Arie Gurfinkel e8e27f0daf Don't simplify bounds when normalizing a lemma 2018-06-28 15:38:50 -04:00
Lev Nachmanson 2087ee3fb0 restore some code that was removed during the rebase 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-06-28 11:59:01 -07:00
Nikolaj Bjorner f7512d6d5c
Merge pull request #1709 from nunoplopes/master 
MAM: check soft limits before calling the interpreter
 2018-06-28 10:31:00 -07:00
Nuno Lopes 46799cb3f0 MAM: check soft limits before calling the interpreter 2018-06-28 18:25:22 +01:00
Nikolaj Bjorner 18121e5241
Merge pull request #1707 from agurfinkel/deep_space 
Deep space
 2018-06-28 05:38:25 -07:00