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

8252 commits

Author SHA1 Message Date
Nikolaj Bjorner 76eae5fa5c add mac build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-20 16:57:01 -07:00
Nikolaj Bjorner dc01266354 fixing after clone
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 20:50:24 -07:00
Nikolaj Bjorner d5bd7878b3 fix example test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 20:03:47 -07:00
Nikolaj Bjorner d5811a13eb add test-benchmarks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 19:18:05 -07:00
Nikolaj Bjorner b727a3463d update vsts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 18:21:34 -07:00
Nikolaj Bjorner b002477d1a fix java API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 18:10:57 -07:00
Nikolaj Bjorner ac2fe879ae update script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 15:55:00 -07:00
Nikolaj Bjorner 965da74d01 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-03-19 15:49:40 -07:00
Nikolaj Bjorner 9598045435 fix java
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 15:49:28 -07:00
Nikolaj Bjorner ba2e28fa0e update build script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 14:55:38 -07:00
Nikolaj Bjorner 7ded2a90e6 remove unreachable from vector
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 11:55:18 -07:00
Nikolaj Bjorner 7a64c82d99 comment out pull
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 11:15:49 -07:00
Nikolaj Bjorner a873cc41bf update vsts script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 10:43:59 -07:00
Nikolaj Bjorner 8602c52bc9 fix test build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 10:41:42 -07:00
Nikolaj Bjorner afb12fe6c3 move script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-18 17:22:58 -07:00
Nikolaj Bjorner 785b7f3e6a vsts cmd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-18 17:03:06 -07:00
Nikolaj Bjorner b82214ef0d try paths to vsvars
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-18 16:59:41 -07:00
Nikolaj Bjorner a7e0f18482 vsts cmd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-18 16:53:04 -07:00
Nikolaj Bjorner af96e42724 fixing local search
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-15 21:11:55 -07:00
Nikolaj Bjorner 59b142f803 fixing local search
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-15 06:48:26 -07:00
Nikolaj Bjorner bf8ea92b99 fixing nls
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-13 17:23:58 -07:00
Nikolaj Bjorner 4375f54c45 adding lns
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-13 13:31:27 -07:00
Nikolaj Bjorner 64954cc551 fix pbge and reduce_tr
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-13 09:07:58 -07:00
Nikolaj Bjorner e7d43ed516 fix pb rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-12 11:22:05 -07:00
Nikolaj Bjorner f04e805fa4 add hiding to auxiliary declarations created in mc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-06 18:02:37 -08:00
Nikolaj Bjorner 19b1248e5e Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-03-06 13:33:40 -08:00
Nikolaj Bjorner d3ceb8c794 radix sort experiment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-06 13:33:37 -08:00
Nikolaj Bjorner 718e5a9b6c add unit extraction
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-06 01:08:17 -08:00
Nikolaj Bjorner 75ba65a18a working on propagation with undef main literal
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-20 01:46:35 -08:00
Nikolaj Bjorner 4c1379e8c9 bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-19 21:49:03 -08:00
Nikolaj Bjorner bb4888ce31 support self-subsumption, remove verbose log 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-11 21:21:55 -08:00
Nikolaj Bjorner 8fb7fb9f98 add missing caching of PB/cardinality constraints, increase limit for compiling cardinalities to circuits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-11 19:27:00 -08:00
Nikolaj Bjorner 4695ca16c8 perf improvements
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-10 11:43:33 -08:00
Nikolaj Bjorner e183f8b743 disable lookahead simplification when external solver is used
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-09 21:46:45 -08:00
Nikolaj Bjorner 18b66a4bd7 fix parameter processing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-09 14:20:07 -08:00
Nikolaj Bjorner f28b158d57 fix another recompilation bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-09 13:47:55 -08:00
Nikolaj Bjorner 4f7b6a2f18 fix missing clear of weights
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-09 10:55:31 -08:00
Nikolaj Bjorner 5206e29bdd fix wrong check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-09 09:18:05 -08:00
Nikolaj Bjorner 19b858dbea fix reset code for level marking
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-09 04:00:32 -08:00
Nikolaj Bjorner 908dfd392e fix validation code, disable PB compilation code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-08 14:08:51 -08:00
Nikolaj Bjorner 72a7164e2d add model checker to external
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-08 13:03:57 -08:00
Nikolaj Bjorner a0b5f6937b fix bugs, add soft timeout to opt frontend
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-08 10:05:26 -08:00
Nikolaj Bjorner 4f630f2a00 fix configuration for compiling equalities, add extended binaries
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-08 09:09:53 -08:00
Nikolaj Bjorner 5e482def18 fix local search encoding bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-08 07:27:32 -08:00
Nikolaj Bjorner 615e1e0845 remove redundant tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 17:17:27 -08:00
Nikolaj Bjorner 064a7f9097 remove tautology
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 16:05:06 -08:00
Nikolaj Bjorner d7f2638ecf reference get_wlist
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 16:03:14 -08:00
Nikolaj Bjorner d684d4fce0 dbl-max
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 15:57:25 -08:00
Nikolaj Bjorner 42cc7c7f87 remove file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 15:53:24 -08:00
Nikolaj Bjorner 7a4a2b6b5b remove file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 15:51:22 -08:00