mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity
5855 commits 23 branches 48 tags 157 MiB
Commit graph

955 commits

Author SHA1 Message Date
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
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
Nikolaj Bjorner 9cd7b9b4f6 fix mutex finding for smt-core: it was returning mutexes for negations of literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-20 22:13:23 -07:00
Nikolaj Bjorner ef9486913b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-19 08:57:16 -07:00
Nikolaj Bjorner 527980e440 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-19 08:57:10 -07:00
Christoph M. Wintersteiger 948bf9540f Fix for previous commit. 2016-10-19 12:07:33 +01:00
Christoph M. Wintersteiger 11997afb5d Fixed potential problems with invalidated iterators. 2016-10-19 12:00:34 +01:00
Nikolaj Bjorner 881e82e3fa remove legacy interface to dt2bv tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-18 23:04:17 -04:00
Christoph M. Wintersteiger 4546915238 Fixed iterator invalidation bug in theory_arith_nl. 
Indirectly relates to #740
 2016-10-18 17:17:19 +01:00
Christoph M. Wintersteiger 9fef51553c Whitespace 2016-10-18 17:15:43 +01:00
Nikolaj Bjorner 948a1e600e undo breaking commit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-18 10:27:47 -04:00
Nikolaj Bjorner 4cae91b096 spacing, unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-17 08:07:23 -04:00
Nikolaj Bjorner 4fda2adec8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-16 15:46:50 -04:00
Nikolaj Bjorner 58198d7cb6 add consequence finding to inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-16 15:45:39 -04:00
Christoph M. Wintersteiger 009af4455d Refactored and fixed model conversion for fpa2bv conversion of unspecified values via theory_fpa. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger 7e705a2d32 Bug fixes for underspecified FP operations. 2016-10-15 18:35:39 +02:00
Christoph M. Wintersteiger bc257211d6 Whitespace 2016-10-15 18:35:39 +02:00
Nikolaj Bjorner 8d2b70a5e2 better encodings for at-most-1, #755 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-10 23:46:03 -07:00
Nikolaj Bjorner 476b06fa14 fix compiler warnings, gcc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-28 16:42:07 -07:00
Nikolaj Bjorner 77b245b3d8 fix proof production to avoid crash. Issue #733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-17 17:29:19 -07:00
Nikolaj Bjorner 1450594fc6 add patch to deal with bug exposed in issue #721 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 12:15:49 -07:00
Nikolaj Bjorner 2f67665c7e ensure stoi axiom even when no value is present for argument. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:40:21 -07:00