mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity
7350 commits 23 branches 48 tags 157 MiB
Commit graph

5993 commits

Author SHA1 Message Date
Christoph M. Wintersteiger e315d063c5 renamed LP bound propagator to avoid linker name clashes 2017-08-01 16:07:51 +01:00
Christoph M. Wintersteiger 6bc5209e26 Fixed build problems with .vcxproj 2017-08-01 15:53:55 +01:00
Nikolaj Bjorner 72c478078e adding cdecl directive to Z3_qe_lite to address build failure for Java bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 23:14:53 -07:00
Nikolaj Bjorner 1820ccd491 z3-qe-lite? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 22:15:57 -07:00
Nikolaj Bjorner b12882d94a a few more spacer related warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 21:56:13 -07:00
Arie Gurfinkel 25c6480e6e updated include directives 2017-07-31 23:16:42 -04:00
Arie Gurfinkel ecd85b314c more includes 2017-07-31 22:51:28 -04:00
Arie Gurfinkel 66108085fa removing pragmas to make travis happy 2017-07-31 22:51:28 -04:00
Nikolaj Bjorner c506f3ddc9 fix build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 18:39:35 -07:00
Nikolaj Bjorner 0eb2915e83 Merge pull request #1182 from agurfinkel/spacer-z3 
Spacer
 2017-07-31 17:10:09 -07:00
Nikolaj Bjorner 49cf899207 remove local change 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 16:33:48 -07:00
Nikolaj Bjorner 5cda9504f1 remove relative include from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 16:32:26 -07:00
Christoph M. Wintersteiger e8cdc34219 Debug fix in fpa2bv converter. Relates to #872. 2017-07-31 22:34:58 +01:00
Arie Gurfinkel ffff16632d updating includes 2017-07-31 17:30:11 -04:00
Arie Gurfinkel f465a2225a fixing include paths 2017-07-31 17:14:43 -04:00
Christoph M. Wintersteiger 6a2fa91818 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 22:12:37 +01:00
Christoph M. Wintersteiger 9601761a6f Added missing float conversion in fpa2bv converter. Relates to #1178. 2017-07-31 22:12:15 +01:00
Arie Gurfinkel 97c5ab30d5 small improvements to bmc engine 
courtesy of Marc Brockschmidt
 2017-07-31 17:04:36 -04:00
Arie Gurfinkel 7168451201 eager quantifier instantiation for quantified array properties 2017-07-31 17:04:16 -04:00
Arie Gurfinkel 2c7a39d580 Optionally blast arrays 
This changes the default behavior of always blasting arrays.
The old behavior can be restored using

   fixedpoint.xform.array_blast=true
 2017-07-31 17:03:18 -04:00
Arie Gurfinkel f5fa6b0bcb optionally disable subsumption checker 2017-07-31 17:03:18 -04:00
Arie Gurfinkel 33c81524d2 optionally disable propagate variable equivalences in interp_tail_simplifier 2017-07-31 17:03:18 -04:00
Arie Gurfinkel 86db446afa python spacer-specific API 2017-07-31 17:03:18 -04:00
Arie Gurfinkel d080c146a2 public API for spacer 2017-07-31 17:03:18 -04:00
Arie Gurfinkel c3d433ede0 implemented spacer-specic muz API 2017-07-31 17:03:18 -04:00
Arie Gurfinkel 1530a39a96 stubs for spacer-specific API 2017-07-31 17:03:18 -04:00
Arie Gurfinkel ffa4957362 do not use array_der when simplifying rules 2017-07-31 17:02:29 -04:00
Arie Gurfinkel a73023da97 preserve rule names when changing rules 2017-07-31 17:02:29 -04:00
Arie Gurfinkel 5b9bf74787 Spacer engine for HORN logic 
The algorithms implemented in the engine are described in the following papers

Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan:
Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. FMCAD 2015: 89-96

Nikolaj Bjørner, Arie Gurfinkel:
Property Directed Polyhedral Abstraction. VMCAI 2015: 263-281

Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki:
SMT-Based Model Checking for Recursive Programs. CAV 2014: 17-34
 2017-07-31 17:02:29 -04:00
