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

7266 commits

Author SHA1 Message Date
Nikolaj Bjorner 4b71bfc95d mac build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 19:19:42 -07:00
Nikolaj Bjorner ff2924e83b fix mac build error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 17:19:40 -07:00
Nikolaj Bjorner abc274e290 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 14:58:12 -07:00
Nikolaj Bjorner d99068e412
Merge pull request #1546 from mtrberzi/refactoring 
theory_str determinism refactoring
 2018-03-20 13:38:50 -07:00
Nikolaj Bjorner 931dbd5933 remove python doc test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-20 13:37:04 -07:00
Murphy Berzish 7759d05efe fix use-after-free 2018-03-19 23:09:07 -04: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 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
Murphy Berzish d26eddf776 re-add indexof-contains heuristic 2018-03-19 18:31:26 -04:00
Murphy Berzish 1f4bfcb4e5 fix indexof subterm 2018-03-19 18:10:06 -04:00
Murphy Berzish 5c692dc79d fixups to theory_str indexof and axiom handling loop 2018-03-19 18:06:42 -04:00
Murphy Berzish 84c30e0b60 theory_str fixups for new collections 2018-03-19 17:03:01 -04:00
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
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 8602c52bc9 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-19 10:41:42 -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
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
Nikolaj Bjorner af96e42724 fixing local search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-15 21:11:55 -07:00
Murphy Berzish 6bb9a82425 experimental axiom-persist for regex conflict clauses 2018-03-15 13:56:44 -04: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 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 bf8ea92b99 fixing nls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-13 17:23:58 -07:00
Pierre Pronchery 5f7bd993de Add support for NetBSD 
Originally from David Holland <dholland@NetBSD.org>.
 2018-03-13 21:59:35 +01: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
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
Nikolaj Bjorner e7d43ed516 fix pb rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-12 11:22:05 -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 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 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 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
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
Bruce Mitchener 4cc9362851 Make proof_checker more const correct. 2018-03-07 13:18:39 +07:00
Murphy Berzish f43a027447 Merge branch 'develop' into issue1379 2018-03-06 22:14:18 -05: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 eb1122c5cb delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-04 21:57:08 -08:00
Nikolaj Bjorner 534a31f74e inherit solver parameters in asserted formulas rewriter. #1511 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-04 05:06:36 -08:00
Nikolaj Bjorner a64fd7145c remove buggy legacy code, rely on pull_cheap_ite option in rewriter, #1511 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-04 03:36:03 -08:00
Nikolaj Bjorner 205d77d591 save last model to ensure it is available fixes #1514 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-03 19:26:31 -08:00
Nikolaj Bjorner 8e09a78c26 fix #1510 by reintroducing automatic declaration of recognizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-02 23:02:20 +09:00
Nikolaj Bjorner a738f5af12 fix #1512 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-02 20:14:59 +09:00
Nikolaj Bjorner 00c3f4fdcd fix bugs found while running sample from #1112 in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-28 22:35:41 +09:00
Nikolaj Bjorner 30de514a88 fix topological traversal crash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-28 11:59:17 +09:00
Nikolaj Bjorner b79d1a6956 fix #1488 for smtlib basic printer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-28 09:22:20 +09:00
Murphy Berzish ac9b03528a add re.allchar support in z3str3 2018-02-26 17:19:45 -05:00
Nikolaj Bjorner 5d457c95aa update registration of built-ins 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-26 21:00:41 +09:00
Nikolaj Bjorner 0199c7515f fix z3.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-26 19:49:13 +09:00
Nikolaj Bjorner ce1b135ec3 address accessor inconsistencies between - and from #1506 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-26 14:57:17 +09:00
Nikolaj Bjorner 45b6e0998a Merge branch 'master' of https://github.com/z3prover/z3 2018-02-25 13:19:59 +09:00
Nikolaj Bjorner e9b6de0746
Merge pull request #1501 from mikhailramalho/master 
Convert BVULT(X,Y) into !BVULE(Y,X)
 2018-02-25 13:19:11 +09:00
Nikolaj Bjorner d5f83205ac
Merge pull request #1495 from AngusL/master 
Fix Python FiniteDomainSortRef.size()
 2018-02-25 13:16:17 +09:00
Nikolaj Bjorner 5741786f3e
Merge pull request #1503 from cocreature/fid-order 
Fix assignment of family ids
 2018-02-25 13:15:40 +09:00
Nikolaj Bjorner 7b68be75c9 fixes to #1500 and #1457 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-25 13:11:20 +09:00
Nikolaj Bjorner 9279cbfbac don't reinit assumptions when the solver is unsat. fixes #1502 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-24 16:30:08 +09:00
Moritz Kiefer 5d0e33c9ad Fix assignment of family ids 2018-02-23 20:22:07 +01:00
Mikhail Ramalho c5336f8003 Convert BVULT(X,Y) into !BVULE(Y,X) 
Signed-off-by: Mikhail Ramalho <mikhail.ramalho@gmail.com>
 2018-02-23 17:17:02 +00:00
