mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
5939 commits 24 branches 48 tags 158 MiB
Commit graph

975 commits

Author SHA1 Message Date
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
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
Nikolaj Bjorner
4d078dc0a9 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:17:49 -07:00
Nikolaj Bjorner
7d7e03e377 rewind qhead to ensure re-propagation after cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 16:23:33 -07:00
Nikolaj Bjorner
41deae52c6 fix enum2bv to handle singleton enumeration types, differentiate disequality conflicts for theories that handle disequalities vs. theories that don't 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 13:35:53 -07:00
Nikolaj Bjorner
4bd83724dd remove conflict on false disequality, introduced regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-26 19:15:05 -07:00
Nikolaj Bjorner
461e88e34c additional robustness check for incremental sat solver core when it recieves interpreted constants, added PB equality to interface and special handling of equalities to adddress performance gap documented in #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:32:13 -07:00
Nikolaj Bjorner
a880e5f49b fix incorrection assertion when checking signs of literals, exposed by miTLS regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 13:12:36 -07:00
Nikolaj Bjorner
c68c56b0e7 fix incorrect assertion when checking signs of literals, exposed by mitls regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 13:09:27 -07:00
Nikolaj Bjorner
33e7dccd42 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 09:11:02 -07:00
Nikolaj Bjorner
0439b795b4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-24 09:10:40 -07:00
Christoph M. Wintersteiger
5716eaafed whitespace 2016-10-24 12:50:05 +01:00
Nikolaj Bjorner
4f3f21bff1 disable local optimization in presence of non-linear constraints, addresses issue #758 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 21:45:35 -07:00
Nikolaj Bjorner
b92bd89a45 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:53:10 -07:00
Nikolaj Bjorner
3778048eb4 add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-23 20:31:59 -07:00
Nikolaj Bjorner
e32e0d460d fix at-most-1 constraint compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-22 21:50:45 -07:00
Nikolaj Bjorner
23b9d3ef55 fix at-most-1 constraint compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-22 18:50:16 -07:00
Nikolaj Bjorner
bb6d826908 use index j to avoid superficial, but typically flagged, name clash with internal index i 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-20 22:17:11 -07:00