mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity
6215 commits 49 branches 53 tags 182 MiB
Commit graph

6215 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
f8a3a46d44 Merge pull request #921 from cheshire/obj_value_as_vector_java 
Obj value as vector java
 2017-02-27 09:53:23 -08:00
George Karpenkov
be1e9918f0 Class Optimize#Handle should be static, 
as it already includes an explicit reference to the Optimize class.
 2017-02-27 18:49:02 +01:00
George Karpenkov
b3be83e7c5 Sane indentation + removing extra spaces for Optimize.java 2017-02-27 18:48:44 +01:00
George Karpenkov
d6c79facc7 Java API for getting the objective value as a triple 
See #911 for the motivation,
and e02160c674 for the relevant change
in C API.
 2017-02-27 18:42:44 +01:00
Nikolaj Bjorner
899843b7cd fix unhandled finite domain sort rewrite case. Issue #918 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-26 17:20:54 -08:00
Nikolaj Bjorner
996c0f0666 fix type on exception message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-25 16:14:50 -08:00
Nikolaj Bjorner
c7591e3c99 remove unreferenced label 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:13:08 -08:00
Nikolaj Bjorner
183ee7e37d expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:10:18 -08:00
Nikolaj Bjorner
e02160c674 expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-24 11:07:40 -08:00
Nikolaj Bjorner
8437cb7132 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-24 07:54:25 -08:00
Murphy Berzish
0ebd93c8b5 add _re.unroll internal operator to seq_decl_plugin 2017-02-23 20:57:19 -05:00
Nikolaj Bjorner
e744d0f271 Merge pull request #910 from mtrberzi/octal-escape 
Add C-style octal escape sequences to seq_decl_plugin
 2017-02-23 16:02:21 -08:00
Murphy Berzish
eb0ba26f90 C-style octal escapes, including 1- and 2-digit escapes 2017-02-23 18:33:10 -05:00
Murphy Berzish
61bbf8ba7e add octal escape to seq_decl_plugin 2017-02-23 18:24:08 -05:00
Nikolaj Bjorner
b0dd3f3238 add recursive function graphs to model, adapt rewriter to bypass branches whose evaluation is redundant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-16 13:58:12 -08:00
Nikolaj Bjorner
c67cf1653c use non _ method from z3printer module so to be resilient against how _ is handled as indicator of private functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-15 08:46:58 -08:00
Nikolaj Bjorner
216e17e5e2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-13 08:16:43 -08:00
Nikolaj Bjorner
e7a21dfac2 add par_and_then 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-13 08:16:39 -08:00
Nikolaj Bjorner
6fcba26ea6 make parameters accessible from expressions. Issue #896 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-12 09:56:49 -08:00
Nikolaj Bjorner
b3dabc7ccf add missing mod/rem/is_int functionality to C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 16:28:15 -05:00
Nikolaj Bjorner
4c6efbbc8b expose numerator/denominators for Martin and Giles 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 16:02:51 -05:00
Nikolaj Bjorner
b42973152f fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 12:02:32 -05:00
Nikolaj Bjorner
3a0e9e8f53 add itos/stoi conversion to API. Issue #895 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-11 11:31:13 -05:00
Christoph M. Wintersteiger
e4411265ea Fixed model-converter segfault in ::check_sat. Relates to #881 2017-02-05 17:53:44 +00:00
Christoph M. Wintersteiger
54280b6cc5 Fixed model-converter segfault in ::check_sat. Relates to #881 2017-02-05 17:20:45 +00:00
Christoph M. Wintersteiger
d6b4e99489 Fixed signed/unsigned warnings 2017-02-05 16:03:00 +00:00
Christoph M. Wintersteiger
c5fe591dbc Merge pull request #739 from angr/fix/soname_version 
Set soname version correctly in cmake build
 2017-02-04 20:39:50 +00:00
Christoph M. Wintersteiger
59db0bc9c4 Merge pull request #829 from legendtang/fix_utf8_conf 
Fixed utf-8 version string handling for python2. Resolved #787
 2017-02-04 20:38:51 +00:00
Christoph M. Wintersteiger
5682c43604 Merge pull request #881 from dwoos/tactic-labels 
Thread labels through tactic system
 2017-02-04 20:37:11 +00:00
Christoph M. Wintersteiger
c56edc63d2 Merge pull request #882 from dwoos/sine-filter 
Add basic Sine Qua Non filtering
 2017-02-04 20:24:09 +00:00
Nikolaj Bjorner
999d17e29b Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-02 11:29:19 -08:00
Nikolaj Bjorner
bd0bd6052a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-02-02 10:19:21 -08:00
Nikolaj Bjorner
9ca52a3361 fix bug in lexicographic handling in maxres: previous assumptions were not committed in corner cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-02 10:19:11 -08:00
Nikolaj Bjorner
2e89c2de3d add par_or tactic to C++ API. #873 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-02 09:35:04 -08:00
Doug Woos
d6fbfe401e add and use new is_pattern recognizer 2017-02-01 16:21:15 -08:00
Doug Woos
44c417904b correctly pretty-print 2017-02-01 16:21:01 -08:00
Doug Woos
a147e2bc35 use is_uninterp 2017-02-01 16:20:40 -08:00
Nikolaj Bjorner
9cfd412cd0 enable pb theory always as pb terms can be introduced during transformations. Issue #884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-01 15:28:29 -08:00
Nikolaj Bjorner
256a0e2d82 move exchange par 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-01 12:12:26 -08:00
Nikolaj Bjorner
40177f7bac bypass combined solver when logic is set to QF_FD 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-01 08:05:04 -08:00
Nikolaj Bjorner
4d8d705b3f bypass combined solver when logic is set to QF_BV or QF_FD 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-02-01 08:02:24 -08:00
Nikolaj Bjorner
f015e3e4cc fix bug in propagation of parameters to combined solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-31 17:17:58 -08:00
Nikolaj Bjorner
bdfa84c6fe fix issues with running parallel solver: random strategy should not be a default on all solvers. Also reuse base solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-31 13:22:03 -08:00
Doug Woos
d9e43f0e6d use insert_if_not_there 2017-01-31 11:48:52 -08:00
Doug Woos
89ba99918e reindent 2017-01-31 11:48:52 -08:00
Doug Woos
c0bb6dd2be delete unused args 2017-01-31 11:48:51 -08:00
Doug Woos
da63f6b0ff delete comment 2017-01-31 11:48:51 -08:00
Doug Woos
b00c4d2e64 add name 2017-01-31 11:48:51 -08:00
Nikolaj Bjorner
1d1949e395 ensure that parallel threads are only invoked when thread count > 1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-30 18:30:06 -08:00
Doug Woos
8196173e29 Introduce and use labels_vec 2017-01-30 15:50:34 -08:00