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

6820 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
9f99482f07 fix model generation for cos/sin transformation. Issue #680 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 10:29:31 -07:00
Christoph M. Wintersteiger
1e5a87887d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-13 15:36:27 +01:00
Christoph M. Wintersteiger
a21d701fa1 tabs 2016-07-13 15:36:21 +01:00
Christoph M. Wintersteiger
3bea00efe3 added smt_params trace 2016-07-13 15:35:29 +01:00
Christoph M. Wintersteiger
cfbe16639f Bugfix for fpa2bv translation 2016-07-13 15:35:14 +01:00
Nikolaj Bjorner
63f89f8c45 add sin/cos conversions for #680 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-12 15:12:40 -07:00
Murphy Berzish
8d47b08244 fix out-of-scope value tester bug in theory_str::gen_free_var_options() 
we now pass tests/z3str/charAt-003.smt2 with detailed debugging turned off!
 2016-07-10 13:05:41 -04:00
Nikolaj Bjorner
f96cfeae9e fix build failures under linux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 13:28:39 -07:00
Nikolaj Bjorner
73cdf809fe Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-09 12:36:22 -07:00
Nikolaj Bjorner
0a6b03808c fix core extraction for QF_BV theory/inc_sat_solver based on regressions pointed out by Matthias Heizmann and Tjark Weber 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 12:35:54 -07:00
Nikolaj Bjorner
8f862f8fed fix core extraction for QF_BV theory/inc_sat_solver based on regressions pointed out by Matthias Heizmann and Tjark Weber 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 12:35:11 -07:00
Christoph M. Wintersteiger
7cf80845fd Merge pull request #675 from FabianWolff/master 
Fix spelling errors
 2016-07-09 17:32:10 +01:00
Nikolaj Bjorner
d7d22cad02 undo comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 05:38:03 -07:00
Nikolaj Bjorner
3d73fe55c7 track assumptions when calling check-sat. regression detected by Tjark Weber running core extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 05:31:49 -07:00
Nikolaj Bjorner
53b3edc8cc add cases for recognizing ALL. Issue #674 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-09 05:18:26 -07:00
Fabian Wolff
6eaab00e83 Fix spelling errors 2016-07-09 11:46:43 +02:00
Nikolaj Bjorner
59865f5502 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-08 17:57:12 -07:00
Nikolaj Bjorner
d5ee7e24bc add simplification for equalities between itos and constant strings, Issue #589 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-08 11:50:39 -07:00
Nikolaj Bjorner
bdbf1c9bf4 add support for default semantics for stoi (non-integer strings map to -1). Issue #670 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-08 10:45:19 -07:00
Murphy Berzish
8aa6fee0af fixups wip 2016-07-08 12:21:11 -04:00
Murphy Berzish
847a5fc1f8 replace old mk_value behaviour in theory_str that creates placeholders for unused terms instead of crashing 2016-07-07 16:13:48 -04:00
Murphy Berzish
9eead64d03 prevent assertion of basic string axioms on variables that go out of scope (theory_str) 
this is testing a crash avoidance feature, the regression is tests/z3str/regex-026.smt2

this also adds some debugging code for a substr() crash but that is WIP
 2016-07-06 17:31:37 -04:00
Nikolaj Bjorner
e9e10f1d5c checking cancel flag to refine the behavior around issue #595 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-03 10:38:54 -07:00
Nikolaj Bjorner
0d0d504d62 change names of reserved identifiers. Issue #666 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-01 14:46:44 -07:00
Nikolaj Bjorner
654780bb4b check that model is availble before evaluation, issue #595 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-01 09:26:01 -07:00
Nikolaj Bjorner
4c786c5f70 add n-ary disjunction and conjunction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-01 08:15:50 -07:00
Murphy Berzish
7d903ff1fa implement process_concat_eq_unroll, WIP 2016-06-30 04:55:11 -04:00
Murphy Berzish
b53da182b6 fix gen_assign_unroll_reg so that it does not assert a contradiction 2016-06-30 04:39:09 -04:00
Murphy Berzish
a2d6149df5 add general-case regex unroll model generation 
WIP as there is currently a SAT-as-UNSAT bug I'm trying to fix

This also changes the semantics of lower_bound and upper_bound,
no longer wrapping the expr that is passed in with mk_strlen().
This actually makes these methods useful for checking bounds
of things other than strings.
 2016-06-30 04:00:42 -04:00
Murphy Berzish
b4110c886f successful unroll of simple unbounded Str2Reg 2016-06-30 02:46:16 -04:00
Murphy Berzish
427632ede3 let free variable assignment work a bit more towards unrolls 2016-06-30 01:42:00 -04:00
Murphy Berzish
21f0a50aba add Unroll check to get_eqc_allUnroll 2016-06-30 01:24:43 -04:00
Murphy Berzish
03827cb487 add more Unroll support to final_check, ctx_dep_analysis 2016-06-30 01:21:21 -04:00
Nikolaj Bjorner
e518d4a5fe typename conventions, issue #664 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-29 17:02:36 -07:00
Nikolaj Bjorner
fd95a9e061 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-29 16:53:46 -07:00
Nikolaj Bjorner
c2f9d35d59 throw exceptions when internalizing expressions with free variables, issue #663 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-29 16:53:28 -07:00
Nikolaj Bjorner
37c9a31296 Merge pull request #661 from cheshire/fix_java_leak 
Java bindings: Force cleaning the queue on context closing.
 2016-06-29 04:56:11 -07:00
Nikolaj Bjorner
5d5004193b avoid crash on box models under cancellation. Issue #654 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-29 04:54:31 -07:00
Nikolaj Bjorner
0fdf01e410 avoid crash on box models under cancellation. Issue # SASSERT(!m_box_models.empty()); 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-29 04:53:28 -07:00
George Karpenkov
cb87991d5f Java bindings: Force cleaning the queue on context closing. 2016-06-29 13:09:05 +02:00
Nikolaj Bjorner
8aee7129f6 shortcircuit stats functions on ground terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-28 21:48:49 -07:00
Nikolaj Bjorner
b303fd59c0 add some version information (and date) to log file to make it easier to trap version mismatch on log files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-28 18:11:30 -07:00
Nikolaj Bjorner
e4a00f6f6f re-include get_error_msg_ex per issue #660 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-28 17:48:11 -07:00
Nikolaj Bjorner
84aec95eda fix up use-list in 3x3 resolution case. Regression RND_3_24.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-28 11:41:57 -07:00
Nikolaj Bjorner
014c693fa5 fix explain map to use negations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-27 15:22:13 -07:00
Murphy Berzish
b31d1a92aa add more support for unroll (WIP) 2016-06-27 14:41:57 -04:00
Nikolaj Bjorner
f786ab15fb add example for MSS enumeration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-26 20:58:48 -07:00
Nikolaj Bjorner
b66d457b19 move arithmetical mbp functionality to model_based_opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-26 16:12:14 -07:00
Nikolaj Bjorner
7fc294d329 move arithmetical mbp functionality to model_based_opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-26 14:30:35 -07:00
Christoph M. Wintersteiger
628a6378c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-24 18:13:08 +01:00