mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity
14084 commits 24 branches 48 tags 158 MiB
Commit graph

170 commits

Author SHA1 Message Date
Lev Nachmanson
110ab5e6ef debug cheap_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-06-12 22:11:11 -07:00
Nikolaj Bjorner
2613f74baa fix #4494 2020-06-11 00:05:19 -07:00
Lev Nachmanson
c967b4aead more efficient patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
c355ee025a fix bugs in patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
e7bb8e57cb fixes in patch blocking 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
91d9b0319e toward full patching in nl 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
c58bd3105b adding more aggressive patching in nl 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
6a5579341d add restore_patched_values 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
47d5515b78 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
2de79be31b change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
b84585beeb more aggressive patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
2710afbea1 change try_patch to a template 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Lev Nachmanson
18016a7100 rename 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-31 20:20:49 -07:00
Nikolaj Bjorner
ea1f50b77e simplify extended contains patterns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-28 19:11:29 -07:00
Lev Nachmanson
caa384f6c9 make m_inf_set private and cosmetic improvements in nla patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-26 12:44:47 -07:00
Lev Nachmanson
bfd2407e0f
Debug (#4415) 
* fix it explanation.h

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

* fix explanation.h

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

* add options to run bound propagation on monomials etc.

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-21 09:55:01 -07:00
Lev Nachmanson
af2f74c05f
smarter explanation.h (#4385) 
* smarter explanation.h

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

* clean explanation API

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

* suppress warnings

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

* disable the warnings

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-19 12:38:44 -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
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
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
146fd77e0f pretty print 2020-05-15 10:12:06 -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
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
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
e32a6714a5 call nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-11 19:12:02 -07:00
Nikolaj Bjorner
1be22a80f6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-11 17:20:18 -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
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
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
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
Lev Nachmanson
a34c5a9450 bail out on big rational numbers in nla monotone lemmas 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-05-04 14:21:48 -07:00
Lev Nachmanson
8921ed56b5 fix a bug in Horner heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-23 15:58:53 -07:00
Lev Nachmanson
5208b64a6b expose only necessary methods of lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-16 12:58:39 -07:00
Nikolaj Bjorner
21a31fcd26 add missing fixed propagations on negated integer inequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-11 02:28:38 -07:00
Lev Nachmanson
29a857e258 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-04-06 17:31:56 -07:00