3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

8168 commits

Author SHA1 Message Date
Nikolaj Bjorner 18e75dc001 Merge branch 'master' of https://github.com/z3prover/z3 2018-03-19 13:34:17 -07:00
Nikolaj Bjorner ebc6ec2eb5 fix #1547 by rewriting legacy recognizers to SMT-LIB2.6 style recognizers which are assumed by theory_datatype
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-19 13:33:58 -07:00
Murphy Berzish a988d01537 add const to iterator loops where it can be used 2018-03-19 12:25:44 -04:00
Murphy Berzish d569485170 Merge remote-tracking branch 'upstream/master' into refactoring 2018-03-19 01:43:18 -04:00
Nikolaj Bjorner b572639fcd fix #1545
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-17 17:49:33 -07:00
Nikolaj Bjorner 72f8e408fc fix #1538
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-17 11:25:07 -07:00
Nikolaj Bjorner aa913c564c moving more std::map std::set to obj_*, #1529
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-17 04:21:28 -07:00
Nikolaj Bjorner f59d4c6ac0 Merge branch 'master' of https://github.com/z3prover/z3 2018-03-16 19:30:23 -07:00
Nikolaj Bjorner 5dd7e2c520 fix #1544
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-16 19:30:13 -07:00
Nikolaj Bjorner b12a1caa07 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-16 09:05:44 -07:00
Nikolaj Bjorner b93a04c38f Merge branch 'master' of https://github.com/z3prover/z3 2018-03-16 07:46:35 -07:00
Nikolaj Bjorner 86d3bbe6cb added TODO markers in theory_str.h for moving to obj_map, remove include of stdbool for now
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-16 07:46:27 -07:00
Nikolaj Bjorner 3a4a58ecfd
Merge pull request #1541 from fmgoncalves/patch-1
Fix #1540 Remove extraneous function
2018-03-16 07:40:13 -07:00
Nikolaj Bjorner 1c8e71bd8b
Merge pull request #1542 from waywardmonkeys/doc-fixes
Fix minor issues in docs.
2018-03-16 07:39:50 -07:00
Bruce Mitchener 0a0b7a9635 Fix minor issues in docs. 2018-03-16 20:56:06 +07:00
Filipe Gonçalves e4cab7bc83
Fix #1540 Remove extraneous function
Remove extra __deepcopy__ function definition that shadows working implementation.
2018-03-16 22:04:39 +10:00
Murphy Berzish 6bb9a82425 experimental axiom-persist for regex conflict clauses 2018-03-15 13:56:44 -04:00
Nikolaj Bjorner b1f05d8271 fix #1539
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-14 18:14:29 -07:00
Nikolaj Bjorner 46048d5150 change lemma display utility to use updated pretty printer
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-14 12:15:13 -07:00
Nikolaj Bjorner 776a7d4e6c Merge branch 'master' of https://github.com/z3prover/z3 2018-03-14 09:04:10 -07:00
Nikolaj Bjorner 5e2723a16e java
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-14 09:04:08 -07:00
Nikolaj Bjorner c229518953 Merge branch 'master' of https://github.com/z3prover/z3 2018-03-14 07:29:38 -07:00
Nikolaj Bjorner 2b2aee3c18 remove unused operators #1530
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-14 07:29:26 -07:00
Nikolaj Bjorner eb5f5e8294
Merge pull request #1537 from DeforaNetworks/khorben/netbsd
Add support for NetBSD
2018-03-13 20:26:46 -07:00
Pierre Pronchery 5f7bd993de Add support for NetBSD
Originally from David Holland <dholland@NetBSD.org>.
2018-03-13 21:59:35 +01:00
Murphy Berzish b5471e7fe0 refactor: use c++11 for (part 1) 2018-03-12 20:04:04 -04:00
Murphy Berzish 73f7e301c3 preliminary refactoring to use obj_map 2018-03-12 17:09:55 -04:00
Nikolaj Bjorner 5651d00751 fix #1534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-12 13:21:31 -07:00
Murphy Berzish 11a339c490 fix include path 2018-03-11 23:26:30 -04:00
Murphy Berzish 49b810e00f Merge branch 'master' into regex-develop 2018-03-11 23:18:55 -04:00
Nikolaj Bjorner 3d9139f6ef bump revision
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 12:07:55 -08:00
Nikolaj Bjorner 5854492504 add stdbool.h to see whether build system breaks #1526
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 11:59:42 -08:00
Nikolaj Bjorner fb3498cd0b
Merge pull request #1528 from DeforaNetworks/khorben/configure-parameters
Fix parameter expansion when configuring Z3
2018-03-10 14:42:01 -05:00
Nikolaj Bjorner 0ce2001449 fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 11:39:22 -08:00
Nikolaj Bjorner 6e87622c8a remove references to deprecated uses of PROOF_MODE #1531
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-10 13:55:01 -05:00
Nikolaj Bjorner e5a1981694 disable GCC flag change to see if this affects build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-09 15:40:35 -05:00
Pierre Pronchery ae165a539e Fix parameter expansion when configuring Z3 2018-03-09 14:20:31 +01:00
Nikolaj Bjorner db63c9299c Merge branch 'master' of https://github.com/z3prover/z3 2018-03-09 05:32:15 -05:00
Nikolaj Bjorner ba603307fc remove stale deprecated annotation #1525
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-09 05:32:01 -05:00
Nikolaj Bjorner fc835ba01e
Merge pull request #1518 from waywardmonkeys/const-proof-checker
Make proof_checker more const correct.
2018-03-09 05:22:49 -05:00
Nikolaj Bjorner 4e31794c44
Merge pull request #1519 from waywardmonkeys/colorize-output-with-ninja
Force color output with Ninja.
2018-03-09 05:18:50 -05:00
Nikolaj Bjorner 895d30a1ff
Merge pull request #1527 from waywardmonkeys/fix-typos
Fix typos.
2018-03-09 05:18:01 -05:00
Bruce Mitchener 878a6ca14f Fix typos. 2018-03-09 14:30:43 +07:00
Nikolaj Bjorner 4f9d198c51
Merge pull request #1517 from mtrberzi/issue1379
Handle third argument of str.indexof in Z3str3
2018-03-08 14:19:01 -08:00
Murphy Berzish bf6975122b integrate contains and indexof in theory_str 2018-03-08 12:37:44 -05:00
Nikolaj Bjorner 02a9696701 fix #1521
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-08 11:19:00 -05:00
Murphy Berzish d1407e843d Merge branch 'issue1379' of github.com:mtrberzi/z3 into issue1379 2018-03-07 18:16:17 -05:00
Murphy Berzish a7caa2fd2a remove useless get_assignments in theory_str final check 2018-03-07 18:16:11 -05:00
Nikolaj Bjorner 246941f2d3 fix #1522
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-07 14:26:38 -08:00
Murphy Berzish fd6d9a9489 Merge branch 'issue1379' of github.com:/mtrberzi/z3 into issue1379 2018-03-07 13:54:45 -05:00