mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
5916 commits 23 branches 48 tags 157 MiB
Commit graph

4785 commits

Author SHA1 Message Date
Nikolaj Bjorner 527c5191a6 Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 12:24:24 -07:00
Nikolaj Bjorner e8f4dd76c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-17 17:29:33 -07:00
Nikolaj Bjorner 77b245b3d8 fix proof production to avoid crash. Issue #733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-17 17:29:19 -07:00
Nikolaj Bjorner cda967ead2 guard verbose output by verbosity level for datalog command-line tool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-16 15:36:40 -07:00
Nikolaj Bjorner 7f29674842 add option to bypass compression of unbound tails, issue #738 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-16 14:56:10 -07:00
Christoph M. Wintersteiger 7a3308110c Merge pull request #722 from wintersteiger/i715 
x64 clause allocator bug fix
 2016-09-16 19:53:08 +01:00
Mikolas Janota 147c0f8152 Removing an unused method from bv_rewriter. 2016-09-16 19:44:37 +01:00
Mikolas Janota ec47a1df50 Adding bv preprocessing techniques. 2016-09-16 19:44:37 +01:00
Christoph M. Wintersteiger 27ea7d8e9d style/formatting 2016-09-16 19:34:48 +01:00
Christoph M. Wintersteiger b70cc47a9d x64 clause allocator fix for del_clause 2016-09-16 19:25:41 +01:00
Christoph M. Wintersteiger 5b1cb49973 x64 clause allocator bug fix 2016-09-16 19:25:41 +01:00
Andrew Dutcher 02217d048b replace all non-portable filepath slashes with os.path.join 2016-09-14 14:19:10 -07:00
Andrew Dutcher 02783d0bfb Minor tweaks to make things more reliable/less obnoxious 2016-09-14 01:49:37 -07:00
Andrew Dutcher 704105306c FINISH IT 2016-09-14 01:40:01 -07:00
Andrew Dutcher 0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Andrew Dutcher fa6cc19184 Moved python bindings into package 2016-09-14 01:33:07 -07:00
Nikolaj Bjorner 9f77759cd6 ensure that status is displayed in SMT-LIB2 compliant way. Issue #734 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-13 10:34:34 -07:00
Nikolaj Bjorner 5a86815f34 fix regression in seq-replace rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-11 05:43:16 -07:00
Nikolaj Bjorner 1450594fc6 add patch to deal with bug exposed in issue #721 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 12:15:49 -07:00
Nikolaj Bjorner 0b57829bdd fix heisenbug, unintialized variable, issue #720 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 11:04:29 -07:00
Nikolaj Bjorner cb140011bc add missing rewrite rule. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:42:36 -07:00
Nikolaj Bjorner 2f67665c7e ensure stoi axiom even when no value is present for argument. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:40:21 -07:00
Nikolaj Bjorner d74e618565 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-08 13:59:22 -07:00
Nikolaj Bjorner e485d1889c update replace semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:59:13 -07:00
Nikolaj Bjorner 76cf28d48b move from uint_set to hashtable over unsigned to save memory overhead in consequence generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:34:59 -07:00
Nikolaj Bjorner 94b67412ec Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-07 11:59:06 -07:00
Nikolaj Bjorner c5dd441947 fixes to consequence generation and cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-07 11:50:26 -07:00
Nikolaj Bjorner 2d9dced1c7 fix spacing, cast to Bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 20:18:31 -07:00
cttghc 758266b952 Fix omission of Z3_model_has_interp in z3++.h 2016-09-06 18:32:41 -05:00
Nikolaj Bjorner 0e9758a211 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-06 14:39:19 -07:00
Nikolaj Bjorner 3b70dd6678 tuning by using get_consequences2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 14:29:40 +08:00
AlexVonB c6b0fc444c Fix VisualStudio 2010 compiler warning C4100 
When compiling with Visual Studio 2010 the buildlog warns of the following: `z3++.h: warning C4100: 'e' : unreferenced formal parameter` and `z3++.h: warning C4100: 'c' : unreferenced formal parameter`. This merge request removes this warning.
 2016-09-05 16:22:00 +02:00
