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

8207 commits

Author SHA1 Message Date
Nikolaj Bjorner
6277ed61c9 pull rounding mode top-level to deal with build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-13 02:09:35 -07:00
Nikolaj Bjorner
973c9602f8 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-12 22:44:33 -07:00
Nikolaj Bjorner
5356c4f7dd remove class from enum class, add default to avoid compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-12 22:44:23 -07:00
Bruce Mitchener
58682c20be dl_util: Use an unsigned to match other values. 2018-10-13 07:58:27 +07:00
Nikolaj Bjorner
efb12331e0
Merge pull request #1873 from xlauko/master 
Add a floating-point support to c++ api.
 2018-10-12 10:52:55 -07:00
Bruce Mitchener
5bd93b8a77 Typo fixes. 2018-10-12 23:38:53 +07:00
Nikolaj Bjorner
a58bc72dfb Merge branch 'master' of https://github.com/z3prover/z3 2018-10-11 22:05:15 -07:00
Nikolaj Bjorner
f5fea8ae30 add parameter to force sat-cleaning on initialization and on simplification phases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-11 22:05:04 -07:00
xlauko
3b86ea3f8a Add a floating-point support to c++ api. 2018-10-11 16:30:59 +02:00
Nikolaj Bjorner
2f9853f1b5
Merge pull request #1865 from ahelwer/master 
Files and changes for Z3 NuGet package
 2018-10-06 21:46:52 -07:00
Andrew Helwer
7941074fd1 Added packaging directions, removed linkresource flag 2018-10-06 18:22:55 -07:00
Nikolaj Bjorner
f14a2b9a7c fix java 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 16:13:23 -07:00
Nikolaj Bjorner
aad09816cb build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 15:16:23 -07:00
Nikolaj Bjorner
c4829dfa22 fix #1577 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 09:01:01 -07:00
Nikolaj Bjorner
44a0dbbc61 fix #1864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-06 08:06:51 -07:00
Lev
99339798ee fix the value oflar_solver.m_status during pop() 
Signed-off-by: Lev <levnach@hotmail.com>
 2018-10-04 19:43:01 -07:00
Nikolaj Bjorner
2097983db3 fix java bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 14:05:38 -07:00
Nikolaj Bjorner
b540868cd7 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-04 13:43:04 -07:00
Nikolaj Bjorner
a549e73b86 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-04 13:43:01 -07:00
Nikolaj Bjorner
f8e5d989bf fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:49:57 -07:00
Nikolaj Bjorner
3bc2213d54 fix #1577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 17:43:42 -07:00
Nikolaj Bjorner
46cdefac4d fix memory leak when cuber isn't run to completion. Found by Daniel Selsam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 10:57:02 -07:00
Nikolaj Bjorner
fd9fd52271 fixing #1847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-02 17:13:46 -07:00
Nikolaj Bjorner
8b981e545d
Merge pull request #1855 from mtrberzi/refactoring-arith 
Z3str3: refactoring, arith_value
 2018-10-02 14:10:36 -07:00
Nikolaj Bjorner
69f35a2970
Merge branch 'master' into intel-compiler 2018-10-02 11:54:52 -07:00
Murphy Berzish
b2f0051114 Merge remote-tracking branch 'upstream/master' into refactoring-arith 2018-10-02 12:38:40 -04:00
Murphy Berzish
39fbf1e174 Z3str3: don't use arith_value::get_value in get_arith_value 2018-10-02 12:28:53 -04:00
Nikolaj Bjorner
55cc89b6bb
Merge pull request #1862 from kbobyrev/arith_eq_solver-cleanup 
[NFC] Cleanup arith_eq_solver.(cpp|h)
 2018-10-02 08:48:49 -07:00
Nikolaj Bjorner
cc312d2f68
Merge pull request #1861 from waywardmonkeys/macos-naming 
Refer to macOS rather than Mac OS / OSX.
 2018-10-02 08:28:02 -07:00
Nikolaj Bjorner
5bf57c2700 fix cubing semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-02 08:14:19 -07:00
Kirill Bobyrev
a376a8d343 [NFC] Cleanup arith_eq_solver.(cpp|h) 
Use for-range loops instead of for-index loops where possible, remove
trailing whitespaces.

This patch does not affect functionality.
 2018-10-02 16:14:01 +03:00
Bruce Mitchener
a76397d3b8 Refer to macOS rather than Mac OS / OSX. 2018-10-02 17:38:09 +07:00
Nikolaj Bjorner
620c5d1d81
Merge pull request #1850 from Nils-Becker/master 
adding call to update_max_generation
 2018-10-01 21:49:14 -07:00
Nikolaj Bjorner
2cf6ada38e
Merge pull request #1856 from waywardmonkeys/minor-fixes 
Minor fixes
 2018-10-01 20:46:27 -07:00
Nikolaj Bjorner
c84182b42a
Merge pull request #1859 from waywardmonkeys/for-range-copy 
Avoid unnecessary copies in for-range loops.
 2018-10-01 20:44:52 -07:00
Nikolaj Bjorner
7082d85115
Merge pull request #1860 from waywardmonkeys/modernize-use-override 
Use 'override' where possible.
 2018-10-01 20:43:56 -07:00
Bruce Mitchener
6d2936e5fc watch_list: Fix indentation. 2018-10-02 10:43:00 +07:00
Bruce Mitchener
1067a5363f theory_lra: Remove unused variable. 2018-10-02 10:42:54 +07:00
Bruce Mitchener
7bc283b84e Avoid unnecessary copies in for-range loops. 2018-10-02 10:38:41 +07:00
Bruce Mitchener
373b691709 Use 'override' where possible. 2018-10-02 10:26:38 +07:00
Nikolaj Bjorner
5eb24d3118 Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 20:22:10 -07:00
Nikolaj Bjorner
9d0aa4d02d update empty cube case for sat/undef cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 20:22:02 -07:00
Nikolaj Bjorner
3c7e7a7ffd
Merge pull request #1852 from janisozaur/unused-const 
Drop unused CV-qualifiers from scalar return values
 2018-10-01 20:10:21 -07:00
Nikolaj Bjorner
4bc6720af7
Merge pull request #1853 from janisozaur/solve-ax-eq-b 
Add missing template instantion for lar_core_solver::m_r_solver
 2018-10-01 20:09:50 -07:00
Nikolaj Bjorner
be8a9c611e incorporate #1854 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 19:49:18 -07:00
Nikolaj Bjorner
096a6c088d Merge branch 'master' of https://github.com/z3prover/z3 2018-10-01 19:32:52 -07:00
Nikolaj Bjorner
bb979a194e remove unused return value of mk_enode following #1856 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 19:32:44 -07:00
Nikolaj Bjorner
b0dac346dc
Merge pull request #1857 from waywardmonkeys/modernize-use-nullptr 
Use nullptr.
 2018-10-01 19:28:58 -07:00
Bruce Mitchener
489582f7fa Remove unused sat_par files. 
These look like they were replaced by `sat_parallel` files and
aren't currently built or used.
 2018-10-02 09:19:14 +07:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00