Murphy Berzish
|
bd2b014008
|
debugging information for dependence analysis
|
2016-06-08 19:32:25 -04:00 |
|
Nikolaj Bjorner
|
cb29c07f06
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-06-08 13:56:12 -07:00 |
|
Nikolaj Bjorner
|
5253f3a12b
|
internalize unsupported operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-08 13:56:01 -07:00 |
|
Murphy Berzish
|
04fe8f66df
|
concat-eq-concat type 1 split 0
|
2016-06-08 16:22:31 -04:00 |
|
Christoph M. Wintersteiger
|
9b91e6ff0a
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-06-08 12:07:19 +01:00 |
|
Christoph M. Wintersteiger
|
a2eb824590
|
Added __nonzero__ and __bool__ functions to Python Z3 ASTs to enable use of Python lists (and similar).
Thanks to Vlad Shcherbina for the recommendation (see 37679447 (comment62859886_37679447) )!
|
2016-06-08 12:07:13 +01:00 |
|
Nikolaj Bjorner
|
314eae50a4
|
Merge pull request #641 from kanigsson/master
Take into account number of monomials for rlimit counting
|
2016-06-07 19:27:06 -07:00 |
|
Johannes Kanig
|
9bfa73ee06
|
Take into account number of monomials for rlimit counting
Should fix issue #611
|
2016-06-08 11:17:26 +09:00 |
|
Murphy Berzish
|
513b4922ee
|
tracing code for string-integer integration
|
2016-06-07 17:40:59 -04:00 |
|
Murphy Berzish
|
62aeff90c5
|
fix string theory setup so that string-integer integration actually works
|
2016-06-07 17:38:57 -04:00 |
|
Nikolaj Bjorner
|
47f97dde89
|
Merge pull request #639 from MikolasJanota/master
Adding translation to ackr_model_converter.
|
2016-06-06 10:09:21 -07:00 |
|
Mikolas Janota
|
9df2a183d6
|
Adding translation to ackr_model_converter.
|
2016-06-06 18:06:45 +01:00 |
|
Nikolaj Bjorner
|
736f2bef46
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-06-04 20:08:26 -07:00 |
|
Nikolaj Bjorner
|
e8d85f91d7
|
disable filtering on negated tails. Issue #634
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-04 20:08:13 -07:00 |
|
Murphy Berzish
|
e0df5bc2ed
|
fixups for string-integer
|
2016-06-04 16:29:10 -04:00 |
|
Christoph M. Wintersteiger
|
f2a869fb58
|
std::unordered_map -> std::map
|
2016-06-04 11:01:46 +01:00 |
|
Christoph M. Wintersteiger
|
626b9160bf
|
collect-statistics additions
|
2016-06-03 20:45:42 +01:00 |
|
Christoph M. Wintersteiger
|
b54ef3623b
|
added collect-statistics tactic
|
2016-06-03 20:26:05 +01:00 |
|
Nikolaj Bjorner
|
19db0c5f2c
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-06-03 10:13:27 -07:00 |
|
Nikolaj Bjorner
|
219b47822b
|
avoid qsat when formulas are quantifier-free. Go directly to SMT
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-03 10:13:16 -07:00 |
|
Christoph M. Wintersteiger
|
a94aff23e6
|
Added clearer FP conversion functions to the Python API.
Implements #476
|
2016-06-03 13:23:12 +01:00 |
|
Nikolaj Bjorner
|
e9e926d4d6
|
UINT32_MAX -> UINT_MAX
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-02 21:00:18 -07:00 |
|
Nikolaj Bjorner
|
21158ea03f
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-06-02 20:58:20 -07:00 |
|
Nikolaj Bjorner
|
eab5a84f62
|
fix issues with int.to.str and seq.len encodings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-06-02 20:57:52 -07:00 |
|
Christoph M. Wintersteiger
|
83ad5d65e4
|
Replaced fp.rem conversion to bit-vectors with an SMT-compliant one.
Fixes #561
|
2016-06-02 20:22:02 +01:00 |
|
Christoph M. Wintersteiger
|
b3b5c6226b
|
MPF code simplification
|
2016-06-02 17:12:24 +01:00 |
|
Murphy Berzish
|
33205cea71
|
completely bypass theory_seq; sorry! I'll put it back when I'm done
|
2016-06-01 17:57:00 -04:00 |
|
Murphy Berzish
|
b5fe473c3a
|
fix compilation errors after merge
|
2016-06-01 17:50:45 -04:00 |
|
Murphy Berzish
|
d79837eed0
|
Merge branch 'develop' into upstream-master
Conflicts:
.gitignore
README
src/ast/ast_smt2_pp.h
src/ast/ast_smt_pp.cpp
src/ast/reg_decl_plugins.cpp
src/cmd_context/cmd_context.cpp
src/parsers/smt2/smt2parser.cpp
|
2016-06-01 17:40:52 -04:00 |
|
Murphy Berzish
|
bc79a73779
|
lower/upper bound WIP
|
2016-06-01 17:23:47 -04:00 |
|
Murphy Berzish
|
f8f7014a18
|
use LRA instead of LIA in strings setup, so that the theory_seq integer value code works
|
2016-06-01 16:34:48 -04:00 |
|
Christoph M. Wintersteiger
|
ade2dbe15a
|
Cache cleanup fix for bv_simplifier_plugin.
Fixes #615
|
2016-05-31 16:47:14 +01:00 |
|
Christoph M. Wintersteiger
|
47e75827ee
|
theory_fpa refactoring
|
2016-05-31 16:22:48 +01:00 |
|
Christoph M. Wintersteiger
|
302c491535
|
theory_fpa refactoring
|
2016-05-31 16:22:24 +01:00 |
|
Christoph M. Wintersteiger
|
03f6b465b9
|
comment typos
|
2016-05-31 16:14:50 +01:00 |
|
Nikolaj Bjorner
|
39acd3594a
|
test variants for seq_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-30 18:15:10 -07:00 |
|
Nikolaj Bjorner
|
f03032bd09
|
updated seq solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-29 14:01:05 -07:00 |
|
Nikolaj Bjorner
|
cddf8091b5
|
strengthen support for int.to.str and length reasoning. Issue #589
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-28 12:36:50 -07:00 |
|
Nikolaj Bjorner
|
c3f498a640
|
strengthen support for int.to.str and length reasoning. Issue #589
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-28 12:26:47 -07:00 |
|
Nikolaj Bjorner
|
8c99d3c431
|
tidy unbound compressor code, add invariant checks
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-28 11:05:26 -07:00 |
|
Nikolaj Bjorner
|
3aea63edb1
|
check for cancellation before internalizing and during to avoid errors. Issue #625
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-27 17:27:37 -07:00 |
|
Nikolaj Bjorner
|
236f1c2a3e
|
bypass stale rules as part of unbounded compression. Issue #624
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-27 10:31:28 -07:00 |
|
Nikolaj Bjorner
|
18a9b89e30
|
bypass stale rules as part of unbounded compression. Issue #624
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-27 09:38:23 -07:00 |
|
Nikolaj Bjorner
|
50d334e4e9
|
fix non-determinism bug in simple joins. Keys were normalized based on pointer equality not object identifier equality. Also some ptr hashtables were used with pointer hashes, and then traversed. reported in issue #619
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-27 07:51:02 -07:00 |
|
Nikolaj Bjorner
|
cfffb0b3c5
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-05-27 07:49:45 -07:00 |
|
Nikolaj Bjorner
|
84ff6fd62a
|
fix non-determinism bug in simple joins. Keys were normalized based on pointer equality not object identifier equality. Also some ptr hashtables were used with pointer hashes, and then traversed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-05-27 07:49:38 -07:00 |
|
Christoph M. Wintersteiger
|
18340b0e95
|
fix for pb2bv_model_converter
|
2016-05-26 18:42:57 +01:00 |
|
Christoph M. Wintersteiger
|
1fe4a82c76
|
Added implementation of pb2bv_model_converter::translate
Fixes #623
|
2016-05-26 18:39:51 +01:00 |
|
Christoph M. Wintersteiger
|
ec270acd32
|
Removed hwf.mul/hwf.div test code.
|
2016-05-26 15:11:21 +01:00 |
|
Christoph M. Wintersteiger
|
9752888704
|
Merge branch 'master' of https://github.com/Z3Prover/z3
|
2016-05-26 15:06:02 +01:00 |
|