Nikolaj Bjorner 424a8c69bd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-02 03:05:23 -07:00
Nikolaj Bjorner dc48008d46 fixestoconsequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-02 11:00:40 +08:00
Nikolaj Bjorner c746d46d80 add validation code, fix bugs in consequence finder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-01 16:21:23 +08:00
Nikolaj Bjorner 4d9aadde35 updated consequence finder to fix bug in processing enumeration types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 16:15:36 +08:00
Nikolaj Bjorner 237fde1f76 fix crash during shutdown. Issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-31 09:57:46 +08:00
Nikolaj Bjorner 310c0f31a1 use type constrsaints for co-variant subtying to enable .net 3.5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 12:07:06 +08:00
Nikolaj Bjorner d4539b8887 fix dt2bv transformation to only work with constants, issue #725 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-30 11:42:14 +08:00
Nikolaj Bjorner 882c3bd0cd fix unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 18:18:11 -03:00
Nikolaj Bjorner 510231df42 fix to #717. The bottom-up COI filter can only use positive facts for filtering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 12:26:38 -03:00
Nikolaj Bjorner b5c521e4b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-23 11:44:48 -03:00
Nikolaj Bjorner 0a09d5ff52 check for non-nullness when handling optional info fields for marking. Fixes issue #719 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-23 11:33:40 -03:00
Christoph M. Wintersteiger b03dc0af3b fixed memory leaks 2016-08-20 17:57:00 -04:00
Christoph M. Wintersteiger 47e95f8676 Fixed binding substitution in macro_util 2016-08-20 17:56:52 -04:00
Nikolaj Bjorner 879f792125 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:13:52 -07:00
Nikolaj Bjorner 2d8325ed43 fix axiomatization of str.replace. Fixes issue #703 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 06:05:13 -07:00
Nikolaj Bjorner 439e8e6b04 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-20 03:53:55 -07:00
Nikolaj Bjorner f2b5c11d1c add option for prettier proof printing, Issue #706 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-20 03:52:45 -07:00
Nikolaj Bjorner 5069da62a3 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:45:06 -07:00
Nikolaj Bjorner e132c5eae8 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:42:40 -07:00
Nikolaj Bjorner b2383a481a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-18 18:02:22 -07:00
Nikolaj Bjorner 665fccf07a addressing max-segment issue for AMD64 + Debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-18 18:01:29 -07:00
Christoph M. Wintersteiger e8141aaa84 debug fixes 2016-08-12 19:52:59 +01:00
Christoph M. Wintersteiger 244c641234 debug check fix 2016-08-12 13:19:12 +01:00
Christoph M. Wintersteiger b74bff7fb7 logic detection fix 2016-08-10 11:39:47 +01:00
Christoph M. Wintersteiger f54a7db108 Added debug traces. 2016-08-09 16:36:49 +01:00
Christoph M. Wintersteiger ff3c630207 .NET API: Added MkMul from IEnumerable. 2016-08-09 16:36:32 +01:00
Christoph M. Wintersteiger 03aa6914a3 Fixed sub-logic detection for the ALL logic. 2016-08-09 13:20:45 +01:00
Nikolaj Bjorner aee6a7fe4c Merge pull request #708 from dstaple/master 
Removed complete() from handling of y.is_zero() in process_power
 2016-08-06 09:06:34 -07:00
Nikolaj Bjorner 14e8126f16 wrapping interruptable with solver consequence call 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-05 11:32:12 -07:00
Douglas B. Staple 87b7674245 Removed complete() from handling of y.is_zero() in process_power 2016-08-05 14:11:51 -03:00
Nikolaj Bjorner f3ef59b095 fix scanner bug at EOF 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-04 13:17:37 -07:00
Nikolaj Bjorner 6582330cc4 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 14:25:57 -07:00
Nikolaj Bjorner bbfe02b25a modulating data-type solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 11:16:29 -07:00
Nikolaj Bjorner 491b3b34aa tune consequence finding. Factor solver pretty-printing as SMT-LIB into top-level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 11:14:29 -07:00
Nikolaj Bjorner cb2d8d2107 add detection of non-fixed variables to consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 19:12:41 -07:00
Nikolaj Bjorner 7562efbe84 add consequence command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 12:59:29 -07:00
Nikolaj Bjorner 7346098895 fix unsat core extraction code in smt_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 11:22:34 -07:00
Nikolaj Bjorner d32019f4c9 fix consequence tracking for negated assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 10:49:06 -07:00
Nikolaj Bjorner 7d545d902d switch to specialized consequence generator in combined_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:36:11 -07:00
Nikolaj Bjorner 2263be1b4d adding consequence examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:24:14 -07:00
Nikolaj Bjorner 82d0310d94 remove repeated default argument, remove tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 21:13:12 -07:00
Nikolaj Bjorner 5c99405db3 finish consequence fast path code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 20:15:47 -07:00
Nikolaj Bjorner 4958edeb42 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 19:40:49 -07:00
Nikolaj Bjorner fa48703445 fix build for non C++11 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 17:04:47 -07:00
Nikolaj Bjorner 0055254f4c fix build for non C++11 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 17:04:06 -07:00
Christoph M. Wintersteiger 2e362aa6c0 build fix 2016-07-29 01:02:48 +01:00
Nikolaj Bjorner 46c911a92f Merge pull request #700 from lorisdanto/master 
added symbolic automata complement for sequences
 2016-07-28 17:00:23 -07:00