Arie Gurfinkel 9f9dc5e19f increased verbosity level of smt_context 2017-07-31 17:01:47 -04:00
Arie Gurfinkel ba6594b241 extra smt params used by spacer 2017-07-31 17:01:47 -04:00
Arie Gurfinkel b269e6b35b comments on proof_utils 2017-07-31 17:01:47 -04:00
Nikolaj Bjorner 013127e947 fix build break based on ambiguous path resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 14:01:39 -07:00
Nikolaj Bjorner 063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -07:00
Nikolaj Bjorner b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger bbf0ebcb74 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 20:18:53 +01:00
Christoph M. Wintersteiger 507356c7bf Fixed bug in fpa2bv converter. Fixes #1178. 2017-07-31 20:18:39 +01:00
Nikolaj Bjorner d130ae2e4f Merge pull request #1181 from agurfinkel/tweaks 
Tweaks
 2017-07-31 11:55:52 -07:00
Nikolaj Bjorner 71d80ab47f fix build break based on new assertion in smt-eq-justification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 11:54:11 -07:00
Christoph M. Wintersteiger 52cf80d637 Simplified bit-vector bounds in fp.rem. Relates to #872. 2017-07-31 19:53:55 +01:00
Christoph M. Wintersteiger ecfd241e19 Injected 3 missing bits of precision into fp.rem. Relates to #872. 2017-07-31 19:53:44 +01:00
Arie Gurfinkel 1d5713c376 move semantics for ref 2017-07-31 14:21:30 -04:00
Arie Gurfinkel 331eec8a05 option to control array_der in qe_lite 2017-07-31 14:19:16 -04:00
Arie Gurfinkel 7670b49ada mark mk_true() and mk_false() const 2017-07-31 14:14:35 -04:00
Arie Gurfinkel 15451ae858 extra flags to control quant_hoist 2017-07-31 14:13:45 -04:00
Arie Gurfinkel be1df279ec make proof_checker less verbose 2017-07-31 14:11:07 -04:00
Nikolaj Bjorner 2ec9944edd Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 10:51:37 -07:00
Christoph M. Wintersteiger a59907170d Fixed renormalization in fp.mul. Relates to #872. 2017-07-31 18:34:46 +01:00
Nikolaj Bjorner 3e8ce53d87 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 09:53:16 -07:00
Nikolaj Bjorner 62b8394bdd fixes #1179 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:52:45 -07:00
Nikolaj Bjorner 74890ca1c8 fixes #1180 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:37:25 -07:00
Nikolaj Bjorner ceca9fbef0 fixes #1176 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:23:55 -07:00
Nikolaj Bjorner 8bd0407adf fix #1177 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 09:13:50 -07:00
Christoph M. Wintersteiger 175f042db8 Fixed renormalization in fp.fma. Relates to #872. 2017-07-28 23:01:01 +01:00
Christoph M. Wintersteiger e677030b74 Fixed sign bug in mpf fp.fma. Relates to #872. 2017-07-28 21:39:44 +01:00
Christoph M. Wintersteiger a30c343d7a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-28 20:24:35 +01:00
Christoph M. Wintersteiger 0610392a05 Bugfix for fp.fma. Fixes #872. 2017-07-28 20:16:13 +01:00
Arie Gurfinkel 78467077f6 fixing a build error 2017-07-28 12:18:12 -04:00
Nikolaj Bjorner 31d6abcfe8 remove arity check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:55:41 -07:00
Nikolaj Bjorner e9b9a29339 revert first fix for #1173, replace by handling single arity chainables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:44:19 -07:00
Nikolaj Bjorner 64233034cc fix #1173 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:26:52 -07:00
Christoph M. Wintersteiger 33ebdc8adc Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. 2017-07-27 23:08:35 +01:00
Nikolaj Bjorner ca67274519 another round of fix for #989 to avoid problems with doxygen generation (TravisCI build failure) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 12:59:34 -07:00
Nikolaj Bjorner c8b5be48de unexpressing interpolants #1172 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 11:44:52 -07:00
Nikolaj Bjorner 18e9e4f4ac fixes #1169 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 09:25:01 -07:00
Nikolaj Bjorner 21759e5eb2 fixes #1172 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 08:59:12 -07:00
Nikolaj Bjorner 6558999cef fixes #1171 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 08:46:20 -07:00
Nikolaj Bjorner d3e1d250a7 fixes #1168 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 07:50:16 -07:00
Nikolaj Bjorner 2cc6baede5 address #1167 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-27 07:44:08 -07:00
Nikolaj Bjorner 1a07c6c188 address ASAN bug report #1160 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-26 20:48:49 -07:00
Nikolaj Bjorner b1298d7bde ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-26 20:28:55 -07:00
Nikolaj Bjorner 3f8b63f5a8 Merge branch 'master' of https://github.com/z3prover/z3 2017-07-26 19:52:11 -07:00
Nikolaj Bjorner bb7b3c510f fix for #1161 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-26 19:52:05 -07:00
Nikolaj Bjorner 9f9c575451 fix bug exposed when running test-z3.exe /a in debug mode, #1159. Add assertions to heap interaction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-25 16:26:45 -07:00
Christoph M. Wintersteiger 75b533f050 Fixed normalization shift in MPF rounder. Relates to #872. 2017-07-25 20:29:10 +01:00
Christoph M. Wintersteiger f1c0ac72e7 Fix for fp.fma encoding. Relates to #872. 2017-07-25 20:29:10 +01:00
Nikolaj Bjorner 9d6be286d0 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-25 10:18:43 -07:00
Nikolaj Bjorner 70f6280bf1 fix regression reported in #1159 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-25 10:18:21 -07:00
Nikolaj Bjorner 3865c45382 Merge pull request #1147 from mtrberzi/fix-get-arith-value 
Improved theory_arith integration in theory_str::get_arith_value()
 2017-07-24 21:21:45 -07:00
