mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
4171 commits 49 branches 53 tags 182 MiB
Commit graph

4171 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
6d8daacdec fix check for satisfiability before calling final_check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 08:35:05 -07:00
Christoph M. Wintersteiger
6191c3ff6e Bugfix (codeplex issue 132). Thanks to George Karpenov for catching this one! 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-10-06 13:46:55 +01:00
Nikolaj Bjorner
7ef1e8a3de turn friends into inliers to respect namespace for non-operator friends. Operaor friends will stil be in file scope so do not take name-space qualifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 19:04:15 -07:00
Nikolaj Bjorner
18e77bd539 fix qe for undef scenarios, codeplex issue 130 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 18:36:15 -07:00
Nikolaj Bjorner
0ccd56b847 fix qe on undef 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 18:33:20 -07:00
Nikolaj Bjorner
c6683fd6fa to fix that timeout of 0 has different interpretations across platforms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 12:27:57 -07:00
Nikolaj Bjorner
cbf470422e remove extra verbose output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 12:10:23 -07:00
Nikolaj Bjorner
4e55f04942 use more efficient encoding of shift operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 10:41:37 -07:00
Nikolaj Bjorner
c706e91019 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 10:37:55 -07:00
Nikolaj Bjorner
db20b2502d try qx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-04 19:50:42 -07:00
Ken McMillan
ec48f6d129 working on transforms for duality 2014-10-04 19:07:14 -07:00
Nikolaj Bjorner
6a3f75822d fix format bug (issue 126) and smaller nits in sat solver (const annotation, disable elimination of external or already elimianted variables) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-04 18:35:18 -07:00
Ken McMillan
e8985ff33d working on transforms in duality 2014-10-04 17:17:33 -07:00
Ken McMillan
16445569f1 fix for quantifier abstraction 2014-10-04 16:31:01 -07:00
Nikolaj Bjorner
f3d2535b46 another unit test for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-03 16:58:46 -07:00
Nikolaj Bjorner
2bf0b5f33f include selected deprecated facilities for easier experimentation with consequence finding over .NET 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-03 13:05:54 -07:00
Nikolaj Bjorner
fbb01f3699 prevent usage that mixes E/e notation with division / for numerals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 23:58:52 -07:00
Nikolaj Bjorner
cb88968588 tuning maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 17:10:51 -07:00
Nikolaj Bjorner
4a286cfd1e fix two bugs in logarithmic shift operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 16:02:40 -07:00
Nikolaj Bjorner
47b81d2ec0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-02 14:33:55 -07:00
Nikolaj Bjorner
d03a4bc306 check cancel flag after bcp. BCP returns in incomplete state after it check's the cancel flag. Propagate returns 'true' in this case so that the main loop exits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 14:33:42 -07:00
Nikolaj Bjorner
93a757f45b add two failing test cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 10:38:43 -07:00
Nikolaj Bjorner
2c70e8d79f port logarithmic encoding to shr, add review comment on rotate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 09:41:53 -07:00
Nikolaj Bjorner
8929c578c1 fix bug in mk_shl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 09:29:49 -07:00
Nikolaj Bjorner
928fc550a5 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-10-02 09:07:53 -07:00
Nikolaj Bjorner
504709f0a1 change implementation of shl to use log(n)*n intermediary bits instead of n^2/2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 09:07:39 -07:00
Nuno Lopes
e778f3e65b DoC: fix bug in insertion when inserting an element equal to on on the disjunction already 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-02 12:49:38 +01:00
Nuno Lopes
7d599fa047 DoC: fix bug I previously introduced in insert 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-02 11:54:53 +01:00
Nuno Lopes
9828b26379 DoC: fix slow path of filter_by_negation when columns are repeated in tgt relation 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-02 09:56:06 +01:00
Ken McMillan
d54d758f45 getting duality to recover from incompleteness-related failures by restarting 2014-10-01 18:16:21 -07:00
Ken McMillan
c5f17df310 fixing an assert caused by previous change in theory_array_base.cpp 2014-10-01 18:15:33 -07:00
Nikolaj Bjorner
bb15ddbf15 update unit tests to use filter_by_negation verifier from check_relation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 15:21:42 -07:00
Nikolaj Bjorner
d8e62cac94 enable flattening even if som is set by default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 14:51:14 -07:00
Nikolaj Bjorner
985e48c66a Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-10-01 13:49:36 -07:00
Nikolaj Bjorner
0b1c180808 fix lexicographic product for MaxSMT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 13:49:23 -07:00
Nikolaj Bjorner
0914748184 revert changes to tactic.cpp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 12:56:00 -07:00
Nikolaj Bjorner
cce287eed1 fix bug in Shannon decomposition for translating PB constraints into formulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 12:51:40 -07:00
Nuno Lopes
04b5d436b3 DoC: fix fast path of filter_negated 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-01 18:03:59 +01:00
Nuno Lopes
5211e9aa1a DoC: compact result of subtract 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-01 17:10:35 +01:00
Nuno Lopes
cbe23c428f fix build of unit tests 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-01 16:08:44 +01:00
Ken McMillan
301cb51bbb added restarts options to duality (plus some other disabled features) 2014-09-30 12:42:30 -07:00
Ken McMillan
4763532501 adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP) 2014-09-30 11:25:47 -07:00
Ken McMillan
4c71e9479d optimizing array final check 2014-09-30 11:21:34 -07:00
Nuno Lopes
115ab12ade DoC: code cleanups 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 17:16:14 +01:00
Nuno Lopes
8d1177bf3f DoC: compact result of substract and maintain invariant 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 16:24:59 +01:00
Nuno Lopes
1606359dc9 DoC: add slow path to emptiness detection that uses SMT solving 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 15:58:38 +01:00
Nuno Lopes
938a5adafa DoC: make fold_neg detect empty TBVs 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 13:00:29 +01:00
Nuno Lopes
5176cbeefb fix printing of TBVs 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 11:26:49 +01:00
Nikolaj Bjorner
83a0611cb9 adding option to selectively enable bcd 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-29 22:15:24 -07:00
Nikolaj Bjorner
60d7872cc8 adding simple BCE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-29 18:00:34 -07:00