Nikolaj Bjorner
|
16aec328f1
|
add comments, fix mixup between lower/upper
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-13 13:42:50 -07:00 |
|
Nikolaj Bjorner
|
33042268b5
|
bounds propagation functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-13 13:36:22 -07:00 |
|
Murphy Berzish
|
5e7806c4a4
|
z3str3: use rational in place of unsigned during model construction
|
2020-05-13 14:32:44 -04:00 |
|
Nikolaj Bjorner
|
bda29ca26a
|
outline for monomial bound propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-13 10:37:46 -07:00 |
|
Murphy Berzish
|
3c606ea9b2
|
z3str3: disable compute_contains() and get_grounded_concats() checks
|
2020-05-13 11:53:26 -04:00 |
|
Nikolaj Bjorner
|
127ef59ce4
|
push explanation to where it is used
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 19:55:07 -07:00 |
|
Nikolaj Bjorner
|
8b546867f0
|
move lemma creation into nra_solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 19:47:29 -07:00 |
|
ahumenberger
|
d706d43712
|
Update README with infos about Julia bindings (#4298)
* Update README for Julia bindings
* Fix links in readme
* Add hash of z3_jll
* Fix typo
|
2020-05-12 19:34:47 -07:00 |
|
Lev Nachmanson
|
b2dc21b107
|
simplify the nla_solver interface (#4312)
* simplify the nla_solver interface
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* more simplifications
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* init m_use_nra_model
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 19:34:03 -07:00 |
|
Murphy Berzish
|
51beeec92f
|
z3str3: heuristics for predicates over int-to-string terms
|
2020-05-12 21:35:24 -04:00 |
|
Nikolaj Bjorner
|
7a6c66a085
|
add stubs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 17:38:16 -07:00 |
|
Nikolaj Bjorner
|
be1a1dd7c2
|
add stubs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 17:36:46 -07:00 |
|
Murphy Berzish
|
22d0dd863b
|
z3str3: properly handle the case when an int.to.str term isn't fully assigned by string/arith theories
|
2020-05-12 19:36:04 -04:00 |
|
Nikolaj Bjorner
|
32055a31db
|
pass resource limits by reference
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 10:49:16 -07:00 |
|
Nikolaj Bjorner
|
bea0d45e6a
|
disable new nlsat connection from master until debugged
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 09:38:17 -07:00 |
|
Nikolaj Bjorner
|
2953d3ed30
|
ignore my shortcut
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 09:10:40 -07:00 |
|
Nikolaj Bjorner
|
91012600ae
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-12 09:10:40 -07:00 |
|
Nikolaj Bjorner
|
dce3cbede4
|
remove incremental_linearization code
|
2020-05-12 09:10:40 -07:00 |
|
Lev Nachmanson
|
a14c2a3051
|
enable nlsat solver call from nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
6b433b54e2
|
disable the call to nlsat from nla_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
3e4a4c6df2
|
rebase with master branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
4b68d98b2a
|
work on nra to nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
8c92cf1b32
|
restore the tactics with nlsat
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
279d55a2c7
|
nra to nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
e32a6714a5
|
call nlsat
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
151397a067
|
nra to nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
dae67987b5
|
add nla_lemma.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Lev Nachmanson
|
7a79397769
|
nra to nla
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
|
2020-05-11 19:12:02 -07:00 |
|
Murphy Berzish
|
bd0180925b
|
z3str3: don't crash when finding initial bounds for a regex that has no solutions (#4276)
|
2020-05-11 17:41:55 -07:00 |
|
pjneary
|
e254e890a1
|
Fix compile error GCC 6.3.1 (#4274)
auto deduce compile error
|
2020-05-11 17:41:34 -07:00 |
|
Nikolaj Bjorner
|
1be22a80f6
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 17:20:18 -07:00 |
|
Nikolaj Bjorner
|
884a68251b
|
fix #4266
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 16:53:59 -07:00 |
|
Nikolaj Bjorner
|
754bafc95e
|
fix #4267
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 13:54:52 -07:00 |
|
Nikolaj Bjorner
|
16478b415b
|
disable order and tangent lemmas on reals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 13:46:25 -07:00 |
|
Nikolaj Bjorner
|
81b3c440ce
|
fix mixup between constraint indices and lpvar explanations fixes various newly reported unsoundness bugs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-11 13:07:28 -07:00 |
|
Nikolaj Bjorner
|
9c972521c4
|
priority code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-10 21:09:14 -07:00 |
|
Nikolaj Bjorner
|
99043399ce
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-10 20:28:35 -07:00 |
|
Nikolaj Bjorner
|
179c9c2da2
|
consolidate methods that add lemma specific information to under "new_lemma"
|
2020-05-10 18:31:57 -07:00 |
|
Nikolaj Bjorner
|
caee936af5
|
build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-10 13:42:19 -07:00 |
|
Nikolaj Bjorner
|
e74faf42ad
|
code review
|
2020-05-10 12:58:05 -07:00 |
|
Nikolaj Bjorner
|
1ecc6a21fa
|
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-10 11:21:15 -07:00 |
|
Nikolaj Bjorner
|
d774ba9da1
|
fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-10 09:57:24 -07:00 |
|
Nuno Lopes
|
6c72f39142
|
fix build
|
2020-05-10 10:35:46 +01:00 |
|
Nikolaj Bjorner
|
0a6908cd15
|
abbreviate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-09 21:54:58 -07:00 |
|
Nikolaj Bjorner
|
086331a24b
|
null
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-09 21:27:45 -07:00 |
|
Nikolaj Bjorner
|
30de76b529
|
add occurs check to other nla_basic lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-09 20:50:27 -07:00 |
|
Nikolaj Bjorner
|
4890c3ce31
|
fix #4230
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-09 18:49:00 -07:00 |
|
Nikolaj Bjorner
|
f044071f5e
|
fix #4260
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-09 18:13:12 -07:00 |
|
Nikolaj Bjorner
|
fdc87f286f
|
na (#4254)
* remove level of indirection for context and ast_manager in smt_theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add request by #4252
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move to def
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4251
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4255
* fix #4257
* add code to debug #4246
* restore new solver as default
* na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* fix #4246
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-09 17:40:02 -07:00 |
|
Nikolaj Bjorner
|
becf423c77
|
remove level of indirection for context and ast_manager in smt_theory (#4253)
* remove level of indirection for context and ast_manager in smt_theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* add request by #4252
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* move to def
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2020-05-08 16:46:03 -07:00 |
|