Arie Gurfinkel
ac6ca4d334
factored out is_variable_proc to a header file
2017-06-20 21:34:49 -04:00
Nikolaj Bjorner
42e7d29df3
Merge pull request #1089 from agurfinkel/fixes
...
Fixes
2017-06-20 18:28:01 -07:00
Arie Gurfinkel
625874e66f
remove debug code
2017-06-20 21:07:38 -04:00
Arie Gurfinkel
372e8b3c49
expose iterator api of obj_hashtable
2017-06-20 21:07:38 -04:00
Arie Gurfinkel
f3019a3de9
api to accumulate stopwatches
2017-06-20 21:07:38 -04:00
Arie Gurfinkel
6eced8836d
expose iterators in expr_map
2017-06-20 21:07:38 -04:00
Arie Gurfinkel
e9100854b9
ensure that variable names are properly quoted
2017-06-20 21:07:38 -04:00
Arie Gurfinkel
69a3e984aa
add is_hypothesis() method
2017-06-20 21:07:38 -04:00
Nikolaj Bjorner
e48e7ef7be
fix assertion, start addressing #1087 by using size_t
2017-06-20 14:38:58 -07:00
Nikolaj Bjorner
0ef14acf2e
fix build break
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-20 14:25:56 -07:00
Nikolaj Bjorner
0fa6274a65
Fix bug #1079 , integrality testing seems to have been wrong
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-20 14:18:43 -07:00
Christoph M. Wintersteiger
78e8e8b893
Kick CI
2017-06-20 18:06:18 +01:00
Christoph M. Wintersteiger
237e6dcd3f
Kick CI
2017-06-20 17:21:24 +01:00
Christoph M. Wintersteiger
ee2fc41626
Kick CI
2017-06-20 15:17:49 +01:00
Christoph M. Wintersteiger
a0b25147d9
Fix for the fix for #1062 .
2017-06-20 14:48:03 +01:00
Christoph M. Wintersteiger
e9258731e4
Merge branch 'master' of https://github.com/Z3Prover/z3
2017-06-20 14:39:26 +01:00
Christoph M. Wintersteiger
ab21caf55f
Reverted fix for quoted echo strings when smtlib2_compliant=false. Kindly reported by Armael Gueneau. Fixes #1062 .
2017-06-20 14:39:22 +01:00
Christoph M. Wintersteiger
054e139c0d
Whitespace
2017-06-20 14:37:26 +01:00
Christoph M. Wintersteiger
7b97688302
Whitespace, typo.
2017-06-20 14:36:40 +01:00
Nikolaj Bjorner
907899debe
Merge branch 'master' of https://github.com/z3prover/z3
2017-06-19 18:24:45 -05:00
Nikolaj Bjorner
f375016a11
disable tweak to seq until there are cycles to test further
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-19 18:23:27 -05:00
Nikolaj Bjorner
894c60bdf9
fix bug in qe-lite reported in #1086 : bookkeeping of unconstrained variables only works for quantifier-free formulas
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-19 18:22:30 -05:00
Christoph M. Wintersteiger
b27a4a3593
Merge pull request #1084 from dennis714/master
...
small typo
2017-06-19 12:00:17 +01:00
Dennis Yurichev
345c0c796b
Merge branch 'master' of github.com:dennis714/z3
2017-06-19 13:56:52 +03:00
Dennis Yurichev
e547000bcf
typo
2017-06-19 13:52:30 +03:00
Nikolaj Bjorner
02161f2ff7
revert internalize logic for re until debugged
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-15 21:13:25 -07:00
Nikolaj Bjorner
e67572ffa6
address issues raised in #998
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-15 20:47:59 -07:00
Nikolaj Bjorner
5be3e959ab
address issues raised in #998
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-15 20:46:47 -07:00
Nikolaj Bjorner
d3320f8b81
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-14 21:48:19 -07:00
Nikolaj Bjorner
f4214e1c71
Merge branch 'master' of https://github.com/z3prover/z3
2017-06-14 21:41:31 -07:00
Nikolaj Bjorner
8ac43c981a
use less memory #1078
2017-06-14 21:41:24 -07:00
Christoph M. Wintersteiger
d8a02bc040
Fixed AST translation functions in .NET and Java APIs. Fixes #1073 .
2017-06-14 13:24:54 +01:00
Nikolaj Bjorner
2d1abf2795
Merge pull request #1076 from chaserhkj/default-pp-mode-api
...
Fix Z3_PRINT_SMTLIB_FULL not working as expected
2017-06-14 03:04:22 -07:00
KangJing Huang (Chaserhkj)
e3f32ca3a8
Fix Z3_PRINT_SMTLIB_FULL not working as expected
2017-06-14 02:18:21 -04:00
Nikolaj Bjorner
c980cfd783
add concat recognizer
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-13 20:51:55 -07:00
Nikolaj Bjorner
b978f78c21
add sequence recognizers
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-13 20:35:35 -07:00
Nikolaj Bjorner
8b12cc0bdf
fix build warning
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-13 19:58:55 -07:00
Nikolaj Bjorner
c2acbc2957
port FuncDecl copy to dotnet, continuation of #1073
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-13 19:11:28 -07:00
Nikolaj Bjorner
7023af4528
Merge branch 'master' of https://github.com/z3prover/z3
2017-06-13 19:03:45 -07:00
Nikolaj Bjorner
a59ee8032c
fix unsoundness bug in axiomatization of str.at. #1067
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-13 19:02:59 -07:00
Nikolaj Bjorner
5066bd01f7
Merge pull request #1070 from delcypher/cmake_file_move
...
[CMake] Move CMake files into their intended location
2017-06-13 13:27:25 -07:00
Nikolaj Bjorner
90a38c9a35
Merge pull request #1073 from chaserhkj/funcdecl-translate-java
...
Add translate method for FuncDecl in java api
2017-06-13 13:27:12 -07:00
KangJing Huang (Chaserhkj)
5799947183
Fix docstrings for FuncDecl.translate
2017-06-13 02:37:41 -04:00
KangJing Huang (Chaserhkj)
3a692fe33c
Add translate method for FuncDecl in java api
2017-06-13 00:37:02 -04:00
Nikolaj Bjorner
6bce173248
properly quote symbols #1061
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-12 18:35:02 -07:00
Dan Liew
814fcd6a17
[CMake] Remove documentation on "Bootstrapping". It is no longer
...
relevant.
2017-06-12 11:59:39 +01:00
Dan Liew
5c3b11f034
[CMake] Modify contrib/cmake/bootstrap.py to do nothing except
...
print a warning.
Now that the CMake files have been moved into their intended location
it is no longer necessary for this script to exist.
However we do not want to break out-of-tree scripts that build Z3 using
CMake to suddenly break. So the script has been modified to do nothing
except print a warning.
Eventually we should remove this script.
2017-06-12 11:59:39 +01:00
Dan Liew
5be503798f
[CMake] Remove bootstrap check. Now that the CMake files are in
...
their correct location we don't need it anymore.
2017-06-12 11:59:38 +01:00
Dan Liew
4b517b96df
[CMake] Move CMake files into their intended location so the
...
`contrib/cmake/bootstrap.py` script no longer needs to be executed.
The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461 . While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.
The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.
This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Nikolaj Bjorner
f0fa439c48
escaping names in get-assignment #1061
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-11 17:17:47 -07:00
