3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-02 11:46:55 +00:00
Commit graph

18 commits

Author SHA1 Message Date
Lev Nachmanson
fe6b777638 improve logging
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2025-11-24 06:41:06 -10:00
Nikolaj Bjorner
17545233e6 encapsulate anum functionality 2024-01-20 12:59:58 -08:00
Bruce Mitchener
50e0fd3ba6
Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
Nikolaj Bjorner
d0e20e44ff booyah
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
a4f668eef0 add unit test for #2867
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-03-24 11:52:41 -07:00
ahumenberger
de9bc930e9
Extract defining components of algebraic number via C and C++ API (#3321)
* First steps toward adding Julia bindings

* Simplifications

* Streamlining

* Friends of tactic and probe

* Add missing functions

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Changes for CxxWrap v0.9.0

* Wrap enumeration and tuple sort

* Wrap z3::fixedpoint

* Wrap z3::optimize

* Wrap missing functions

* Fix aux types

* Add some missing functions

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 5aab9f9240.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit cfccd7ca2c.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit f24740c595.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 592499eaa0.

* Checkout current version of pipeline

* Build Julia bindings on macOS

* Extract components of algebraic number

* Add type to C API function name

* Remove blank line

* Typo in doc

* Return Z3_ast_vector containing coefficients
2020-03-17 09:09:02 -07:00
Nikolaj Bjorner
d3b105f9f8 move out sign
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-20 16:22:38 -06:00
Nikolaj Bjorner
39edf73e78 fix #2613 fix #2612
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-10-05 16:57:51 -07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +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
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
4bc044c982 update header guards to be C++ style. Fixes issue #9
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Leonardo de Moura
607fab486c Fix incorrect uses of set_cancel()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-17 18:48:10 -08:00
Leonardo de Moura
0d230375be added polynomial evaluation at algebraic point
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-08 20:39:16 -08:00
Leonardo de Moura
1871bef6e1 cleaned algebraic params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 12:47:20 -08:00
Leonardo de Moura
cf28cbab0a saved params work
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-11-29 17:19:12 -08:00
Leonardo de Moura
9e299b88c4 reorganizing the code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-10-23 21:53:34 -07:00
Renamed from src/polynomial/algebraic_numbers.h (Browse further)