Nikolaj Bjorner 741f940119 Merge pull request #1158 from facanferff/master 
pretty printer: fix typo with ReSort sort name
 2017-07-24 21:19:18 -07:00
Nikolaj Bjorner 49f88d9d90 fix uninitialized warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 12:52:10 -07:00
Nikolaj Bjorner a94f5fb04a fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 12:15:10 -07:00
Nikolaj Bjorner ae5e39a8b8 Merge branch 'master' of https://github.com/z3prover/z3 2017-07-24 09:18:27 -07:00
Nikolaj Bjorner 7fd0777cf1 fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 09:18:16 -07:00
Nikolaj Bjorner a0a8bc2a62 fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 09:12:43 -07:00
Fábio Ferreira 2e2782577b pretty printer: fix typo with ReSort sort name 2017-07-23 02:32:35 +01:00
Christoph M. Wintersteiger 0f1583309d Bugfix for fp.fma. One piece of puzzle #872. 2017-07-21 21:12:45 +01:00
Christoph M. Wintersteiger faa19117e4 Fixed inconsistent state upon solver interruption. Partially fixes #951. 2017-07-21 17:42:48 +01:00
Christoph M. Wintersteiger 943dc8118a Improved collect-statistics tactic 2017-07-20 13:44:47 +01:00
Murphy Berzish 7ddb940f77 add e_internalized() check in theory_str::get_arith_value() 2017-07-19 10:15:38 -04:00
Murphy Berzish 69f0ed9b1f remove disabled code block in get_arith_value() 2017-07-18 13:13:12 -04:00
Murphy Berzish c6707688ba improved get_arith_value() in theory_str 
Since the root of the eqc of an integer term should be a constant
if there is a constant in that eqc, we can ask for it directly
without either iterating over the entire eqc or
asking the arithmetic solver (and receiving potentially stale info).
 2017-07-18 13:11:03 -04:00
