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

12992 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 41965acaf1 less is even more correct, fix #3244 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 15:17:01 -07:00
Nikolaj Bjorner 0f5cc2ec70 add missing API call for solverInterrupt to Java. Fix #3382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 14:52:59 -07:00
Nikolaj Bjorner b3e1e302f7 fix #3320 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 13:22:17 -07:00
Nikolaj Bjorner daadc1dd8c fix #3391 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 13:04:30 -07:00
Nikolaj Bjorner 19cdf08818 fix #3396 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 12:45:37 -07:00
Nikolaj Bjorner 7cb6f41d0a fix #3390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 11:15:15 -07:00
Nikolaj Bjorner 24dd047892 fix #3397, use it or lose it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 11:06:19 -07:00
Nikolaj Bjorner fbf5fc9482 fix #3385 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 10:50:26 -07:00
Nikolaj Bjorner 31164c2eaf fix #3386 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 10:40:34 -07:00
Nikolaj Bjorner b590751e92 fix #3389 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 10:36:34 -07:00
Nikolaj Bjorner a45532da73 fix #3392 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 09:47:23 -07:00
Nikolaj Bjorner 752b498254 fix #3384 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-17 18:02:30 -07:00
Nikolaj Bjorner 55ebb236db add self-contained check for triangle inequality for #2867 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-17 15:39:30 -07:00
Lev Nachmanson dae3cd450b fix a bug in nex_creator, already fixed in debug branch 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-17 14:46:46 -07:00
Nikolaj Bjorner fd54408629 fix leaks exposed by #3383 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-17 13:01:46 -07:00
Nikolaj Bjorner 719c5dd911 fix #3342 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-17 12:14:28 -07:00
Nikolaj Bjorner 89ff533dcd port fix #3376 from Debug branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-17 11:08:30 -07:00
Nikolaj Bjorner 7996472923 fix ? #3370 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-17 10:38:26 -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 1c5283f3a4 remove mk_pp to fix build on some platforms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 20:36:41 -07:00
Arie Gurfinkel 6180a5276d
Logging facility for spacer plus minor improvements (#3368) 
* [spacer] logging solver events

New option fp.spacer.trace_file='file.log' enables logging solving events
into a file.

These events are useful for debugging the solver, but also for visualizing
the solving process in a variety of ways

* [spacer] allow setting logic for solvers used by spacer

* [spacer] option to set arithmetic solver explicitly

* [spacer] improve of dumping solver_pool state for debugging

* fix propagate_ineqs to handle strict inequality

Co-authored-by: Nham Van Le <nv3le@precious3.eng.uwaterloo.ca>
 2020-03-16 20:31:44 -07:00
Nikolaj Bjorner f06deca7e0 fix #3347 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 20:21:04 -07:00
Nikolaj Bjorner d002423133 fix ? #3342 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 20:09:28 -07:00
Nikolaj Bjorner 019acdb1ef fix #3350 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 19:56:18 -07:00
Nikolaj Bjorner f86205b0e8 fix #3343 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 12:24:22 -07:00
Nikolaj Bjorner e7ec842cf5 fix #3348 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 12:14:19 -07:00
Nikolaj Bjorner 3209d4ff6c fix #3351 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 12:05:35 -07:00
Nikolaj Bjorner bb1fe358c1 fix #3356 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 11:54:01 -07:00
Nikolaj Bjorner 9c9ce0b920 fix #3363, already fixed in Debug branch, importing fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 11:45:11 -07:00
Nikolaj Bjorner ed70d246d3 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 11:39:09 -07:00
Nikolaj Bjorner 1bddfd40c3 fix #3364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-16 11:38:25 -07:00
Nikolaj Bjorner a5c60ec517 Update arith_decl_plugin.cpp 
use integer sorts
 2020-03-15 14:30:02 -07:00
Nikolaj Bjorner 6ad261e24c fix #3330 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-15 09:49:44 -07:00
Nikolaj Bjorner 4d30e9b411 fix #3332 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-15 09:16:44 -07:00
Nikolaj Bjorner 6c67654e64 fix #3335 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-15 09:12:43 -07:00
Nikolaj Bjorner f323da8f37 fix #3304 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 22:41:13 -07:00
Nikolaj Bjorner 894702d600 fix #3301 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 14:42:24 -07:00
Nikolaj Bjorner 42dbee9165 fix #3302 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 14:39:03 -07:00
Nikolaj Bjorner ec0349819f fix #3298 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 12:15:05 -07:00
Nikolaj Bjorner 47bd06338e fix #3283 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:54:24 -07:00
Nikolaj Bjorner 6b319f9ac3 fix #3297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:49:05 -07:00
Nikolaj Bjorner 974541e244 fix #3299 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:44:25 -07:00
Nikolaj Bjorner c613ab0ba0 fix #3286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:42:26 -07:00
Nikolaj Bjorner 9f6a0a0a48 fix #3289, recent regression introduced when dealing with push on inconsistent state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 10:50:41 -07:00
Nikolaj Bjorner 51e459d02b fix #3294 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 10:46:03 -07:00
Nikolaj Bjorner b29c77dc87 fix #3295 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 09:51:18 -07:00
Nikolaj Bjorner 6f2b5696d5 fix #3279 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 17:08:20 -07:00
Nikolaj Bjorner 31c3ac016a fix #3275 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 13:55:12 -07:00
Nikolaj Bjorner 59755dd72e fix #3260 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 11:42:25 -07:00
Nikolaj Bjorner d530d1314b fix #3276 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 11:20:12 -07:00