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

6277 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
c81ee05098 Fixes for .NET Core build 2016-11-02 13:36:29 +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
Christoph M. Wintersteiger
ed5137ffd2 build fix 2016-11-01 11:23:42 +00:00
Nikolaj Bjorner
84172302a2 fix bug in mutex extraction, reported by Patrick Trentin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-11-01 00:16:16 +01:00
Nikolaj Bjorner
ba942af5a8 disable sat solver when proofs are turned on. Fixes issue #768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 23:27:39 +01:00
Nikolaj Bjorner
fa1a0aa7ba remove buggy and unused equivalence relation plugin. Github issue #770 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 22:59:56 +01:00
Nikolaj Bjorner
ff75f88c4f fix memory abuse in internalization in inc-sat-solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-31 22:25:58 +01:00
Nikolaj Bjorner
596f07e548 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-28 08:27:21 -07:00
Nikolaj Bjorner
3714e520be fix performance bottlnecks: gc of literals walk through potentially huge watch-lists, avoid user-push/pop around calls to solver2tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 08:27:11 -07:00
Nikolaj Bjorner
7764148dd3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:42:27 -07:00
Nikolaj Bjorner
2475f3bff5 ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:41:27 -07:00
Nikolaj Bjorner
4d078dc0a9 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-28 07:17:49 -07:00
Christoph M. Wintersteiger
f1412d3f32 Bugfix for bouned_int2bv_solver 2016-10-28 14:23:01 +01:00
Christoph M. Wintersteiger
02e1bae9cb whitespace 2016-10-28 14:22:27 +01:00
Christoph M. Wintersteiger
6fb358a432 Build fix for libz3.vcxproj. 2016-10-28 13:45:10 +01:00
Christoph M. Wintersteiger
9c16d16bc8 removed debug output 2016-10-28 12:22:28 +01:00
Nikolaj Bjorner
ca309341c3 fixing cancellation code paths for inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 22:07:46 -07:00
Nikolaj Bjorner
b1d673e3eb catch cancellation exceptions, return undef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 16:34:26 -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
24fc19ed58 speed up consequence finding by avoiding local search whenver assumption level is reached during the initial phase 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-27 08:15:39 -07:00
Christoph M. Wintersteiger
253cfeb0af Added FPA numeral accessors/predicates to Python API 2016-10-27 15:07:34 +01:00
Christoph M. Wintersteiger
95d7b33ebb Added is_numeral_negative to .NET and Java APIs 2016-10-27 15:07:10 +01:00
Christoph M. Wintersteiger
e4f7ff9881 Added Z3_fpa_is_numeral_negative to FPA API 2016-10-27 15:06:24 +01:00
Nikolaj Bjorner
485372ec2a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-26 19:15:11 -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
Christoph M. Wintersteiger
23c58a1ef6 Added FPA numeral predicates to ML API 2016-10-26 18:53:20 +01:00
Christoph M. Wintersteiger
903d962a3c Merge branch 'fpa_numeral_accessors' of https://github.com/wintersteiger/z3 into fpa_numeral_accessors 2016-10-26 18:44:49 +01:00
Christoph M. Wintersteiger
935c523ef8 Added FPA numeral predicates to Java API 2016-10-26 18:44:35 +01:00
Christoph M. Wintersteiger
c573a7446b Added FPA numeral predicates to .NET API 2016-10-26 18:44:25 +01:00
Christoph M. Wintersteiger
bea7bc5e30 Bugfix for bv2fpa_converter. Fixes #767. 2016-10-26 16:32:44 +01:00
Christoph M. Wintersteiger
cf93e39666 Fixed FPA unbiased exponent accessors 2016-10-26 15:54:33 +01:00
Christoph M. Wintersteiger
e381cef92c Marked .NET Z3Exception as serializable 2016-10-26 15:12:10 +01:00
Christoph M. Wintersteiger
93346380e0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-26 14:08:50 +01:00
Christoph M. Wintersteiger
ead970b477 Bugfix for Python API. 
Thanks to John D. Ramsdell for reporting this issue (http://stackoverflow.com/questions/39584779/why-is-the-sort-of-a-bound-variable-forced-not-to-be-a-finite-domain-sort).
 2016-10-26 14:08:33 +01:00
Christoph M. Wintersteiger
1494c605f9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-26 12:59:49 +01:00
Christoph M. Wintersteiger
86285e1641 disabled unnecessary assertion 2016-10-26 12:59:26 +01:00
Nikolaj Bjorner
da4289fadc fix unit tests for pb 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-25 20:47:48 -07:00
Nikolaj Bjorner
d0c5b86a2a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-10-25 20:32:20 -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
Christoph M. Wintersteiger
c7fddf80c2 fixed unhandled case warning in test/qe_arith.cpp 2016-10-25 14:34:00 +01:00
Christoph M. Wintersteiger
8c5c564d6c fixed initialization order warning in pb2bv_rewriter 2016-10-25 14:31:29 +01:00
Christoph M. Wintersteiger
6ea45b4d65 fix for Python API installation 2016-10-25 14:23:55 +01:00
Christoph M. Wintersteiger
963dfad10e fix for biased flag on get_numeral_exponent_string 2016-10-25 14:17:23 +01:00
Christoph M. Wintersteiger
dc78a04135 removed debug output 2016-10-25 12:20:45 +01:00
Nikolaj Bjorner
fefd00aa49 fix sign of constant in pb constraint 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 20:28:56 -07:00
Nikolaj Bjorner
b82b53dc34 add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 17:41:52 -07:00
Nikolaj Bjorner
e4d2c5867a remove dead (and incorrect) code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-10-24 15:52:47 -07:00