3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Commit graph

8250 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
41cb287079 re-add cpp file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 15:48:34 -08:00
Nikolaj Bjorner
4ecf186580 remove files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-02-07 15:43:33 -08:00