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

6289 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
0ab2067b69 produce error message for cores with optimization. Issue #825 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:15:40 +01:00
Nikolaj Bjorner
99b7c26e9f exposing regular expression features to address issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 13:05:02 +01:00
Nikolaj Bjorner
8e6600c6be add python API for newly exposed regex constructors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 09:09:03 +01:00
Nikolaj Bjorner
976fadf771 add missing complement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:21:57 +01:00
Nikolaj Bjorner
0473d2ef56 add regular expression features to C# API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:17:13 +01:00
Nikolaj Bjorner
a82b5e21fe add regular expression operations to C and C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 06:11:36 +01:00
Nikolaj Bjorner
4e25bffab6 add range constructor to .NET API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:33:02 +01:00
Nikolaj Bjorner
feb801564b adding range to C API. Issue #831 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-08 18:28:27 +01:00
Christoph M. Wintersteiger
dc0d29a00c Bugfix for model construction. Fixes #828. 2016-12-08 16:14:54 +00:00
Wensheng Tang
99d10d1224 Fixed utf-8 version string handling for python2. Resolved #787 2016-12-08 15:09:59 +08:00
Christoph M. Wintersteiger
f1a704484b Re-added context creation locks in the Java API. Relates to #819. 2016-12-01 23:16:15 +00:00
Nuno Lopes
dedae29300 add a few more statics to avoid symbol clashes 2016-12-01 17:37:07 +00:00
Nuno Lopes
e697d3e810 remove 2 outdated comments 2016-12-01 14:10:31 +00:00
Nuno Lopes
42b26c63e5 make a few functions static 2016-12-01 14:01:20 +00:00
Nikolaj Bjorner
7ebc660b6d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-30 09:52:15 -08:00
Nikolaj Bjorner
024082a45f adding preferred sat, currently disabled, to wmax. Fixing issue #815 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-30 09:52:05 -08:00
Nikolaj Bjorner
d9227b95ea blast distinct in incremental BV solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-29 15:45:23 -08:00
Nuno Lopes
4b4365470d mam compiler: move reset of matched_exprs cache next to code reset 2016-11-28 15:40:25 +00:00
Nuno Lopes
2babd192b8 small optimization in compilation of multi-patterns 
also make the path faster for single patterns
 2016-11-28 14:43:47 +00:00
Nuno Lopes
4452ac0d6d optimize pattern matching code generator for DAG patterns 
generated code now uses COMPARE instructions to compare subtrees instead of diving into both subtrees. Code is thus smaller and fails faster.
 2016-11-28 13:48:15 +00:00
Christoph M. Wintersteiger
1799310155 Fixed iterator invalidation bug in SAT probing. Relates to #798. 2016-11-26 14:07:05 +00:00
Nikolaj Bjorner
441dbbb94b streamline logging in arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-24 13:08:50 -08:00
Nikolaj Bjorner
facc3215da Merge pull request #805 from MartinNowack/feat_unlimited_timeout 
Do not request time stamp if not needed
 2016-11-23 08:49:38 -08:00
Martin Nowack
762e5fd093 Do not request time stamp if not needed 
If no timeout is needed for solving queries, time stamps do not
need to be acquired.
 2016-11-23 16:38:21 +01:00
Nuno Lopes
1d417f6527 fix warnings in configure script 2016-11-23 09:32:20 +00:00
Nikolaj Bjorner
7a4c20698f fix handling of AC operator ++ on regular expressions. Issue #804 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-22 13:02:17 -08:00
Christoph M. Wintersteiger
71ca355257 Fixed OpenMP problems in log synchronization. Relates to #798. 2016-11-22 13:26:29 +00:00
Christoph M. Wintersteiger
dee7c29b19 Added optional synchronization for multi-thread API logs. Relates to #798. 2016-11-22 11:32:25 +00:00
Christoph M. Wintersteiger
03f8b871a1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-21 14:49:37 +00:00
Christoph M. Wintersteiger
aaf449ae27 Fix for the documentation scripts. Fixes #799. 2016-11-21 14:49:32 +00:00
Nikolaj Bjorner
d3fe015ff5 Merge pull request #796 from rickyz/nondependent_name 
Fix GCC/Clang compilation.
 2016-11-20 06:29:37 -08:00
Nikolaj Bjorner
725e79e9eb re-enable ematching on recursive function definitions, disabling ematching breaks regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-20 06:24:47 -08:00
Nikolaj Bjorner
650a719298 fix crash in new clique code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-20 06:20:22 -08:00
Ricky Zhou
9939d07827 Fix GCC/Clang compilation. 
The calls to negate use a non-dependent name, so GCC and Clang do not
examine dependent base classes when looking up the name. Adds a using
declaration as suggested at
https://isocpp.org/wiki/faq/templates#nondependent-name-lookup-members.
 2016-11-20 05:09:30 -08:00
Nikolaj Bjorner
6a9b5ea3af fix unsoundness reported in issue #777, disable ematching on recursive function definition axioms exposed in #793 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 15:29:43 -08:00
Nikolaj Bjorner
2ff5af7d42 fix bug incorrect clearing of goals during node creation. Issue #777 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 10:06:16 -08:00
Nikolaj Bjorner
a5bae72bdf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-19 08:09:55 -08:00
Nikolaj Bjorner
df0e3a100c tune initialization for wmax and sortmax 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 08:04:06 -08:00
Nikolaj Bjorner
ea601dd403 fix and coallesce clique functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-19 03:55:48 -08:00
Christoph M. Wintersteiger
ad76e536b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-17 16:36:44 +00:00
Christoph M. Wintersteiger
b138a0f6d3 Cleaned up hacky rewriter cancelation fix in theory_fpa. 2016-11-17 16:36:39 +00:00
Christoph M. Wintersteiger
a97358965b Fixed interruption/cancelation issue in rewriter. 2016-11-17 16:28:49 +00:00
Nikolaj Bjorner
1600823435 fix perf bug reported in #790 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-17 05:38:52 +02:00
Nikolaj Bjorner
123b50ed3c Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-17 04:26:36 +02:00
Nikolaj Bjorner
e9db934f1a improving perf of mutex finding, revert semantics of 0 timeout to no-timeout. Issue #791 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-17 04:26:17 +02:00
Christoph M. Wintersteiger
9053e6eba6 Resolved merge conflicts. Added FPA API input validity checks. 2016-11-15 20:19:40 +00:00
Christoph M. Wintersteiger
58728bb7b3 Merge pull request #789 from wintersteiger/gh570-att-2 
Gh570 att 2
 2016-11-15 20:13:24 +00:00
Christoph M. Wintersteiger
dcf643f711 Merge branch 'master' of https://github.com/Z3Prover/z3 into gh570-att-2 2016-11-15 19:59:54 +00:00
Christoph M. Wintersteiger
c7787feebb Assertion fix for theory_fpa. Relates to #570. 2016-11-15 19:59:22 +00:00
Christoph M. Wintersteiger
ee60ba824f Bugfix for rewriter exceptions in theory_fpa. Relates to #570. 2016-11-15 19:59:08 +00:00