mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 02:41:52 +00:00
Code Activity
5573 commits 23 branches 48 tags 156 MiB
Commit graph

5573 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner ceb3f0c869 patch full version for cmake to re-enable build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:30:39 -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 1239c8f8e8 update MSF example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 11:20:31 -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
Nikolaj Bjorner 375682e98d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-26 14:31:40 -07:00
Nikolaj Bjorner 9cab896632 adding sign option if keyfile is present 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-26 14:31:29 -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 d9afcb4eaf Merge pull request #695 from PhilippWendler/java-api-enum-lookup 
Java API: Improve enum lookup (fromInt methods)
 2016-07-23 11:16:03 -07:00
Philipp Wendler c3b8c15f35 Java API: Make enum lookup more efficient. 
The existing code causes an allocation of an array with all enum values
on every method call (inside the values() method),
and loops over all enum entries.
 2016-07-22 17:32:57 +02:00
Philipp Wendler f325b51213 Java API: In fromInt() methods of enums fail on invalid value. 
The existing code just returns one of the enum values if an unknown int
value is passed, silently hiding bugs.
 2016-07-22 17:32:57 +02:00
Nikolaj Bjorner 9ed2c846a9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-21 18:19:10 -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 16e3a91bdf fix issues reported by Geoff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-21 07:56:21 -07:00
Nikolaj Bjorner 1073e161c7 remove deprecated max-sat solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-20 19:08:23 -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 f3d657ebd1 add tptp5 example to cmake, adding output SZS directives for Geoff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-15 12:09:23 -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