Nikolaj Bjorner 8221a09659 fast path for antecedent extraction in smt_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 16:49:19 -07:00
Loris D'Antoni 73bd4acfc5 added symbolic automata complement for sequences 2016-07-28 13:50:05 -07:00
Nikolaj Bjorner 074f1ad778 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 11:20:23 -07:00
Nikolaj Bjorner 14f29e7265 add basic built-in consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:20:17 -07:00
Christoph M. Wintersteiger 6f874c5c1d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 18:07:48 +01:00
Christoph M. Wintersteiger 7fefe40f21 Added/improved facilities for strong name signing of the .NET assembly. 2016-07-28 18:07:34 +01:00
Christoph M. Wintersteiger 0d83f99d8d Fixed comment 2016-07-28 18:06:26 +01:00
Christoph M. Wintersteiger 3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Nikolaj Bjorner b7de813c63 set solver on simplify command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 15:35:44 -07:00
Nikolaj Bjorner 0997eba700 adding hash/eq to uint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 13:41:41 -07:00
Nikolaj Bjorner 5f5ef8b38d adding support for distinct for dt2bv, re-entry harness for ~Context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 09:02:56 -07:00
Christoph M. Wintersteiger 8fa29f6970 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-26 19:21:57 +01:00
Christoph M. Wintersteiger eec68cfa2d Added 32/64 bit indication and githash to output of -version. 2016-07-26 19:21:50 +01:00
Nikolaj Bjorner 67c6f9be91 have the classifier revert to full arithmetic on non-difference logic, reported on http://stackoverflow.com/questions/38594208/changing-order-of-z3-fixepoint-queries-changes-the-result/38596187#3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-26 10:32:54 -07:00
Nikolaj Bjorner 56c78753f0 updating default solver selection. Add dt2bv transformation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-24 18:16:32 -07:00
Nikolaj Bjorner a85c5f0fac add handling of recognizers to enumeration types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-24 17:29:17 -07:00
Nikolaj Bjorner 6bf446dfc2 add tactic to eliminate enumeration sorts in favor of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-23 14:13:40 -07:00
Nikolaj Bjorner 083939ab0e add tactic to eliminate enumeration sorts in favor of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-23 14:11:21 -07:00
Nikolaj Bjorner 3581f6de42 remove stale SLS option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-21 18:18:42 -07:00
Nikolaj Bjorner f522d995d1 apply 'to-real' coercion only on integers. bug reported by Geoff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 19:03:25 -07:00
Nikolaj Bjorner b56837e09b fix build break: throw only on invalid model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 13:11:22 -07:00
Nikolaj Bjorner a59ed0fc2f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-20 12:18:16 -07:00
Nikolaj Bjorner 60711bb0cd deal with model construction, issue #684. fix model construction for ite #678. WIth this version, issue #686 does not repro 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 12:18:07 -07:00
Nikolaj Bjorner fe34e8bf00 Add OP_INTERNAL to handle cases of function symbols that don't have external semantics (at least in a way that is supported by means of building terms) Issue #688 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 12:13:54 -07:00
Nikolaj Bjorner 5f39c4371c fix proof generation for unit resolution. Issue #691 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 11:54:39 -07:00
Nikolaj Bjorner 6559fd817d Fix bit-blasting discrepancy. #690 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 10:53:53 -07:00
Nikolaj Bjorner cf48eb5f72 mark also ast in parameters as GC roots. Issue #676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-17 19:16:15 -04:00
Nikolaj Bjorner 64674386de fix ubuntu build failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-15 13:39:50 -07:00
Nikolaj Bjorner 6f971a3a86 add object z3 objects to target context during translation, to fix build regression failure on z3test.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-15 11:44:38 -07:00
Nikolaj Bjorner 4f5b0667ef fix rounding mode for pseudo-boolean constraint creation, Issue #683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-14 12:34:18 -07:00
Nikolaj Bjorner 3a83788b97 remove unfinished ite-macro finder, tune ast GC to ensure nodes are roots only once 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-14 09:46:09 -07:00
Nikolaj Bjorner 4720d578a4 add proper garbage collection to ast_manager. Issue #679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-14 09:05:16 -07:00
Nikolaj Bjorner b080e3a216 garbage collect all api::object references when calling del_context. Request issue #679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 22:26:21 -07:00
Nikolaj Bjorner f30fb7639e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-13 20:32:24 -07:00
Nikolaj Bjorner 3989d238c0 fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 20:32:18 -07:00
Nikolaj Bjorner 3a70b6aab4 fix model generation, add rewrite rules for sin(acos(x)) reduction to help model validation. Issue #680 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 11:12:27 -07:00
Nikolaj Bjorner 247e94a7c0 fix model generation for cos/sin transformation. Issue #680 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-13 10:34:12 -07:00
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
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
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
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 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
Nikolaj Bjorner 30cf0d19eb use of mk_bool_val 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 09:11:45 -07:00
Nikolaj Bjorner f72d9c25c6 merge with update to bv rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 09:08:01 -07:00
Nikolaj Bjorner 017165c474 fix bug with model completion and remove spurious std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 09:02:12 -07:00
Christoph M. Wintersteiger 70301ad3c8 Added bv*mul_no*flow handling in bv_rewriter. 
Fixes #657.
 2016-06-24 16:25:11 +01:00
