updates to seq and bug fixes (#4056)

* na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4037 * nicer output for skolem functions * more overhaul of seq, some bug fixes * na * added offset_eq file * na * fix #4044 * fix #4040 * fix #4045 * updated ignore * new rewrites for indexof based on #4036 * add shortcuts * updated ne solver for seq, fix #4025 * use pair vectors for equalities that are reduced by seq_rewriter * use erase_and_swap * remove unit-walk * na * add check for #3200 * nits Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * name a type Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove fp check Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove unsound axiom instantiation for non-contains Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix rewrites Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4053 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #4052 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 22, 2020 · 95a78b2 · 95a78b2
1 parent 53c14bd
commit 95a78b2
Show file tree

Hide file tree

Showing 39 changed files with 1,516 additions and 1,654 deletions.
diff --git a/.gitignore b/.gitignore
@@ -73,6 +73,7 @@ src/api/ml/z3enums.ml
 src/api/ml/z3native.mli
 src/api/ml/z3enums.mli
 src/api/ml/z3.mllib
+out/**
 *.bak
 doc/api
 doc/code

diff --git a/README.md b/README.md
@@ -204,6 +204,9 @@ See [``examples/python``](examples/python) for examples.
 
 [WebAssembly](https://github.com/cpitclaudel/z3.wasm) bindings are provided by Clément Pit-Claudel.
 
+### ``Julia```
+Julia bindings can be enabled using the build option Z3_BUILD_JULIA_BINDINGS from the CMake system.
+
 ## System Overview
 
 ![System Diagram](https://github.com/Z3Prover/doc/blob/master/programmingz3/images/Z3Overall.jpg)

diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
@@ -96,6 +96,10 @@ class ll_printer {
     void display_params(decl * d) {
         unsigned n = d->get_num_parameters();
         parameter const* p = d->get_parameters();
+        if (n > 0 && p[0].is_symbol() && d->get_name() == p[0].get_symbol()) {
+            n--;
+            p++;
+        } 
 
         if (n > 0 && !d->private_parameters()) {
             m_out << "[";