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

11275 commits

Author SHA1 Message Date
Nikolaj Bjorner c2e5cd78c8 change lar_terms to use column indices 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-06 12:13:59 -07:00
Nuno Lopes 3313590b95 fix #3713: too much caching in dom-simplify for OR expressions 2020-04-06 12:11:26 +01:00
Nuno Lopes 346d852bbd fix build 2020-04-06 11:19:04 +01:00
Nikolaj Bjorner 9e7af79094 initialization order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 18:16:40 -07:00
Nikolaj Bjorner b9c9687caf bool_vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 18:14:56 -07:00
Nikolaj Bjorner da6297f31f bool_vector 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 17:41:19 -07:00
Nikolaj Bjorner dff5071598 compile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 17:03:26 -07:00
Nikolaj Bjorner daa904c9d2 fix #3778 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 15:13:36 -07:00
Nikolaj Bjorner b79b8c9bc4 fix #3777 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 15:08:28 -07:00
Nikolaj Bjorner 406c0792f1 fix #3775 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 14:04:00 -07:00
Nikolaj Bjorner bb1119a6ca fix #3774 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 13:59:28 -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 2ed26e8e73 fix #3762 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 12:10:02 -07:00
Nikolaj Bjorner efc02282f4 fix #3758 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 12:01:17 -07:00
Nikolaj Bjorner 1949a978ce fix #3760 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 11:39:25 -07:00
Nikolaj Bjorner 077f2248ca fix #3756 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 11:32:53 -07:00
Nikolaj Bjorner 54d981e88f fix #3757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 11:25:29 -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 080dbb13b0 tv alignment, code review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 03:35:19 -07:00
Nikolaj Bjorner fddbac0f52 use tv for interfacing on get_term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 02:42:00 -07:00
Nikolaj Bjorner 296a97d0d3 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 01:03:38 -07:00
Nikolaj Bjorner 399cf75ad4 fpa warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 00:55:13 -07:00
Nikolaj Bjorner 9e374d6514 remove trace for #3725 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 00:53:16 -07:00
Nikolaj Bjorner 4842c71019 fix #3537 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 00:38:14 -07:00
Nikolaj Bjorner eacde16b3e fix #3199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:55:44 -07:00
Nikolaj Bjorner 8118292def fix #3754 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:20:44 -07:00
Nikolaj Bjorner 7477e96e59 fix #3519 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:18:15 -07:00
Nikolaj Bjorner 5516e420a1 disable bapa from smt interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:09:28 -07:00
Nikolaj Bjorner e419565239 fix #3751 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 23:01:30 -07:00
Nikolaj Bjorner 7ae9734db2 fix #3752 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 22:56:41 -07:00
Nikolaj Bjorner 2f80acb1bc fix #3543 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 21:56:46 -07:00
Nikolaj Bjorner 0fc8ebc8cc fix #3683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 18:56:10 -07:00
Nikolaj Bjorner 7e8753cd3f fix #3726 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 18:48:09 -07:00
Nikolaj Bjorner 10768bd005 fix #3727 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 18:41:13 -07:00
Nikolaj Bjorner 6ac19ed8d0 fix #3728 - fail only model validation if the expression is false, there are too many false positives being reported 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 18:34:32 -07:00
Nikolaj Bjorner 82d7ca46ba fix #3729 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 18:06:23 -07:00
Nikolaj Bjorner fadc3761bd fix #3731 - abuse of parameter combinations, trying to use qsat on arrays, but disabling array equality expansion during model evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 17:06:43 -07:00
Nikolaj Bjorner 8faf35e2e0 fix #3735 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 16:47:00 -07:00
Nikolaj Bjorner 9fbe178de4 fix #3735 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 16:36:54 -07:00
Nikolaj Bjorner 7838e99f47 fix #3749 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 14:45:29 -07:00
Nikolaj Bjorner 8d59355b88 fix #3750 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 14:37:51 -07:00
Nikolaj Bjorner 0735491557 path fix #3747, this patches incoherent behavior of terms / ival from lar_solver. The variables occurring in terms are mapped to columns and not as original variables/terms. theory_lra has to interact with the column_corresponds_to_term test instead of relying on the terms themselves carrying the relevant information 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 14:27:56 -07:00
Nikolaj Bjorner 121a6de32c fix #3748 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 13:22:30 -07:00
Nikolaj Bjorner 031b3a55ef fix #3733 persist uninterpreted atoms across calls to incremental sat solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 13:11:39 -07:00
Nikolaj Bjorner c70e9af09d fix #3734 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 12:53:24 -07:00
Nikolaj Bjorner 64d157d81e fix #3739 - dependencies may be valid even if they are null 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 11:58:39 -07:00
Nikolaj Bjorner c26d3f5437 fix #3740 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 11:31:29 -07:00
Nikolaj Bjorner df1c6c8a21 fix #3742 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 11:27:37 -07:00
Nikolaj Bjorner b4aba81e35 fix #3743 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 11:00:04 -07:00
Nikolaj Bjorner 41e11857e5 fix #3744 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 10:57:49 -07:00
Nikolaj Bjorner 9531c5e167 fix #3573 fix #3723 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 10:45:57 -07:00
Nikolaj Bjorner 31e16c7d60 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 20:20:33 -07:00
Nikolaj Bjorner f4472927c0 play nice with sanitizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 17:39:22 -07:00
Nikolaj Bjorner 6f65051f2c silence some build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 17:11:34 -07:00
Nikolaj Bjorner 8cb59fe8a6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 17:06:06 -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 0b856638e9 fix #3721 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 15:31:44 -07:00
Nikolaj Bjorner 3bd340af44 fix #3705 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 15:08:35 -07:00
Nikolaj Bjorner 759fb03daf fix #3695 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 14:39:56 -07:00
Nikolaj Bjorner 918b6a8c03 trace & threads = undef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 13:58:22 -07:00
Nikolaj Bjorner a839017cc6 fix #3709 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 13:53:09 -07:00
Nikolaj Bjorner b642686dca fix #3678 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 13:28:37 -07:00
Shaoyuan CHEN a119953676
z3py: fix And/Or context deduction (#3687) 2020-04-03 13:13:51 -07:00
Lev Nachmanson 9d58fccd41 fix in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-03 12:43:20 -07:00
Lev Nachmanson 7890555455 fix in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-03 12:37:57 -07:00
Nikolaj Bjorner c25975a429 fix #3703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 12:35:20 -07:00
Nikolaj Bjorner bbc63cd5b5 fix #3714 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 12:28:05 -07:00
Nikolaj Bjorner f92c6ad170 fix #3708 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 12:23:54 -07:00
Nikolaj Bjorner cd2f6705aa fix #3715 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 12:05:48 -07:00
Nikolaj Bjorner 8e033c1e71 fix #3716 fix #3719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 12:05:48 -07:00
Lev Nachmanson 7fe46de266 trace random update 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-03 12:00:19 -07:00
Nikolaj Bjorner fd2eab85f1 fix #3717, non-linear requires reflection 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 10:55:48 -07:00
Nikolaj Bjorner 9092cdc3a5 remove stdout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 10:42:17 -07:00
Nikolaj Bjorner 50624723af fix #3704 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 10:38:31 -07:00
Nikolaj Bjorner c431a100b7 fix #3707 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 21:31:01 -07:00
Nikolaj Bjorner 64a0e62648 fix #3699 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 21:17:01 -07:00
Nikolaj Bjorner be3a9b227c fix #3699 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 20:35:15 -07:00
Nikolaj Bjorner 26192e848c fix #3675 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 17:41:06 -07:00
Lev Nachmanson afce09efe4 assert that the sdi is infinite by default 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-02 15:58:46 -07:00
Lev Nachmanson b45311cc7c use only scoped intervals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-02 15:58:46 -07:00
Lev Nachmanson cf3f06ee26 use scoped interval 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-02 15:58:46 -07:00
Nikolaj Bjorner 896a1b2048 fix #3679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 15:04:56 -07:00
Nikolaj Bjorner f98b94bdbc fix #3680 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 15:04:56 -07:00
Nikolaj Bjorner bab879c832 fix #3685 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 15:04:56 -07:00
Lev Nachmanson 55329ea935 more fixes in patching of monomials 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-02 14:47:06 -07:00
Nikolaj Bjorner 2d01c64d2c fix #3682 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 12:30:25 -07:00
Nikolaj Bjorner 700ad1f2b9 fix #3689 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 11:33:22 -07:00
Nikolaj Bjorner a7aff1bcf0 fix regression on string ops 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 10:03:35 -07:00
Nikolaj Bjorner 3eefd18c58 fix #3688 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 09:59:16 -07:00
Nikolaj Bjorner 8290cfadcc fix #3694 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 08:05:43 -07:00
Nikolaj Bjorner 57d430b3fd fix #3700 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 06:38:14 -07:00
Nikolaj Bjorner 78ebe0a94c fix #3701 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-02 06:22:32 -07:00
Nikolaj Bjorner b686bb61fe fix #3673 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 18:18:44 -07:00
Nikolaj Bjorner 2ac8d3461e fix #3670 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:35:53 -07:00
Nikolaj Bjorner 4c69f9e31b invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:27:06 -07:00
Nikolaj Bjorner f0a6837c67 invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:17:09 -07:00
Nikolaj Bjorner ea08fcf65c invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:15:48 -07:00
Lev Nachmanson 0dc5bad6e4 fix in patching of monics 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-01 12:58:34 -07:00