Christoph M. Wintersteiger da34de340d Fixed bug in sat model converter. Fixes #1148. 2017-07-15 20:25:13 +01:00
Christoph M. Wintersteiger 680f342247 Merge pull request #1145 from delcypher/fix_doc_typo 
Fix minor typo in C API documentation
 2017-07-12 15:47:44 +01:00
Dan Liew 5b511f12b3 Fix minor typo in C API documentation 2017-07-12 13:07:19 +01:00
Dan Liew 89c8f1722f Fix typo that prevented uses of bvsmod_i being parsed. 2017-07-12 12:53:10 +01:00
Jack Feser 0e45777104 add get_num_scopes to python solver api 2017-07-11 14:42:34 -04:00
Murphy Berzish 86e7f83e06 proper theory_arith integration in theory_str::get_arith_value() 2017-07-11 13:24:48 -04:00
Nikolaj Bjorner 2b0106c199 doc fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-09 11:26:27 +02:00
Nikolaj Bjorner 2af08a378d avoid complaining about division by 0 as unhandled in theory-lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 18:21:47 -07:00
Nikolaj Bjorner 5714f830b0 fix check for finite sorts #1122 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 13:37:24 -07:00
Nikolaj Bjorner ea331ebfbe revert update to #1134 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 08:29:16 -07:00
Nikolaj Bjorner d06e48a361 detect overlapping signatures #1134 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 08:13:14 -07:00
Nikolaj Bjorner 49cf3f8008 update documentation according to #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-07 07:44:55 -07:00
Nikolaj Bjorner 465ed7d068 adding doc #1132 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-05 10:21:57 -07:00
Murphy Berzish b14364a117 fix theory_str warnings: rename get_value() to get_arith_value() 2017-07-05 11:06:40 -04:00
Nikolaj Bjorner 41803ec1cf fix trace/debug build for unreferenced variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 19:55:38 -07:00
Nikolaj Bjorner cba9a160d3 deal with warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 19:42:22 -07:00
Nikolaj Bjorner 5b8e3ae198 Merge pull request #1129 from mtrberzi/fix-warnings 
clean up warnings in theory_str
 2017-07-04 19:41:43 -07:00
Nikolaj Bjorner bd92797663 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 15:25:59 -07:00
Nikolaj Bjorner d66db280a8 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:43:32 -07:00
Nikolaj Bjorner a1306eaab6 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:17:37 -07:00
Nikolaj Bjorner 253870c6d7 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:08:23 -07:00
Murphy Berzish 03fe3d74f8 clean up warnings in theory_str 2017-07-04 13:28:18 -04:00
Nikolaj Bjorner 031d7e1b59 use iterators, update build icon for osx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 16:58:40 -07:00
Nikolaj Bjorner 08524a2d90 cleanup for warning message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 11:47:17 -07:00
Nikolaj Bjorner be4b0ffe69 fix unsoundness bug instroduced when fixing #1125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-30 19:36:38 -07:00
Nikolaj Bjorner c44c8284bd use worklist algorithm to avoid stack overflow #1125 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-30 18:10:36 -07:00
Christoph M. Wintersteiger 1a59123819 Fixed x86/x64 issues in theory_str 2017-06-28 12:49:10 +01:00
Lev Nachmanson 4d0fda81df fix run of lp_solver for mps files 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-06-27 11:45:29 -07:00
Lev Nachmanson dfe15adf7e fix maybe non initialized warning 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-06-26 16:32:44 -07:00
Nikolaj Bjorner 244cbc2638 ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-26 10:04:50 -07:00
Nikolaj Bjorner 7db1847f51 fix bitrot in maxsat example reference management #1116 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-26 09:36:53 -07:00
Dan Liew 42e0f8f9ce Unbreak Z3 C++ API exception support for GCC < 5.0. This was broken 
by 0b1d564509 .

Older versions of GCC do not define `__cpp_exceptions` which caused
exceptions to not be raised leading to unexpected failures. To fix
this also check the `__EXCEPTIONS` macro which is used by older GCC
versions.

