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

991 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
856cf7d4f9 fix generation of fresh constants for uninterpreted sort in EPR, Issue #649 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-04 15:51:35 +00:00
Nikolaj Bjorner
be9d5c7088 fix evaluator for array store expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-02 21:33:24 +00:00
Nikolaj Bjorner
f61600d1d8 fixing unsat core extraction for tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-02 14:14:55 +00:00
Nikolaj Bjorner
46c4fdaae5 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-11-01 18:39:00 +01:00
Nikolaj Bjorner
305e080239 enable unsat core extraction in nlsat_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-01 17:57:28 +01:00
Christoph M. Wintersteiger
026309a325 bugfix for disequality propagation in smt_context 2016-11-01 14:21:06 +00:00
Nikolaj Bjorner
7764148dd3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:42:27 -07:00