3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Commit graph

10312 commits

Author SHA1 Message Date
Nikolaj Bjorner 6f6880812b Merge branch 'master' of https://github.com/z3prover/z3 2019-01-06 13:01:19 -08:00
Nikolaj Bjorner 71e239c08e fix #2061
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-06 11:49:47 -08:00
Nikolaj Bjorner ed4223af94
Merge pull request #2064 from varming/cv/utf8
Specify UTF-8 encoding in python scripts
2019-01-06 12:58:37 +08:00
Carsten Varming e1a9154555 Specify UTF-8 encoding in python build scripts 2019-01-05 13:48:15 -05:00
Nikolaj Bjorner e770f37f52
Merge pull request #2062 from Chen-Huanyi/master
Implement QUIP variant in mini_quip
2019-01-05 08:05:42 +08:00
Huanyi Chen 19471f9fa3 Implement mini_quip 2019-01-04 18:30:02 -05:00
Huanyi Chen 83e3a79bd1 Remove testcase that takes long time to finish 2019-01-04 17:31:47 -05:00
Nikolaj Bjorner fb397cbe25 remove incorrect assertion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-04 08:18:40 -08:00
Nikolaj Bjorner 425c47bc81 Merge branch 'master' of https://github.com/z3prover/z3 2019-01-04 07:47:00 -08:00
Nikolaj Bjorner 0d400a5ad6 fix bit2bool bug reported by Jianying Li
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-04 07:46:53 -08:00
Nikolaj Bjorner b0fe7d9a21
Merge pull request #2056 from msoeken/nuget-release
Make Ubuntu package more generic
2019-01-02 11:02:08 +08:00
Mathias Soeken 878f297dac Make Ubuntu package more generic. 2019-01-01 17:20:33 +01:00
Nikolaj Bjorner b533ba39d6 use private rewriter to avoid surprises
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-29 17:13:32 +08:00
Nikolaj Bjorner 815faa96d9 remove dotnet35 support
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-29 16:44:03 +08:00
Nikolaj Bjorner f8a3300026 introduce proxies to differentiate from arithmetical variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-29 11:13:15 +08:00
Nikolaj Bjorner da82826a87
Merge pull request #2052 from Chen-Huanyi/master
Substitute "Vars" in queries and  Make sure init is included when generalize
2018-12-29 11:08:03 +08:00
Huanyi Chen 4b29b208ad Add few more testcases 2018-12-28 13:28:15 -05:00
Huanyi Chen 300e99b67a Make sure init is included when generalize 2018-12-28 13:21:40 -05:00
Huanyi Chen b083c7546e Substitue Vars in queries
Replace Vars that are representing primary inputs as "i#" when query
solvers.
2018-12-28 13:21:35 -05:00
Nikolaj Bjorner e40884725b remove unused euf-mbi
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-28 19:47:48 +08:00
Nikolaj Bjorner 64103038a7 simplify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-28 12:20:53 +08:00
Nikolaj Bjorner 0628711c4a simplify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-28 12:18:29 +08:00
Nikolaj Bjorner 6a2d54b31e cleanup and doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-28 11:59:17 +08:00
Nikolaj Bjorner da95fd7d83 fixing get-arith-vars and extraction of private variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-28 11:23:52 +08:00
Nikolaj Bjorner 2cc3918027 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-28 09:38:31 +08:00
Nikolaj Bjorner 8829fa96de change projection function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-28 09:38:17 +08:00
Nikolaj Bjorner d879e2732a
Merge pull request #2050 from waywardmonkeys/allow-disabling-invoking-debugger
If NO_Z3_DEBUGGER, also drop defining invoke_gdb.
2018-12-27 17:23:31 -08:00
Bruce Mitchener 877df0f1cc If NO_Z3_DEBUGGER, also drop defining invoke_gdb. 2018-12-27 09:21:45 -05:00
Nikolaj Bjorner 8b3abe120c Merge branch 'master' of https://github.com/z3prover/z3 2018-12-26 21:04:44 +08:00
Nikolaj Bjorner 076cfa5813 working on revising project0 to project
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-26 21:04:35 +08:00
Nikolaj Bjorner 04fb8a45eb
Merge pull request #2049 from waywardmonkeys/fix-typos
Fix typos.
2018-12-24 16:31:58 -08:00
Bruce Mitchener 44bc00f13d Fix typos. 2018-12-23 21:58:57 -05:00
Nikolaj Bjorner 9379ec3a68 add back pre_visit, which does get called from rewriter_def/rewriter.h
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-21 18:52:09 -08:00
Nikolaj Bjorner 99cc4747c5 fixing #1971
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-21 17:21:04 -08:00
Nikolaj Bjorner 95db37d105 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-21 17:10:41 -08:00
Nikolaj Bjorner b0b6394c6c fixing #1971
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-21 17:10:37 -08:00
Nuno Lopes 3104291b80 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 23:02:15 +00:00
Nuno Lopes 178e5b31e8 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 22:49:06 +00:00
Nuno Lopes 52f960a7c8 elim_uncnstr_tactic: remove m_imp idiom to reduce mem alloc 2018-12-21 19:48:18 +00:00
Nikolaj Bjorner e1dc553228 inc version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-20 13:15:50 -08:00
Nikolaj Bjorner d6df51951f release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-20 10:32:36 -08:00
Nikolaj Bjorner a63d1b1848 update doctest
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-18 11:57:20 -08:00
Nikolaj Bjorner 35e8decdb1 for #2039
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-18 11:27:04 -08:00
Nikolaj Bjorner b6bf299b8b update upolynmial test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-17 17:41:50 -08:00
Nikolaj Bjorner 360d6f963e reduce output
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-17 17:05:48 -08:00
Nikolaj Bjorner bd96eaff47 axiomatize pb-eq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-17 08:26:59 -08:00
Nikolaj Bjorner f4d03edf22 remove unreachable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-16 15:54:30 -08:00
Nikolaj Bjorner 2dcf36e96c fix #2044
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-16 15:32:38 -08:00
Nikolaj Bjorner 82a89120b0 fix #2042
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-16 15:26:40 -08:00
Nikolaj Bjorner f56749a241 fix #2041, fix #2043
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-16 15:18:49 -08:00