Lev Nachmanson a238a0a37d fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-02-22 17:07:21 -08:00
Lev Nachmanson dbe5df85c3 fix the override warning 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-02-22 08:44:50 -08:00
Nikolaj Bjorner 41e0a12678 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-22 09:22:30 +09:00
Nikolaj Bjorner 6ed95718ce fix more warnings with override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-22 08:53:17 +09:00
Nikolaj Bjorner 919989cfe8 fix more warnings with override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-22 08:39:31 +09:00
Nikolaj Bjorner a4c58ec4c2 fix #1496 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-22 08:05:28 +09:00
Nikolaj Bjorner d70ee71a43 try another build fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 22:38:10 +09:00
Nikolaj Bjorner 763c250734 try another build fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 22:33:44 +09:00
Nikolaj Bjorner 24f56fd74c try another build fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 22:29:22 +09:00
Nikolaj Bjorner 7b6f51941c fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 22:18:47 +09:00
Nikolaj Bjorner b3fa5d7978 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-21 21:59:00 +09:00
Nikolaj Bjorner 54b00f357b fix rule inlining, add WithParams to pass parameters directly to python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-21 21:57:54 +09:00
Angus Lepper 7b91195770
Fix Python FiniteDomainSortRef.size() 2018-02-20 19:37:17 +00: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
Moritz Kiefer b0997661cc Insert sort declaration for nullary sorts declared using declare-datatype 2018-02-19 17:53:53 +01:00
TheRealNebus e5aa79ba6a disjoint cores 2018-02-19 13:29:15 +00:00
Nikolaj Bjorner a2f907c7d1 fix #1492 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-18 13:20:15 -08:00
Nikolaj Bjorner c7063631e1 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-16 12:07:23 -08:00
TheRealNebus 3a7efb91ae implemented CLD 2018-02-16 19:48:29 +00:00
TheRealNebus 3bbc09c1d2 MSS based MaxSMT solver 2018-02-16 14:44:22 +00:00
Nikolaj Bjorner fadcac8f6d fix #1491 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-15 12:39:08 -08:00
Nikolaj Bjorner a231ff3735 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-14 21:47:25 -08:00
Nikolaj Bjorner 0bbdee810d fix #1488 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-14 21:46:20 -08:00
Nikolaj Bjorner 1323b8f63f
Merge pull request #1485 from waywardmonkeys/modernize-redundant-void-arg 
Remove redundant void arg.
 2018-02-13 08:14:05 -08:00
Bruce Mitchener 971a5eddcb Use bool literal false instead of 0. 2018-02-13 19:23:47 +07:00
Bruce Mitchener 7bf80c66d0 Remove redundant void arg. 
While this was needed in ANSI C, it isn't in C++ and triggers a warning
in clang-tidy when `modernize-redundant-void-arg` is enabled.
 2018-02-13 18:51:52 +07:00
Nikolaj Bjorner eab7ae58be fix #1484 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-12 23:30:10 -08:00
Murphy Berzish 762129d4c7 fixups to theory_str for regex 2018-02-12 17:45:07 -05:00
Murphy Berzish 54206e3674 Merge branch 'develop' into regex-develop 
Conflicts:
	src/smt/theory_str.h
 2018-02-12 17:25:50 -05:00
Nikolaj Bjorner 792fdb915f remove deprecated comments about bv2int/int2bv being treated as uninterpreted, raise in #1481 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-12 13:07:09 -08:00
Nikolaj Bjorner e1100af52c ensure that final model is logged by the time it is produced fix #1463 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-12 12:04:24 -08:00
Bruce Mitchener 76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07: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
Bruce Mitchener 7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07: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
Bruce Mitchener b7d1753843 Use override rather than virtual. 2018-02-09 21:19:27 +07: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 2b847478a2
Merge pull request #1478 from waywardmonkeys/unnecessary-value-param-fixes 
Remove unnecessary value parameter copies.
 2018-02-09 02:20:47 -08:00
Bruce Mitchener 757b7c66ef Remove unnecessary value parameter copies. 2018-02-09 16:35:34 +07:00
Bruce Mitchener 50f3e9c3c0 Fix typos. 2018-02-09 16:35:26 +07: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 3f7453f5c5 fixing build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 20:23:31 -08:00
Nikolaj Bjorner 61934d8106 align semantics of re.allchar with string proposal. #1475 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 20:08:15 -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
Nikolaj Bjorner 25eeb7aeac fix build isses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:39:56 -08:00
Nikolaj Bjorner 6f610674fa fix errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:31:57 -08:00
Nikolaj Bjorner 61f99b242e xor to xr to avoid clang issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:25:02 -08:00
Nikolaj Bjorner fa0c75e76e rename to core2 to avoid overloaded virtual 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:13:13 -08:00
Nikolaj Bjorner 5a8154c156 fix errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 14:47:16 -08:00
Nikolaj Bjorner 734d48fa33 fix errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 14:29:28 -08:00
Nikolaj Bjorner 10894069b0 fix compiler error reported by Luca 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 13:19:40 -08:00
Nikolaj Bjorner bee4716a85 lia2card simplifications, move up before elim01 (which could be deprecated) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 12:56:30 -08:00
Nikolaj Bjorner 1ee7871bbf to fix #1476 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-06 18:48:03 -08:00
Nikolaj Bjorner 43441d0fd5 add LP parser option to front-end and opt context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-06 14:02:44 -08:00
Nikolaj Bjorner cb6896087d fix #1468 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-06 10:21:02 -08:00
Nikolaj Bjorner 159e6ad987
Merge pull request #1472 from levnach/dev 
adding template definitions
 2018-02-06 07:52:16 -08:00