Nikolaj Bjorner 67ea78a4a5 Add basic MARCO example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 08:00:23 -07:00
Nikolaj Bjorner 914bf2ff3b extend constant folding for bit-vector overflow/underflow operators, #657 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-24 07:43:05 -07:00
Christoph M. Wintersteiger e9eb88e1b3 fixed java build issues. Relates to #648. 2016-06-24 15:08:56 +01:00
Christoph M. Wintersteiger 3e96a7972f Merge pull request #648 from cheshire/no_finalizers 
Replace finalizers with PhantomReferences in Java API
 2016-06-24 14:17:29 +01:00
Christoph M. Wintersteiger d90a575981 Merge pull request #646 from martin-neuhaeusser/ocaml-c89 
Make C-layer of OCaml bindings C89 compatible.
 2016-06-24 13:40:50 +01:00
Nikolaj Bjorner 98a34ca51f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-23 21:39:34 -07:00
Nikolaj Bjorner c72ed3e6b4 update core minimization code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-23 21:39:28 -07:00
Christoph M. Wintersteiger 0a575936d0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-23 19:31:08 +01:00
Christoph M. Wintersteiger 8bde7b8a4c Added facilities for dumping smt_params for debugging purposes 2016-06-23 19:31:00 +01:00
Nikolaj Bjorner 41edf5f91e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-22 20:25:55 -07:00
Nikolaj Bjorner 5b497b6249 reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-22 20:25:47 -07:00
Christoph M. Wintersteiger 89b1d7d8da Fixed test case 2016-06-22 18:52:40 +01:00
Nikolaj Bjorner fa6f9b4a37 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-20 16:39:08 -07:00
Nikolaj Bjorner 9c099d6b1b fix mb maximization logic, so far not accessible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-20 16:39:03 -07:00
George Karpenkov b086aac45f Use constructors instead of static methods for Context.java. 2016-06-16 18:21:55 +02:00
Nikolaj Bjorner bfe26390f0 fix bug introduced when hiding unused variables in 96e157e, reported by Mikolas Janota 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-14 08:12:32 -07:00
Nikolaj Bjorner 8da0146318 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-14 08:10:21 -07:00
Nikolaj Bjorner 9253ca9d86 make use of warning_msg safe for formatting. Thanks to Scott McPeak for reporting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-14 08:10:10 -07:00
Christoph M. Wintersteiger c8c262fb93 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-06-14 13:14:30 +01:00
Christoph M. Wintersteiger 3ea71b4b25 Fixed SMT2 scanner to allow 0xFF characters. 
Thanks to Santiago Zanella-Beguelin for reporting this issue.
 2016-06-14 12:49:48 +01:00
Nikolaj Bjorner b11f9050e3 fix bugs exposed from bad indentation warnings, #650 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-13 18:20:25 -07:00
Nikolaj Bjorner 16ad33bf39 add collection of statistics #652 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-13 18:17:49 -07:00
George Karpenkov b65d83aacf Java API: explain the phantom references mechanics in Javadoc. 2016-06-13 12:22:32 +02:00
George Karpenkov a914822346 JavaAPI: DecRefQueue -- do not use move_limit for now. 2016-06-13 12:18:31 +02:00
George Karpenkov 26d6c99aac Typo in Javadoc. 2016-06-13 12:11:03 +02:00
George Karpenkov 27aa37946e Do not lock on context creation and deletion. 2016-06-13 12:09:34 +02:00
Nikolaj Bjorner c7ff05cc78 enable core minimization with qsat in case it turns out to be useful 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-12 15:58:12 -07:00
George Karpenkov 22ffd65d1e Java API: split incRef into incRef and addToReferenceQueue 
One method should do one thing only, it's easy to mix things up
otherwise.
 2016-06-12 21:01:58 +02:00
