3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Commit graph

10624 commits

Author SHA1 Message Date
Nuno Lopes c0f7afacc4 bump cmake minimum version to 3.4 as it was released 3+ years ago
some misc compiler flags cleanup
2019-03-07 09:58:36 +00:00
Nikolaj Bjorner c7bbf2f8de Merge branch 'master' of https://github.com/z3prover/z3 2019-03-07 00:07:54 -08:00
Nikolaj Bjorner 9d2a106838 unused variable warning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-07 00:07:48 -08:00
Nikolaj Bjorner f7773fdcc8 rewrite quantifiers in model evaluator #2171
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-06 22:04:31 -08:00
Nikolaj Bjorner 5abc4a6d68 rewrite quantifiers in model evaluator #2171
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-06 22:03:57 -08:00
Nikolaj Bjorner 65f0da9806
Merge pull request #2170 from mtrberzi/issue2092
z3str3: fix str.indexof with offset (issue #2092)
2019-03-06 17:36:46 -08:00
Nikolaj Bjorner de7731fd22
Merge pull request #2167 from Egor18/master
Fix misprint
2019-03-06 17:36:28 -08:00
Nikolaj Bjorner d6e0f7659d Merge branch 'master' of https://github.com/z3prover/z3 2019-03-06 10:18:36 -08:00
Nikolaj Bjorner 5a02edc8cd add recognizer for distinct
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-06 10:18:29 -08:00
Murphy Berzish e05596e7e5 z3str3: fix str.indexof with offset (issue #2092) 2019-03-06 11:41:56 -05:00
Nuno Lopes 7ad4ced12f librt no longer needed(?) 2019-03-06 12:16:48 +00:00
Nuno Lopes c4d9754eef cmake: remove old directive 2019-03-06 11:12:18 +00:00
Egor Bredikhin 21be4e6d16
Fix misprint 2019-03-05 17:09:27 -05: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 5c13acbf9f remove print directive that doesn't compile
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 20:48:13 -08:00
Nikolaj Bjorner 0c0e79a937 add logging to lar-solver to capture state for unbounded optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 20:33:12 -08:00
Nikolaj Bjorner 19e7b75536 set status optimal also on object
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 19:31:51 -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 752ac09fee fix #2161
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 14:30:59 -08:00
Nikolaj Bjorner 7b4c919fcf stubs for stronger array equality rewriting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 14:11:05 -08:00
Nikolaj Bjorner 6c331279ae fix array regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 13:22:12 -08:00
Nikolaj Bjorner 8b261df77a Merge branch 'master' of https://github.com/z3prover/z3 2019-03-03 13:10:16 -08:00
Nikolaj Bjorner e51b5fd99c fix t154 regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 13:10:11 -08:00
Nikolaj Bjorner 3723c1af0a
Merge pull request #2166 from levnach/Prover
fixes in indices in lar_solver::maximize_term()
2019-03-03 13:00:51 -08:00
Lev Nachmanson 06725de477 fixes in indices in lar_solver::maximize_term()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2019-03-03 10:57:25 -10:00
Nikolaj Bjorner 8e812ea239 revert fix for #2164
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 12:51:26 -08:00
Nikolaj Bjorner 7399f78dfd disable model compression for regressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 12:40:59 -08:00
Nikolaj Bjorner 3ee5c0e7d9 fix #2164 address some of simplification shortcommings from #2151 #2152 #2153
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-03-03 11:33:44 -08:00
Nuno Lopes ccc170a06e model evaluator: cleanup cache when model_eval param changes 2019-03-02 16:42:18 +00:00
Nikolaj Bjorner 210e448666
Merge pull request #2163 from levnach/Prover
enable lar_solver::constraint_holds
2019-03-01 08:37:06 -08:00
Nikolaj Bjorner 006590f329 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-28 14:29:20 -08:00
Nikolaj Bjorner a2dddbd7a5 check pb solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-28 14:28:03 -08:00
Lev Nachmanson 69f03952a7 enable lar_solver::constraint_holds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2019-02-28 12:11:34 -10:00
Nikolaj Bjorner e76cea4684 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 11:44:45 -08:00
Nikolaj Bjorner 6d9b746e70 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 11:42:48 -08:00
Nikolaj Bjorner 69d7d8ff87 local
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-28 11:42:17 -08:00
Nikolaj Bjorner 5fa5719c6f fix #2159
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-28 08:58:58 -08:00
Nikolaj Bjorner b632c08fe0 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 08:35:26 -08:00
Nikolaj Bjorner 4c76d43670 add binary_merge encoding option
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-28 08:35:22 -08:00
Nuno Lopes 6a0c409b0f move a few strings instead of copying 2019-02-28 10:53:27 +00:00
Nikolaj Bjorner 2417bedb98 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-27 14:43:44 -08:00
Nikolaj Bjorner a2dcf87e10 add ESRP signing of nuget packages
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-27 14:43:39 -08:00
Nikolaj Bjorner e79f7ca1fd
Merge pull request #2150 from Nils-Becker/master
Logging Support for Theory Solvers
2019-02-27 17:06:31 +01:00
Nikolaj Bjorner ea9e2f6642 fix #2158
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-26 15:13:47 -08:00
Nikolaj Bjorner c4ee4ffae4 fix pre-prejection>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-26 07:12:34 -08:00
Nikolaj Bjorner bef509b02e Yakir!
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-25 19:20:35 -08:00
Nikolaj Bjorner d9b4f237fe remove opt dependency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-25 18:18:19 -08:00
Nikolaj Bjorner 46f3b7374c Merge branch 'master' of https://github.com/z3prover/z3 2019-02-25 18:15:28 -08:00
Nikolaj Bjorner 4876426866 project
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-25 18:15:24 -08:00