mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
6006 commits 23 branches 48 tags 157 MiB
Commit graph

998 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
2458db30cf Corner-case fix for smt::solver::pop_core 2017-01-12 12:49:26 +00:00
Christoph M. Wintersteiger
650ea7b9cc Bugfix for smt.core.extend_patterns 2017-01-11 18:40:11 +00:00
Christoph M. Wintersteiger
384468bc99 Added option to extend unsat cores with literals that (potentially) provide quantifier instances. 2017-01-10 20:22:20 +00:00
Christoph M. Wintersteiger
ba9d36605b Formatting, whitespace 2017-01-10 20:22:20 +00:00
Christoph M. Wintersteiger
8047f0d91a GCC compilation/keyword fix. Relates to #864 2017-01-10 14:06:56 +00:00
Nikolaj Bjorner
8d09b6e4a8 add at-least and pbge to API, fix for issue #864 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-01-09 21:23:00 -08:00
Nikolaj Bjorner
a4d5c4a00a make get_consequence call skip check-sat if a model is already there 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-30 18:05:19 -08:00
Nikolaj Bjorner
8dde60f634 initialize watch in assign_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-26 10:18:55 -08:00
Nikolaj Bjorner
2bd29548da improve parser error message over API, streamline names of statistics for arithmetic solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-25 17:27:56 -08:00
Nikolaj Bjorner
46df31babf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-22 20:54:14 -08:00
Nikolaj Bjorner
1787fa8296 remove redundant disjunction in compilation of at-most-1 constraints, log mutexes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 20:54:09 -08:00
Nikolaj Bjorner
a444a33c30 updated encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-22 17:45:21 -08:00
Nikolaj Bjorner
f52baf1e17 fix build again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:48:43 -08:00
Nikolaj Bjorner
4bcf1bf2f6 fix debug build, unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:44:49 -08:00
Nikolaj Bjorner
df492e200f merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 10:04:02 -08:00
Nikolaj Bjorner
8d18fd075e remove sources for unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-21 09:54:45 -08:00
Nikolaj Bjorner
c1480b4389 handle model generation from issue #748. Deal with warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-12 00:40:52 +01:00
Nikolaj Bjorner
dea3b8ddf7 address warnings from #836 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 13:14:36 +01:00
Nikolaj Bjorner
fe10f2d244 address #835 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-10 07:51:16 +01:00
Christoph M. Wintersteiger
4c664f1c05 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:03:36 +00:00
Christoph M. Wintersteiger
16b32ecf12 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.

(+reversed accidental debug code commit).
 2016-12-09 15:03:31 +00:00
Nikolaj Bjorner
a17e957362 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-12-09 15:32:26 +01:00
Nikolaj Bjorner
acba529bce fix bug in encoding of axioms for indexof. Issue #806 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-12-09 15:32:15 +01:00
Christoph M. Wintersteiger
56b1a8b086 Bugfix for special-case handling in fp.fma. 
Thanks to Florian Schanda for reporting this bug.
 2016-12-09 13:43:05 +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
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
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
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
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
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
b138a0f6d3 Cleaned up hacky rewriter cancelation fix in theory_fpa. 2016-11-17 16:36:39 +00: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
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
Nikolaj Bjorner
e65d80dedd make semantics of extract/substr deterministic. Issue #781 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-15 18:29:51 +02:00
Nikolaj Bjorner
fa8427258a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-15 15:07:15 +02:00
Nikolaj Bjorner
e21bd8dacc fix lexicographic combinations for wmax: pb constrsaints were not interpreted in Boolean benchmarks. #782 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-15 15:07:05 +02:00
Christoph M. Wintersteiger
6204f67d38 Fixed problems with aborted rewriters in theory_fpa. Relates to #570. 2016-11-14 17:40:09 +00:00
Christoph M. Wintersteiger
5ef7d38d72 Whitespace 2016-11-05 14:39:23 +00:00
Christoph M. Wintersteiger
50c323dc74 Whitespace 2016-11-05 14:35:56 +00:00
Nikolaj Bjorner
caf0a1e80d fix breaking change to theory-seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-05 07:22:27 +00:00
Nikolaj Bjorner
152321bce6 fix crash in poly normalizer exposed by qe. Issue #775 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 20:29:12 +00:00