Nikolaj Bjorner
|
19d4b0a97a
|
resolve conflicts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-02 10:38:37 -07:00 |
|
Nikolaj Bjorner
|
538411c67f
|
remove dependencies on fd_tactic.h
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-01 15:03:34 -07:00 |
|
Nikolaj Bjorner
|
4e65c13726
|
adding lookahead and lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-06-01 14:49:54 -07:00 |
|
Christoph M. Wintersteiger
|
a7d5bb7b36
|
Tabs
|
2017-05-31 12:18:00 +01:00 |
|
Nikolaj Bjorner
|
7d245be4e1
|
enable exposing internal solver state on interrupted solvers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-30 17:33:27 -07:00 |
|
Nikolaj Bjorner
|
f698efa403
|
Merge branch 'master' of https://github.com/z3prover/z3 into opt
|
2017-05-22 12:59:36 -07:00 |
|
Nikolaj Bjorner
|
d1fec7c029
|
bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-21 15:39:05 -07:00 |
|
Nikolaj Bjorner
|
29a49f4427
|
convert static random fields to non-static
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-11 16:46:07 -07:00 |
|
Nikolaj Bjorner
|
9b3e2a9afe
|
re-enable LRA after fixing dispatch for LRA in smt-setup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-11 09:16:07 -07:00 |
|
Nikolaj Bjorner
|
b915f78281
|
merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-07 17:05:57 -07:00 |
|
Nikolaj Bjorner
|
d14f2af5ae
|
deal with subtraction that manages to sneak in. Issue #996
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-05-01 15:22:06 -07:00 |
|
Nikolaj Bjorner
|
8205b45839
|
initial integration of opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-04-27 19:13:00 -07:00 |
|
Nikolaj Bjorner
|
67513a2cf5
|
fix detection of bounds under conjunctions. Issue #971
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-04-11 07:40:09 +08:00 |
|
Christoph M. Wintersteiger
|
27a1758857
|
Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body.
|
2017-04-07 21:19:20 +01:00 |
|
Nikolaj Bjorner
|
05c5b3b07b
|
merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-03-09 22:45:52 +01:00 |
|
Nikolaj Bjorner
|
5f5819f029
|
fix xor handling, and defaults for cardinality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-03-09 22:44:41 +01:00 |
|
Nikolaj Bjorner
|
29969648ba
|
check that formulas are in lira before invoking qsat. Issue #919
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-03-09 05:52:46 +01:00 |
|
Nikolaj Bjorner
|
fcda4cee9f
|
ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-03-09 05:29:56 +01:00 |
|
Nikolaj Bjorner
|
899843b7cd
|
fix unhandled finite domain sort rewrite case. Issue #918
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-26 17:20:54 -08:00 |
|
Nikolaj Bjorner
|
e9b49644b2
|
Merge branch 'master' of https://github.com/z3prover/z3 into opt
|
2017-02-25 16:20:33 -08:00 |
|
Nikolaj Bjorner
|
e02160c674
|
expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-24 11:07:40 -08:00 |
|
Nikolaj Bjorner
|
4220432ac3
|
Merge branch 'master' of https://github.com/z3prover/z3 into opt
|
2017-02-11 11:57:47 -05:00 |
|
Nikolaj Bjorner
|
b6b6035cfb
|
tuning and fixing drat checker
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-07 16:50:39 -08:00 |
|
Christoph M. Wintersteiger
|
e4411265ea
|
Fixed model-converter segfault in ::check_sat. Relates to #881
|
2017-02-05 17:53:44 +00:00 |
|
Christoph M. Wintersteiger
|
54280b6cc5
|
Fixed model-converter segfault in ::check_sat. Relates to #881
|
2017-02-05 17:20:45 +00:00 |
|
Christoph M. Wintersteiger
|
d6b4e99489
|
Fixed signed/unsigned warnings
|
2017-02-05 16:03:00 +00:00 |
|
Christoph M. Wintersteiger
|
5682c43604
|
Merge pull request #881 from dwoos/tactic-labels
Thread labels through tactic system
|
2017-02-04 20:37:11 +00:00 |
|
Christoph M. Wintersteiger
|
c56edc63d2
|
Merge pull request #882 from dwoos/sine-filter
Add basic Sine Qua Non filtering
|
2017-02-04 20:24:09 +00:00 |
|
Doug Woos
|
d6fbfe401e
|
add and use new is_pattern recognizer
|
2017-02-01 16:21:15 -08:00 |
|
Doug Woos
|
44c417904b
|
correctly pretty-print
|
2017-02-01 16:21:01 -08:00 |
|
Doug Woos
|
a147e2bc35
|
use is_uninterp
|
2017-02-01 16:20:40 -08:00 |
|
Nikolaj Bjorner
|
40177f7bac
|
bypass combined solver when logic is set to QF_FD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-01 08:05:04 -08:00 |
|
Nikolaj Bjorner
|
4d8d705b3f
|
bypass combined solver when logic is set to QF_BV or QF_FD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-02-01 08:02:24 -08:00 |
|
Doug Woos
|
d9e43f0e6d
|
use insert_if_not_there
|
2017-01-31 11:48:52 -08:00 |
|
Doug Woos
|
89ba99918e
|
reindent
|
2017-01-31 11:48:52 -08:00 |
|
Doug Woos
|
c0bb6dd2be
|
delete unused args
|
2017-01-31 11:48:51 -08:00 |
|
Doug Woos
|
da63f6b0ff
|
delete comment
|
2017-01-31 11:48:51 -08:00 |
|
Doug Woos
|
b00c4d2e64
|
add name
|
2017-01-31 11:48:51 -08:00 |
|
Doug Woos
|
8196173e29
|
Introduce and use labels_vec
|
2017-01-30 15:50:34 -08:00 |
|
Doug Woos
|
3791810920
|
add const &
|
2017-01-30 15:09:57 -08:00 |
|
Nikolaj Bjorner
|
37ee4c95c3
|
adding parallel threads
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2017-01-30 02:09:08 -08:00 |
|
Doug Woos
|
a9d61d48ae
|
Add basic Sine Qua Non filtering
|
2017-01-27 11:22:39 -08:00 |
|
Doug Woos
|
5796e15088
|
Thread labels through tactic system
|
2017-01-27 11:07:13 -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
|
20790c46ee
|
bail out on failure to properly project
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-11 04:23:07 +01:00 |
|
Nikolaj Bjorner
|
fe10f2d244
|
address #835
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-10 07:51:16 +01:00 |
|
Nikolaj Bjorner
|
e092232f67
|
add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2016-12-09 23:17:52 +01:00 |
|
Nuno Lopes
|
dedae29300
|
add a few more statics to avoid symbol clashes
|
2016-12-01 17:37:07 +00:00 |
|
Nuno Lopes
|
42b26c63e5
|
make a few functions static
|
2016-12-01 14:01:20 +00:00 |
|