Also `#undef` the `Z3_THROW` macro at the end of the header file
because this is an implementation detail that we don't want to leak
to clients.
 2017-06-25 23:03:39 +01:00
Christoph M. Wintersteiger 2fceac04d4 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-25 22:19:54 +01:00
Christoph M. Wintersteiger c395516058 Adjusted rlimit increments in theory_arith to avoid non-termination issues 2017-06-25 22:19:42 +01:00
Christoph M. Wintersteiger ffbf19d944 Merge branch 'master' of https://github.com/wintersteiger/z3 2017-06-25 20:46:14 +01:00
Christoph M. Wintersteiger ad7aff2334 Added rlimit increments in theory_arith to avoid non-termination issues via F*. 2017-06-25 20:45:56 +01:00
Nikolaj Bjorner 1631a68981 make the option soup dependencies more user-friendly, #1109 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-23 16:57:50 -07:00
Nikolaj Bjorner 1681419052 adding change notes to release notes for a future release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-23 16:50:33 -07:00
Nikolaj Bjorner 9d1852343c add separate get-objectives command #1107 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-23 16:34:38 -07:00
Nikolaj Bjorner e3ec7e7d05 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-23 11:34:18 -07:00
Nikolaj Bjorner cd4bb5beaf another fix for #1101 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-23 11:34:10 -07:00
Arie Gurfinkel c7fbab0c11 propagate rule names during xform 2017-06-23 09:38:04 -04:00
Arie Gurfinkel 0dead22dca fix missing initialization 2017-06-23 09:38:04 -04:00
Arie Gurfinkel 9874db7458 [CMake] typos in cmake 2017-06-23 09:37:49 -04:00
Nikolaj Bjorner 7386f2e045 #1101 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-22 14:18:53 -07:00
Lev Nachmanson 2a5f1d6e93 add a template instantination 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-06-22 10:32:35 -07:00
Nikolaj Bjorner 77ffa9f32f Merge pull request #1095 from agurfinkel/mev_fix 
model_evaluator fix
 2017-06-21 20:17:44 -07:00
Arie Gurfinkel 972ab6298c (mev) only reduce function interpretation 2017-06-21 22:59:52 -04:00
Nikolaj Bjorner 2d49119d2a add note to Context documentation about scoped uses of contexts #1077 2017-06-21 18:56:16 -07:00
Arie Gurfinkel 493a3a6312 (mev) call expand_value only at the end 
There is no need to expand array values throughout evaluation.
They are expanded during array equality checking (if requested), and
can be expanded at the very end of evaluation (if needed).
 2017-06-21 20:58:10 -04:00
Arie Gurfinkel d5ca902bf6 (mev) bug fix in expanding array equalities 
The stores were processed in the wrong order so that

  (store (store a x y) x u)

was reduced to

  (store a x y)

instead of

  (store a x u)
 2017-06-21 20:58:10 -04:00
Arie Gurfinkel e62e563e2d (mev) renamed variable to clarify that it is unused 2017-06-21 20:58:10 -04:00
Nikolaj Bjorner 1fee5fd94e Merge pull request #1094 from delcypher/cmake_fix_generated_cpp_deps 
[WIP][CMake] Fix broken regeneration of some .cpp files
 2017-06-21 17:47:41 -07:00
Dan Liew d00892c9a6 [CMake] Fix dependencies for generating mem_initializer.cpp. 
Previously CMake was not aware of which headers files the generation
of `mem_initializer.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declare memory initializers/finalizers change.
* New headers are added that declare memory initializers/finalizer.

Now the `z3_add_component()` CMake function has been modifed so that
it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument
which allows the headers that declare memory initializers/finalizers
to be explicitly listed.

With this information CMake will now regenerate `mem_initializer.cpp`
correctly.

This required the `mk_mem_initializer_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:56:53 +01:00
Dan Liew 6f48a145aa [CMake] Fix dependencies for generating gparams_register_modules.cpp. 
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.