Lev Nachmanson c74ad46682 remove a duplicate definition 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-02-05 21:22:46 -08:00
Nikolaj Bjorner 309012e127
Merge pull request #1474 from waywardmonkeys/inconsistent-missing-override 
Fix inconsistent missing override warnings.
 2018-02-05 20:33:56 -08:00
Bruce Mitchener 5911f810ed Fix inconsistent missing override warnings. 2018-02-06 11:23:08 +07:00
Bruce Mitchener 54b3cd0071 Reserve vector space when possible. 
This fixes all current instances of the
`performance-inefficient-vector-operation`
warning in clang-tidy.
 2018-02-06 11:21:17 +07:00
Nikolaj Bjorner b2bd4dd3b4 fix #1471 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-05 18:54:14 -08:00
Nikolaj Bjorner b8680f8a46 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-05 18:33:39 -08:00
Nikolaj Bjorner a1d4e485a4 fix #1469 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-05 18:33:31 -08:00
Nikolaj Bjorner 9d37257059
Merge pull request #1465 from waywardmonkeys/fix-typos 
thanks
 2018-02-05 18:31:09 -08:00
Nikolaj Bjorner 3e810d6c54 remove static from format (not thread safe), remove std::move #1466 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-05 16:46:49 -08:00
Nikolaj Bjorner 2853558bc2
Merge pull request #1466 from waywardmonkeys/reduce-copying 
Use const refs to reduce copying.
 2018-02-05 16:37:44 -08:00
Lev Nachmanson a5caa50606 adding template definitions 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-02-05 09:42:56 -08:00
Nikolaj Bjorner e332652989 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-04 20:54:49 -08:00
Nikolaj Bjorner 885dfad237 fix #1458 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-04 20:54:21 -08:00
Christoph M. Wintersteiger 175273fe27 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-02-04 22:43:43 +00:00
Nikolaj Bjorner caaaa23438 Merge branch 'master' of https://github.com/z3prover/z3 2018-02-04 13:06:54 -08:00
Nikolaj Bjorner bf04c38a63 add logging for #1470 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-04 13:06:14 -08:00
Nikolaj Bjorner 20d6543538 set uninitialized fields. Maybe related to #1468 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-04 12:56:21 -08:00
Nikolaj Bjorner 20fe08d80c fix more bugs with compilation of pb equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-04 09:51:45 -08:00
Nikolaj Bjorner 354c16454a fix bug in translation of pbeq into sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-03 22:19:25 -08:00
Nikolaj Bjorner badb32f9ae neatify rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-03 16:33:14 -08:00
Nikolaj Bjorner d07688d80b update lia2card to handle broader intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-03 15:52:34 -08:00
Nikolaj Bjorner db347c007d remove legacy bce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-03 09:39:39 -08:00
Christoph M. Wintersteiger 333374229d Fixed UFs for unspecified cases of FP conversion operators. Thanks for Youcheng Sun for reporting this bug. 2018-02-03 16:48:05 +00:00
Christoph M. Wintersteiger c3ed986031 Fixed RNA FP rounding mode semantics. Fixes #1190 and bugs reported by Youcheng Sun. 2018-02-03 16:46:21 +00:00
Christoph M. Wintersteiger 8689921e9c Fixed missing bit of precision in fp.to_ubv/fp.to_sbv. Thanks to Youcheng Sun for reporting this bug. 2018-02-03 15:16:23 +00:00
Nikolaj Bjorner e95840b640 ate/acce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-02 20:51:41 -08:00
Christoph M. Wintersteiger ad3b0ecad0 Fixed pattern rewriting to produce only valid patterns (which led to a segfault). Bug reported by Youcheng Sun. 2018-02-02 19:27:36 +00:00
Nikolaj Bjorner a6ac6958a6 fix gcc compilation error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-02 09:48:02 -08:00
Nikolaj Bjorner 161ee1c108 fix ugcd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-01 20:23:21 -08:00
Nikolaj Bjorner ad92bfb1a1 fix python build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-01 20:19:24 -08:00
Nikolaj Bjorner eca250933d disable uhle from lookahead solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-01 19:56:01 -08:00
Bruce Mitchener ae8027e594 Fix typos. 2018-02-01 19:39:43 +07:00
Nikolaj Bjorner 75bf942237 throttle cce pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-31 21:15:07 -08:00
Nikolaj Bjorner a639452553 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-01-31 11:10:54 -08:00
Nikolaj Bjorner 7ada6c25d9 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-31 11:10:42 -08:00
Nikolaj Bjorner e32bfda5a6 fixup cce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-31 10:21:27 -08:00
Nikolaj Bjorner 2739342aba fix updates to cce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-30 23:41:04 -08:00