mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity
13845 commits 24 branches 48 tags 158 MiB
Commit graph

987 commits

Author SHA1 Message Date
Nikolaj Bjorner
b2bfb1faea fix nla_monotone lemmas again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 17:26:54 -07:00
Lev Nachmanson
aaf05f18ab fix a bug in an simplifying interval expressions with terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-16 15:19:32 -07:00
Nikolaj Bjorner
a3f56f0d95 revert 'fix' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 12:43:26 -07:00
Nikolaj Bjorner
d352c61e01 fix regression with mainintaing signs for monotonicity lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 11:17:39 -07:00
Lev Nachmanson
cd833e892f avoid iterations on std::unordered_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-16 08:55:15 -07:00
Nikolaj Bjorner
ccda9d56d7 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 15:57:38 -07:00
Nikolaj Bjorner
90f5595067 fix order lemma bug see 30ce6f20f2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 15:38:55 -07:00
Nikolaj Bjorner
31a96b3afa review of monotonicity lemma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 15:16:46 -07:00
Lev Nachmanson
30ce6f20f2 move nla stats to nla_core 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 13:03:18 -07:00
Lev Nachmanson
01279582ff move nla stats to nla_core 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 12:58:34 -07:00
Lev Nachmanson
82fd2a062d make calling nra from nla optional 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 12:16:40 -07:00
Lev Nachmanson
08940cff8f comment out the call to nra_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 11:26:40 -07:00
Nikolaj Bjorner
9c9fe712ad disable nra in master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 10:36:53 -07:00
Nikolaj Bjorner
7e4b232ac4 fix comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-15 10:36:21 -07:00
Lev Nachmanson
6a4062809d
Nra add term (#4331) 
* n

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* do not create assumptions

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* disable nra_solver

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-15 10:35:42 -07:00
Nikolaj Bjorner
0c91109577 order lemmas on also rationals 2020-05-15 10:12:06 -07:00
Nikolaj Bjorner
146fd77e0f pretty print 2020-05-15 10:12:06 -07:00
Nikolaj Bjorner
b43ed70874 extend monomial bounds to handle powers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-14 19:13:17 -07:00
Nikolaj Bjorner
4e51633e6f adding monomial bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 18:45:47 -07:00
Lev Nachmanson
bdecbe4ed7 remove a duplicate method 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-13 15:38:20 -07:00
Nikolaj Bjorner
fff1426556 remove unreferenced label 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 13:54:47 -07:00
Lev Nachmanson
6b28973799
nla review (#4321) 
* 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>

* work on NSB comments

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* work on NSB comments

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 13:52:42 -07:00
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
Nikolaj Bjorner
bda29ca26a outline for monomial bound propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 10:37:46 -07: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
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
Nikolaj Bjorner
be1a1dd7c2 add stubs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-12 17:36:46 -07: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
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
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
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
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
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