This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:56:46 +01:00
Dan Liew 229fd3dc3e [CMake] Fix dependencies for generating install_tactic.cpp. 
Previously CMake was not aware of which headers files the generation
of `install_tactic.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared tactics/probes changed.
* New tactics/probes were added to new header files.

Now the `z3_add_component()` CMake function has been modifed to take an
optional `TACTIC_HEADERS` argument which allows the headers that declare
tactics/probes to be explicitly listed. The necessary component
declarations have been modified to declare their tactic/probe header
files.

With this information CMake will now regenerate `install_tactic.cpp`
correctly.

This required the `mk_install_tactic_cpp_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:03:48 +01:00
Nikolaj Bjorner b516f22549 refine test for non-fd to be more inclusive while addressing #1092 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-21 08:01:03 -07:00
Nikolaj Bjorner a3ee785923 disable dt2bv for quantified variables as enum2bv does not handle them. #1092 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-21 07:29:21 -07:00
Arie Gurfinkel af28057980 preserve dl rule names during xforms 2017-06-20 22:23:55 -04:00
Arie Gurfinkel 50f794c4f5 api for accessing dl_rule name 2017-06-20 22:23:55 -04:00
Arie Gurfinkel 7840f6cead typo in a comment 2017-06-20 22:23:55 -04:00
Arie Gurfinkel ef62621f50 make qe_lite prefer simpler definitions 2017-06-20 21:51:08 -04:00
Arie Gurfinkel 9f73359a86 improve comments 2017-06-20 21:50:35 -04:00
Arie Gurfinkel ac6ca4d334 factored out is_variable_proc to a header file 2017-06-20 21:34:49 -04: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 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
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
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 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
Nikolaj Bjorner f5b54f042c apply correction by ddcc #1069 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-11 11:40:39 -07:00
Dan Liew c629dcc53f [Doxygen] Rewrite documentation of Z3_mk_solver() and 
`Z3_mk_simple_solver()` to try to make it clearer what the differences
are between these APIs.

This an attempt to address issues noted in #1035.
 2017-06-11 14:04:18 +01:00
Nikolaj Bjorner f44a3e1bbc print_core as a function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 10:18:07 -07:00
Nikolaj Bjorner 8acb37e734 revert change to 1065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:45:18 -07:00
Nikolaj Bjorner 582a069c51 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-10 09:31:02 -07:00
Nikolaj Bjorner b8e8e090ad filter assumptions by membership in initial list #1065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:30:01 -07:00
Nikolaj Bjorner d5f646929e print success #1068 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:16:36 -07:00
Dan Liew bcb3981c5f [Doxygen] Fixed mismatched @{ and @} declaration which prevented 
the `capi` group from being declared properly. For example this
prevented from `Z3_mk_solver()` from appearing in the `capi` group.
 2017-06-07 18:49:43 +01:00
Dan Liew 85c7f5d865 [Doxygen] Fix some Doxygen warnings for z3_optimization.h 2017-06-07 18:45:12 +01:00
Christoph M. Wintersteiger 0137104683 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-06 16:04:45 +01:00
Christoph M. Wintersteiger 83e9c40265 Added __deepcopy__ operators to ref-counted objects in the Python API 2017-06-06 16:04:38 +01:00
Nikolaj Bjorner af285d02c3 add documentation per #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-05 08:38:28 -07:00
Nikolaj Bjorner 4f04301305 add documentation per #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-05 07:55:32 -07:00
Nikolaj Bjorner a8ff97c0f4 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-04 11:05:21 -07:00
Nikolaj Bjorner 668bad6121 print success after reset assertions #1057 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-04 11:04:54 -07:00
Nikolaj Bjorner efd5727676 add shorthand for enumerating constants in a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:35:09 -07:00
Nikolaj Bjorner 2908ab4069 fix reference count issue with pinning to expr_ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:56:25 -07:00
Nikolaj Bjorner e9ed3af455 fix regression in str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:35:35 -07:00
Nikolaj Bjorner fda59f5a24 expose operator kinds for internal functions using their sequence variants. Issue #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:32:17 -07:00
Nikolaj Bjorner 1fa60f4893 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-01 09:11:09 -07:00
Nikolaj Bjorner 52e0f3b539 add string accessors to managed APIs #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:10:49 -07:00
Christoph M. Wintersteiger 596652ed36 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-31 18:35:52 +01:00
Christoph M. Wintersteiger 4f0a87299c Fixed signed/unsigned comparison warnings 2017-05-31 18:35:06 +01:00
Christoph M. Wintersteiger a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner 546d22e77a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-30 11:18:43 -07:00
Nikolaj Bjorner 415824b600 put temporaries on trail 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-30 11:18:33 -07:00
Nikolaj Bjorner 870017e2ce Merge pull request #1049 from chaserhkj/java-api-update-fix 
`Expr.update()` in java API should not return super class
 2017-05-29 18:14:54 -07:00
