mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity
5351 commits 23 branches 48 tags 157 MiB
Commit graph

5351 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 7534b53bae Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-06 14:51:25 +01:00
Christoph M. Wintersteiger ee7b09b3b6 Merge pull request #3 from martin-neuhaeusser/ml_api_patch3 
Improvements of the OCaml API implementation
 2016-04-06 14:47:36 +01:00
Christoph M. Wintersteiger 86ca224460 Merge pull request #554 from MikolasJanota/trailing 
Trailing
 2016-04-06 14:25:58 +01:00
martin-neuhaeusser 95454679e2 Another round of pretty printing 2016-04-06 12:45:21 +02:00
martin-neuhaeusser bd9d13279a Pretty printing 2016-04-06 12:39:19 +02:00
martin-neuhaeusser 1662ba8353 Add more comments on comparison functions in the C layer of the OCaml bindings 2016-04-06 12:36:11 +02:00
martin-neuhaeusser b873c6b508 Simplify OCaml API 
This patch simplifies the implementation of the OCaml bindings. For example,
the applyX wrapper functions have become unnecessary in the new OCaml API.
It also removes the internal ML2C structure that was used as an intermediate
layer between the C and the OCaml layer.
 2016-04-06 12:10:59 +02:00
Mikolas Janota 7ad9dec6c2 Adding cpp files for bv_trailing to CMakeLists. 2016-04-06 11:04:17 +01:00
Mikolas Janota dbffc15b98 Improvements in caching of bv_trailing. 2016-04-06 11:04:15 +01:00
mikolas 9ba5bbfd33 Re-factoring and comments in bv_trailing. 2016-04-06 11:04:13 +01:00
Mikolas Janota 248feace34 fixing the behavior in bv_trailing 2016-04-06 11:04:11 +01:00
mikolas fced47386e More work on trailing 0 analysis. 2016-04-06 11:04:09 +01:00
mikolas ddb6ae4eab More work on trailing 0 analysis. 2016-04-06 11:04:07 +01:00
mikolas 78cb1e3c7b More work on trailing 0 analysis. 2016-04-06 11:04:05 +01:00
mikolas c7f1746321 Starting to work on trailing 0 analysis. 2016-04-06 11:04:03 +01:00
Nikolaj Bjorner 493b86eca7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-05 22:27:11 +02:00
Nikolaj Bjorner b97d694e5e undo model evaluation to BR_FULL pending regression in assertion violation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 22:26:57 +02:00
Christoph M. Wintersteiger efd923b826 Merge pull request #552 from MikolasJanota/bug_fix 
Avoiding adding spurious +0 in poly_rewriter::cancel_monomials.
 2016-04-05 19:06:19 +01:00
mikolas 05ce886afe Avoiding adding spurious +0 in poly_rewriter::cancel_monomials. 2016-04-05 17:26:48 +01:00
Christoph M. Wintersteiger 991eae8767 Merge pull request #2 from martin-neuhaeusser/ml_api_patch2 
Correct reference counting and handling of NULL pointers in new OCaml bindings.
 2016-04-05 13:01:04 +01:00
martin-neuhaeusser 71f991c5df Avoid using physical equality checks in OCaml bindings (z3.ml) 
This patch avoids the use of physical equality wherever possible
and improves some details of the OCaml implementation.
 2016-04-05 12:51:03 +02:00
Nikolaj Bjorner c454b81b2c special case branching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 11:57:49 +02:00
Nikolaj Bjorner ed1a5797fb check that a clause was not removed to fix issue #551 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-04 20:15:49 +02:00
martin-neuhaeusser f133f478c8 Translate correctly between OCaml option values and NULL pointers 
This patch refactors the update_api script and the z3.ml implementation
to properly translate between OCaml options and NULL pointers. Some
unifications and simplifications (avoidance of unnecessary value allocation)
in the script that creates the native bindings.
 2016-04-04 17:16:15 +02:00
