Josh Berdine
4401abbb4a
Return bool instead of int from Z3_rcf_interval ( #8046 )
...
In the underlying realclosure implementation, the interval operations for
{`lower`,`upper`}`_is_`{`inf`,`open`} return `bool` results. Currently these
are cast to `int` when surfacing them to the API. This patch keeps them at
type `bool` through to `Z3_rcf_interval`.
Signed-off-by: Josh Berdine <josh@berdine.net>
2025-11-25 18:08:17 -08:00
Nuno Lopes
bd8c870bbe
api: avoid some string copies when using mk_external_string
2024-12-28 09:42:54 +00:00
Christoph M. Wintersteiger
16753e43f1
Add accessors for RCF numeral internals ( #7013 )
2023-11-23 17:54:23 +01:00
Nuno Lopes
73a24ca0a9
remove '#include <iostream>' from headers and from unneeded places
...
It's harmful to have iostream everywhere as it injects functions in the compiled files
2022-06-17 14:10:19 +01:00
Nikolaj Bjorner
4a6083836a
call it data instead of c_ptr for approaching C++11 std::vector convention.
2021-04-13 18:17:35 -07:00
Bruce Mitchener
0231bc44bc
Simplify boolean code.
...
Now that the C API is using bool, this can be simplified.
2018-12-07 22:06:51 +07:00
Bruce Mitchener
edf8ba44d1
Switch from using Z3_bool to using bool.
...
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
2018-11-20 11:27:09 +07:00
Bruce Mitchener
56bbed173e
Remove usages of Z3_TRUE / Z3_FALSE.
...
Now that this is all using stdbool.h, we can just use true/false.
For now, we leave the aliases in place in z3_api.h.
2018-11-20 00:25:37 +07:00
Nikolaj Bjorner
1eb8ccad59
overhaul of error messages. Add warning in dimacs conversion
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-07-04 16:04:37 -07:00
Bruce Mitchener
76eb7b9ede
Use nullptr.
2018-02-12 14:05:55 +07:00
Dan Liew
a2d7b43554
Update header includes to be relative to src/ directory.
2017-08-17 18:26:53 +01: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
baee4225a7
reworking cancellation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:21:24 -08:00
Leonardo de Moura
77f58269ed
Add html pretty printing mode for RCF package
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-27 10:19:54 -08:00
Leonardo de Moura
c9b7ea35b6
Fix typo
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-16 08:39:24 -08:00
Leonardo de Moura
799fe073db
Add API for extracting numerator/denominator of RCF numerals. Add field to store the original isolating interval before refinement.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 18:29:08 -08:00
Leonardo de Moura
742f2b07dd
Add support for compact string representation in the RCF API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-14 11:08:32 -08:00
Leonardo de Moura
7312f49f88
Fix Visual Studio warnings
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-13 09:06:07 -08:00
Leonardo de Moura
4cd2998743
Add power operator to C and Python RCF APIs
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-10 13:05:47 -08:00
Leonardo de Moura
56db84a0e5
Fix RCF API logging bug
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-07 15:10:16 -08:00
Leonardo de Moura
09b5724d82
Simplify RCF C API. Add Z3_rcf_mk_roots (C API) and MkRoots (Python API). Implement basic root isolation support.
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-07 12:25:28 -08:00
Leonardo de Moura
3e19df0441
Fix API logging bug
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-06 21:25:46 -08:00
Leonardo de Moura
9fbbdb56e4
Implement RCF external C API
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-06 20:06:27 -08:00
Leonardo de Moura
47c6a73e19
Add RCF external API skeletons
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-01-05 22:24:56 -08:00