KangJing Huang (Chaserhkj) 8092dd5aa3 Fix Expr.update in java API returning superclass 2017-05-29 20:51:42 -04:00
Nikolaj Bjorner 4cbf938cf3 enable get-unsat-assumptions command per request in #1048 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 16:26:22 -07:00
Nikolaj Bjorner 2de80b5ce9 add pb built in ops for logic ALL #1045 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 10:08:50 -07:00
Nikolaj Bjorner d95ac58bad remove throw in reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 12:09:35 -07:00
Nikolaj Bjorner f80a622a8f add colon to assertion stack levels #1046 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 11:10:46 -07:00
Nikolaj Bjorner 1654ad7059 adding escape characters to reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-27 14:56:38 -07:00
Nikolaj Bjorner f3a0b7e0cd change command-line experience for pareto fronts. It now requires multiple check-sat calls to loop over the fronts. This allows querying each model in turn. #1008 2017-05-23 20:05:10 -07:00
Nikolaj Bjorner 49faaaa8f1 allowing non-literal assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 15:01:00 -07:00
Nikolaj Bjorner 6f2cd4817b ensure arith.reflect has default true 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 14:09:45 -07:00
Nikolaj Bjorner 3f89c1418b fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 12:51:14 -07:00
Nikolaj Bjorner 23ff580a67 get rid of timeb dependencies, pull request #1040 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 12:16:43 -07:00
Nikolaj Bjorner edb164587f get rid of a simplifier dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 10:12:32 -07:00
Nikolaj Bjorner af4346f16a expose arith reflection, get rid of long m_manager attribute in asserted fromulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 10:04:29 -07:00
Nikolaj Bjorner 2834fea9b3 fix x64 warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 08:58:21 -07:00
Nikolaj Bjorner 90af406338 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-23 08:51:38 -07:00
Nikolaj Bjorner 8e9739d3b0 work around crash #1039 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 08:51:26 -07:00
Nikolaj Bjorner 2cbeedec69 accept hereditarily finite sorts in datalog engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-22 19:32:43 -07:00
Nikolaj Bjorner 622d8c951c remove redundant data-type function declarations from pretty-printed output. #1034 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-22 14:40:42 -07:00
Nikolaj Bjorner b782ec35cc avoid print statements from assertions when the assertion does not trigger. Stackoverflow question http://stackoverflow.com/questions/44094927/creating-formula-taking-too-much-time-in-z3py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-21 10:35:59 -07:00
Ken McMillan bf7c6292bd removing FOCI2 interface from interp 2017-05-19 16:21:57 -07:00
Lev Nachmanson 1b62592015 change in a comment 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2017-05-18 13:44:00 -07:00
Nikolaj Bjorner 79a8e9aab0 fix build break #1029 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-18 12:09:51 -07:00
Nikolaj Bjorner 4069e76ab0 remove unused column function field, #1021 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 21:27:43 -07:00
Nikolaj Bjorner ceec81de0b simplify code, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:32:08 -07:00
Nikolaj Bjorner 7fab670719 fix regression, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:21:32 -07:00
Nikolaj Bjorner d2ac59f238 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-14 14:10:01 -07:00
Nikolaj Bjorner 3290a933b5 remove spurious include file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-14 14:09:42 -07:00