Nikolaj Bjorner
|
3113901c8f
|
rename is_atom
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-21 23:15:57 -07:00 |
|
Nikolaj Bjorner
|
f349d3d013
|
fix extraction of non-units
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-21 21:15:28 -07:00 |
|
Nikolaj Bjorner
|
984e74428a
|
fix include path for z3_version.h
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-21 20:41:26 -07:00 |
|
Nikolaj Bjorner
|
8e0eebf507
|
fix include path for z3_version.h
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-21 20:37:13 -07:00 |
|
Nikolaj Bjorner
|
e391416855
|
fix include path for z3_version.h
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-21 20:30:50 -07:00 |
|
Nikolaj Bjorner
|
0c4754d94b
|
rename version.h to z3_version.h to differentiate name in install include directory. Add support for z3_version.h in python build system. #1833
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-21 20:13:58 -07:00 |
|
Nikolaj Bjorner
|
38c6429184
|
Merge pull request #1838 from NikolajBjorner/master
remove offsets from terms to fix cut generation
|
2018-09-21 17:03:42 -07:00 |
|
Nuno Lopes
|
0b7918c52e
|
remove spurious pragma
|
2018-09-21 09:37:36 +01:00 |
|
Nikolaj Bjorner
|
618e1bee5b
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-20 20:41:00 -07:00 |
|
Nikolaj Bjorner
|
c59a957737
|
add non-units method
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-20 20:37:14 -07:00 |
|
Nikolaj Bjorner
|
4e75efa485
|
Merge pull request #1839 from dselsam/master
extend(src/api/c++/z3++.h): support units() for solver class
|
2018-09-20 20:04:17 -07:00 |
|
Nikolaj Bjorner
|
39ed27101e
|
include version.h in install include directory for cmake build #1833
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-20 19:56:55 -07:00 |
|
Daniel Selsam
|
d6a1d17d69
|
extend(src/api/c++/z3++.h): support units() for solver class
|
2018-09-20 19:47:32 -07:00 |
|
Nikolaj Bjorner
|
382bce4bb7
|
fix #1836
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-20 19:19:40 -07:00 |
|
Nikolaj Bjorner
|
91dbcbc36f
|
fix test build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-20 18:57:47 -07:00 |
|
Nikolaj Bjorner
|
d75b6fd9c1
|
remove offsets from terms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-20 11:06:05 -07:00 |
|
Nikolaj Bjorner
|
dcda39e76e
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-19 17:12:32 -07:00 |
|
Nikolaj Bjorner
|
c8e8b4796f
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-19 14:33:32 -07:00 |
|
Nikolaj Bjorner
|
3c553c17e8
|
fix dump utility for cuts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-19 14:32:56 -07:00 |
|
Lev Nachmanson
|
8b95a4ba63
|
Merge pull request #1837 from levnach/gomory
keep the coefficients of 'at lower' variables positive, and the rest …
|
2018-09-19 13:27:22 -07:00 |
|
Lev Nachmanson
|
a99ebed907
|
keep the coefficients of 'at lower' variables positive, and the rest negative for Gomory cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2018-09-19 10:17:27 -07:00 |
|
Nikolaj Bjorner
|
ed19af4c4e
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-19 09:02:37 -07:00 |
|
Lev Nachmanson
|
ac878698b9
|
Merge pull request #1834 from levnach/gomory
Gomory
|
2018-09-18 19:56:03 -07:00 |
|
Lev Nachmanson
|
b90d571d9a
|
fixing the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2018-09-18 15:36:01 -07:00 |
|
Lev
|
041458f97a
|
fixes the +- bug in gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-18 14:42:32 -07:00 |
|
Lev
|
b940b7873b
|
work on Gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-18 13:47:18 -07:00 |
|
Lev
|
ca3ce964ce
|
work on Gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-18 13:34:05 -07:00 |
|
Murphy Berzish
|
144b72244e
|
clean up pragmas, Z3str3 refactoring
|
2018-09-18 16:11:47 -04:00 |
|
Murphy Berzish
|
7e419137b1
|
Z3str3: refactor regex automata to subroutine, use arith_value
|
2018-09-17 16:13:34 -04:00 |
|
Nikolaj Bjorner
|
5bbe0508e4
|
Merge branch 'master' of https://github.com/z3prover/z3
|
2018-09-16 13:43:55 -07:00 |
|
Nikolaj Bjorner
|
1a3fe1edd3
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-16 13:43:38 -07:00 |
|
Nikolaj Bjorner
|
286126dde9
|
fix #1828, add self-contained utility to extract arithmetical values for use in theory_seq and theory_str and other theories that access current values assigned to numeric variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-16 13:31:37 -07:00 |
|
Nikolaj Bjorner
|
2b35f1a924
|
quip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-16 13:14:41 -07:00 |
|
Nikolaj Bjorner
|
3e7ed52b71
|
Merge pull request #1829 from levnach/gomory
Gomory
|
2018-09-15 23:21:43 -07:00 |
|
Nikolaj Bjorner
|
98dfd82765
|
adding quipie
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-15 21:55:49 -07:00 |
|
Lev
|
106b677201
|
fixes in gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-15 17:47:54 -07:00 |
|
Lev
|
34bdea750c
|
fixes in gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-15 17:46:16 -07:00 |
|
Lev
|
8c122ba9bd
|
fixes in gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-15 17:33:35 -07:00 |
|
Lev
|
03d55426bb
|
fixes in gomory cut
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-15 17:15:46 -07:00 |
|
Nikolaj Bjorner
|
0232383191
|
mini IC3 sample
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-15 16:59:06 -07:00 |
|
Lev
|
324396e403
|
separate the gomory cut functionality in a separate file
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-14 17:12:49 -07:00 |
|
Lev
|
26764b076f
|
adjust cuts and branch (m_t and m_k) for terms
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-14 12:39:46 -07:00 |
|
Lev
|
257ba6218f
|
remove gomory.h
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-14 11:54:10 -07:00 |
|
Lev
|
22213a9e73
|
rebase
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-14 11:53:54 -07:00 |
|
Lev Nachmanson
|
57357b7ece
|
does not compile
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2018-09-14 11:52:44 -07:00 |
|
Lev
|
5dee39721a
|
rebase
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-14 11:52:14 -07:00 |
|
Lev
|
e705e5a309
|
branch on inf basic in gomory
Signed-off-by: Lev <levnach@hotmail.com>
|
2018-09-14 11:49:39 -07:00 |
|
Nikolaj Bjorner
|
78950fde17
|
initialize solver before parse is invoked. Fixes issue reported by Selsam
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-09-13 19:05:45 -07:00 |
|
Nikolaj Bjorner
|
19d3b5cfd1
|
Merge pull request #1826 from dselsam/master
remove duplicate method definitions
|
2018-09-13 18:38:17 -07:00 |
|
Daniel Selsam
|
2a8d207bf4
|
remove duplicate method definitions
|
2018-09-13 14:31:52 -07:00 |
|