mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity
6446 commits 24 branches 48 tags 158 MiB
Commit graph

6446 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish
fd968783a5 fix model generation for theory_str 2016-06-09 20:35:26 -04:00
Murphy Berzish
1520760a04 string-integer integration in free var gen 2016-06-09 20:31:21 -04:00
Murphy Berzish
91d82956b2 string concat-eq type 3 integer integration 2016-06-09 16:25:19 -04:00
Murphy Berzish
6f5ee2c3ce string concat-eq type 2 integer integration 2016-06-09 16:04:13 -04:00
Murphy Berzish
ae74b47924 string concat-eq type 1 integer integration 2016-06-09 15:41:31 -04:00
Christoph M. Wintersteiger
bd187e0989 Bugfix for fp.min/fp.max in fpa2bv converter; hide BV UFs from FP models. 
Fixes #642
 2016-06-09 17:51:31 +01:00
Christoph M. Wintersteiger
bfeab9cc15 Added facilities for hiding UFs in smt::model_generator 2016-06-09 17:49:45 +01:00
Christoph M. Wintersteiger
879363157f Bugfix for fpa2bv_converter 2016-06-09 12:09:53 +01:00
Murphy Berzish
6332372573 more debugging info in theory_str final check; fix variable classification bug 2016-06-08 20:01:56 -04:00
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