George Karpenkov 2a347f04bf Java API: FuncInterp.Entry should be an inner static class 
...as it does not use any fields of the outer FuncInterp object.
 2016-06-12 21:00:51 +02:00
George Karpenkov 5657399d55 Bugfix for incorrect order of operations. 2016-06-12 20:39:54 +02:00
George Karpenkov 495ef0f055 Java bindings with no finalizers 
Replacing finalizers with PhantomReferences, required quite a lot of
changes to the codebase.
 2016-06-12 20:27:01 +02:00
George Karpenkov dfc80d3b69 Do not needlessly catch exceptions in Java bindings 
A lot of existing code in Java bindings catches exceptions just to
silence them later.

This is:
a) Unnecessary: it is OK for a function to throw a RuntimeException
without declaring it.
b) Highly unidiomatic and not recommended by Java experts (see Effective
Java and others)
c) Confusing as has the potential to hide the existing bugs and have
them resurface at the most inconvenient/unexpected moment.
 2016-06-12 14:14:11 +02:00
Nikolaj Bjorner 9f5a117443 move mus to solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-10 16:24:14 -07:00
martin-neuhaeusser f069b1c0e9 Make C-layer of OCaml bindings C89 compatible. 
This patch ensures that the C code generated for the OCaml stubs complies with C89. It is needed to compile Z3 with OCaml support with Visual Studio versions older than VS2013.
 2016-06-10 16:49:06 +02:00
Nikolaj Bjorner 19f98547f7 fix memory leak Issue #643 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-06-09 21:59:10 -07: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
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
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 http://stackoverflow.com/questions/37669576/converting-z3-cnf-formula-into-list-of-lists-representation-using-z3py/37679447?noredirect=1#comment62859886_37679447)!
 2016-06-08 12:07:13 +01: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
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
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
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
Christoph M. Wintersteiger e28929c72c Removed hwf.rem test code. 2016-05-26 15:05:55 +01:00
Nikolaj Bjorner cdf3c2571c Merge pull request #622 from dstaple/master 
Export default tactic for use via the SMT-LIB 2 interface.
 2016-05-26 06:47:27 -07:00
Christoph M. Wintersteiger 4b00ea69db refcount fix for theory_fpa 2016-05-26 14:01:06 +01:00
Douglas B. Staple 725b1c56e5 Export default tactic for use via the SMT-LIB 2 interface. 2016-05-26 09:55:08 -03:00
Christoph M. Wintersteiger 15d871cfe0 Bug and style fix for fpa2bv converter. 2016-05-26 13:39:54 +01:00
Nikolaj Bjorner b8716b3339 avoid use-before-def crashes fp-operations.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 14:32:39 -07:00
Nikolaj Bjorner dfbbea31b7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-25 14:23:17 -07:00
Nikolaj Bjorner a07381ac19 fix regression in evaluator exposed by build failure on fp-array-6.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 14:23:07 -07:00
Christoph M. Wintersteiger 04a68bbb0a Eliminated a number of potential memory leaks in fpa2bv code. 
Relates to #615
 2016-05-25 18:50:57 +01:00
Christoph M. Wintersteiger f1c915bcf1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-25 18:21:14 +01:00
Christoph M. Wintersteiger ce69072305 Made nra tactic public. 2016-05-25 18:21:04 +01:00
Nikolaj Bjorner cd441c318e add compare utility to compress common cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 09:03:24 -07:00
Nikolaj Bjorner af3cc7e578 tune array evaluation, still disabled 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-25 08:57:59 -07:00
Christoph M. Wintersteiger c4610e0423 renamed variable to avoid clashes 2016-05-24 14:37:43 +01:00
Christoph M. Wintersteiger 9717161bb8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-05-24 10:58:23 +01:00
Nikolaj Bjorner c20b391cf7 reduce warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-05-23 14:32:51 -07:00
Christoph M. Wintersteiger 617e941015 fp2bv refactoring 2016-05-23 18:10:17 +01:00
Christoph M. Wintersteiger 8370bb8986 removed unused variable 2016-05-23 16:31:57 +01:00
Christoph M. Wintersteiger bf3a5effbc Fixed and refactored fp.min/fp.max for theory_fpa. 
Fixes #616
 2016-05-23 15:38:25 +01:00