Nikolaj Bjorner ec5a4ba63d add documentation comment for evaluation, Issue #536 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-04 12:59:18 +02:00
Nikolaj Bjorner 9667185af0 issue #549, replace BoolVal by False, otherwise creates regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 12:53:50 +02:00
Nikolaj Bjorner 11e8f06272 issue #549, replace False by BoolVal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 12:52:15 +02:00
Nikolaj Bjorner 33e7640645 disable mb branching pending unit test analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-03 10:53:37 +02:00
martin-neuhaeusser b85516c271 Fix reference counting in the C layer of the OCaml bindings 
The Z3 context and its reference counters are stored in a structure which is allocated
by the C layer outside the OCaml heap, whenever a Z3 context is created. The structure
and its Z3 context are disposed, once the last reference counter reaches zero. Reference
counters are decremented by C-level finalizers.

The OCaml representations for a Z3 context wrap only a pointer to the corresponding structure.
 2016-04-03 09:41:06 +02:00
Nikolaj Bjorner 03336ab9f2 add evaluation of array equalities to model evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-02 15:07:01 +02:00
Nikolaj Bjorner f6aaa5cc8d Merge pull request #550 from seahorn/farkas 
typo: gt -> ge
 2016-04-02 11:13:30 +02:00
Arie Gurfinkel 44d4902bb4 typo: gt -> ge 2016-04-02 10:13:14 +02:00
Christoph M. Wintersteiger ccd18283e7 Moved extension_converter func_interp entry compression to func_interp. 
Relates to #547
 2016-04-01 15:38:38 +01:00
Christoph M. Wintersteiger 3b82604590 whitespace 2016-04-01 15:37:40 +01:00
Christoph M. Wintersteiger d55a6725c9 Compressed func_interps in extension_model_converter. 
Fixes #547.
 2016-04-01 15:17:38 +01:00
Christoph M. Wintersteiger eb9c5b7cdb Disabled bogus assertions. 
Fixes #489
 2016-04-01 13:25:37 +01:00
Christoph M. Wintersteiger 852dc6d190 whitespace 2016-04-01 13:22:16 +01:00
Christoph M. Wintersteiger 405650c183 bugfix for ackr_model_converter (refcounts were off due to func_interps not being copied properly). 2016-04-01 13:17:48 +01:00
Christoph M. Wintersteiger dafda681b2 Bugfix for zero-extend. 
Fixes #548
 2016-04-01 12:48:06 +01:00
Christoph M. Wintersteiger dcca3a9bb1 whitespace 2016-04-01 12:46:49 +01:00
Christoph M. Wintersteiger b178420797 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-31 18:11:30 +01:00
Christoph M. Wintersteiger f4c330ba5c Merge pull request #1 from martin-neuhaeusser/my-ml-api 
Use a custom block for storing a Z3_config in the ML bindings.
 2016-03-31 18:10:43 +01:00
Martin R. Neuhaeusser feae0e8277 Use a custom block for storing a Z3_config in the ML bindings. 2016-03-31 18:31:59 +02:00
Christoph M. Wintersteiger bf92e53688 Annotation fix for pattern/quantifier probes 2016-03-30 18:35:49 +01:00
Christoph M. Wintersteiger 1724811e1b qffp tactic cleaned up to be in line with the default behavior of other tactics. 2016-03-30 15:23:46 +01:00
Christoph M. Wintersteiger cb2bf48254 Added has_quantifier probe 2016-03-30 15:22:53 +01:00
Christoph M. Wintersteiger d746b410cf whitespace 2016-03-30 15:22:21 +01:00
Christoph M. Wintersteiger 264bb6321a Merge pull request #545 from MikolasJanota/lackr 
Lackr, should fix #544
 2016-03-29 19:50:02 +01:00
Mikolas Janota 217c0419a1 Avoiding adding a superfluous unary AND in lackr. 2016-03-29 19:34:30 +01:00
Mikolas Janota 363f57a2f4 Silently bailing out on quantifiers in lackr. 2016-03-29 19:19:07 +01:00