Nikolaj Bjorner
|
66b38eac9f
|
add back dotnet after adding ;*.cs to path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-07 20:07:55 -07:00 |
|
Nikolaj Bjorner
|
02e71c7d23
|
fix #2650, use datatype constructor producing smallest possible tree whenever possible
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-07 16:23:44 -07:00 |
|
Nikolaj Bjorner
|
82c39f81a3
|
fix str.at rewrite
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-06 20:43:48 -07:00 |
|
Nikolaj Bjorner
|
9a516e5e41
|
fix str.at rewrite
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-06 20:43:02 -07:00 |
|
Nikolaj Bjorner
|
39edf73e78
|
fix #2613 fix #2612
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-05 16:57:51 -07:00 |
|
Nikolaj Bjorner
|
016732aa59
|
move some tracing to verbose
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-03 17:21:47 -07:00 |
|
Nikolaj Bjorner
|
88f0e4a64c
|
fix #2592 #2593 #2597 #2573 - duplicates, also fix #2603
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-10-01 13:14:12 -07:00 |
|
Nikolaj Bjorner
|
74aa47f458
|
fix #2578
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-23 13:52:27 -07:00 |
|
Nikolaj Bjorner
|
0b06a9b5d8
|
fix minor version numbering
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-23 01:57:03 -07:00 |
|
Nikolaj Bjorner
|
04ae00048d
|
fix #2567
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-17 18:48:21 -04:00 |
|
Nikolaj Bjorner
|
67c4777514
|
fix #2548 fix #2530
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-13 15:03:04 +02:00 |
|
Nikolaj Bjorner
|
bc723fbe89
|
fix #2539
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-06 15:07:43 +03:00 |
|
Nikolaj Bjorner
|
29f0897afc
|
tweaking nlqsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-09-06 09:42:57 +03:00 |
|
Nikolaj Bjorner
|
2e6908bd9e
|
fix #2509, fix issue with model inheritance exposed by #2483
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-27 10:48:22 -03:00 |
|
Bruce Mitchener
|
ce7f9c3f3d
|
Remove unused variable.
|
2019-08-04 18:37:05 -07:00 |
|
Nikolaj Bjorner
|
4431a534b3
|
fix #2450 - track assumptions across lazy explanations and variable equalities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-03 07:57:16 -07:00 |
|
Nikolaj Bjorner
|
db5af3088b
|
logging for #2450
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 16:47:18 -07:00 |
|
Nikolaj Bjorner
|
1d488d07fa
|
nlsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-02 15:06:34 -07:00 |
|
Nikolaj Bjorner
|
7f073a0585
|
fix #2452 fix #2451
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-08-01 16:28:15 +08:00 |
|
Nikolaj Bjorner
|
26c1c744aa
|
fix #2396
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 17:36:30 -04:00 |
|
Nikolaj Bjorner
|
0bca2aabff
|
remove invocation of debugger
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-07-12 17:07:44 -04:00 |
|
Nikolaj Bjorner
|
6071797ba9
|
fix again
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-08 12:11:43 +02:00 |
|
Nikolaj Bjorner
|
f79dccccfe
|
fix #2238
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-05-08 10:15:57 +02:00 |
|
Nikolaj Bjorner
|
28773c8d5c
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-04-27 13:49:44 -07:00 |
|
Nikolaj Bjorner
|
944ce1135b
|
replace __debug__ by Z3_DEBUG #2225
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2019-04-27 13:47:53 -07: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
|
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 |
|
Nikolaj Bjorner
|
8040eddf65
|
fix #1658 fix #1689
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-06-18 16:41:04 -07:00 |
|
Bruce Mitchener
|
76eb7b9ede
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
Bruce Mitchener
|
b7d1753843
|
Use override rather than virtual.
|
2018-02-09 21:19:27 +07:00 |
|
Bruce Mitchener
|
73b3da37d8
|
Typo fixes.
|
2018-01-02 22:48:06 +07:00 |
|
Nikolaj Bjorner
|
8dadd30db5
|
add __copy__, __deepcopy__ as alias to translate on same context #1427. Add generalized Gaussian elimination as an option to first-pass NL solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2018-01-01 17:11:43 -08:00 |
|
Nikolaj Bjorner
|
79a9dfd8fd
|
adding pre-processing to nlsat for equations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-30 20:35:33 -08:00 |
|
Nikolaj Bjorner
|
c3add4eeda
|
add back missing initialization of lo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-15 06:56:36 -08:00 |
|
Nikolaj Bjorner
|
21f685fa5a
|
fix nlsat regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-15 06:54:02 -08:00 |
|
Nikolaj Bjorner
|
397cdfc608
|
avoid crash on nl
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-15 06:38:56 -08:00 |
|
Nikolaj Bjorner
|
1c3d385c25
|
fix crashes in nlsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-14 17:24:13 -08:00 |
|
Nikolaj Bjorner
|
ab39f06df7
|
fix crashes in nlsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-14 17:22:49 -08:00 |
|
Nikolaj Bjorner
|
e5fa35e969
|
add integer branch and bound to nlsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-12-14 17:07:17 -08:00 |
|
Nikolaj Bjorner
|
2b82fd5d0c
|
updated include directives
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-08-01 10:51:47 -07:00 |
|
Nikolaj Bjorner
|
b19f94ae5b
|
make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-07-31 13:24:11 -07:00 |
|
Nikolaj Bjorner
|
305e080239
|
enable unsat core extraction in nlsat_tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-11-01 17:57:28 +01:00 |
|
Nikolaj Bjorner
|
96e157e201
|
fix warnings for unused variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-17 13:54:22 -07:00 |
|
Nikolaj Bjorner
|
680c28d083
|
remove nnf conversion which breaks NRA property
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-20 16:34:04 -07:00 |
|
Nikolaj Bjorner
|
20bbdfe31a
|
moving remaining qsat functionality over
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-03-19 15:35:26 -07:00 |
|
Nikolaj Bjorner
|
54ac71cada
|
ensure limit children are safe for race conditions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-12 10:23:56 -08:00 |
|
Nikolaj Bjorner
|
baee4225a7
|
reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-11 16:21:24 -08:00 |
|
Nikolaj Bjorner
|
981f8226fe
|
moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-12-11 13:36:47 -08:00 |
|
Nikolaj Bjorner
|
d9b6623400
|
include rlimit in nlsat, include dedicated error message, for issue #216
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2015-09-29 09:16:46 -07:00 |
|
Leonardo de Moura
|
70baa3c8c9
|
Add nlsat.factor option. This is a workaround for the slow factorization procedure.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2013-01-02 21:18:02 -08:00 |
|