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

10297 commits

Author SHA1 Message Date
Huanyi Chen 83e3a79bd1 Remove testcase that takes long time to finish 2019-01-04 17:31:47 -05: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
Nikolaj Bjorner 58b9fc437d add sin/cos axiom regardless of whether sin/cos can be eliminated. fix #2037
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-13 16:09:08 -06:00
Nikolaj Bjorner c5ada288c2 updated script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-12 12:46:28 -08:00
Nikolaj Bjorner 8d23ad2f7e fix generation of assembly-sign-input to take escape sequences and absolute paths
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-12 10:14:38 -08:00
Nikolaj Bjorner db3e5ce070
Merge pull request #1997 from waywardmonkeys/change-64-bit-configuration-strategy
Change how 64 bit builds are detected.
2018-12-12 09:55:13 -08:00
Nikolaj Bjorner 83f64ad604 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 20:27:37 -08:00
Nikolaj Bjorner b3d0ed6143 fix #2035 regression. correct axiom is |extract(s,i,l)| <= l or l < 0, but it is subsumed by encoding of extract, so new axiom is not useful
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 20:27:28 -08:00
Nikolaj Bjorner 02f01fcef1 adding esrp feature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 17:31:09 -08:00
Nikolaj Bjorner 93c59ffbd9 update script to sign assembly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 15:48:33 -08:00
Nikolaj Bjorner c1b03e8ca6 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:38:44 -08:00
Nikolaj Bjorner bfcea7a819 perf improvements by reordering variable branching #1676
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:38:36 -08:00
Nikolaj Bjorner 271e86020a Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:35:34 -08:00
Nikolaj Bjorner 045fef35ed fix build break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:35:27 -08:00
Nikolaj Bjorner 021c5315a7
Merge pull request #2034 from Bronsa/patch-1
Change error message from "internal failure" to "Object allocation failed"
2018-12-11 09:32:32 -08:00
Nikolaj Bjorner a3f9e3168d simplify ~context #1948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:29:59 -08:00
Nikolaj Bjorner 796689f708 #1948 remove memory allocation in nlsat::solver::~solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-12-11 09:08:53 -08:00