mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
13385 commits 23 branches 48 tags 157 MiB
Commit graph

11221 commits

Author SHA1 Message Date
Lev Nachmanson cf0952c232 roll back in maximize_term if the integrality is broken 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 17:59:45 -07:00
Nikolaj Bjorner f21b60a6e1 remove output from normalize bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 17:46:53 -07:00
Nikolaj Bjorner e2cab00b1b fix #3583 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 17:37:57 -07:00
Nikolaj Bjorner 48581eb7ab fix #3598, feature overload abuse 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 17:29:02 -07:00
Nikolaj Bjorner 296e56c28f fix #3575 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 17:26:43 -07:00
Nikolaj Bjorner 03d7a9acff #3581, bail out when smt solver gives up 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 17:19:57 -07:00
Nikolaj Bjorner 330b3cc8d6 fix #3584 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 16:50:53 -07:00
Nikolaj Bjorner 7f8738dd85 fix #3542 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 16:24:47 -07:00
Lev Nachmanson 3e845010dd replace v by j in lp printouts 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 15:59:03 -07:00
Nikolaj Bjorner a6e7ed039c fix #3587 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 15:18:37 -07:00
Nikolaj Bjorner 8a961a5ce9 fix #3554 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 15:02:55 -07:00
Nikolaj Bjorner 0ca5f59e35 fix #3550 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:45:38 -07:00
Nikolaj Bjorner fe81de6d39 fix #3555 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:37:38 -07:00
Nikolaj Bjorner b9dd18483c fix #3571 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:11:36 -07:00
Nikolaj Bjorner d4aa850412 fix #3572 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:09:47 -07:00
Nikolaj Bjorner e263f9b238 fix #3559 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 14:00:30 -07:00
Nikolaj Bjorner de2ad26826 fix #3568 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:51:45 -07:00
Nikolaj Bjorner 04e51ffcb5 fix #3569 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:40:59 -07:00
Nikolaj Bjorner 53b5ca3c2b disambiguate call 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:35:40 -07:00
Nikolaj Bjorner 5152c9500d fix #3591 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 13:08:58 -07:00
Nikolaj Bjorner bf9779cb87 fix #3593 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 12:46:18 -07:00
Nikolaj Bjorner aeee44398d fix #3594 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 12:40:24 -07:00
Lev Nachmanson 7936df8e0b pass std::function as const aliases 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-30 12:20:47 -07:00
Nikolaj Bjorner ba4765f16f debugging #3511 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner f74079de01 fix #3529 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner c142f99127 fix #3532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner 0b10cb3312 fix #3528 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Lev Nachmanson 9be7bda69a fix a bug in column patching 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson 7a950dd667 patch reals 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Lev Nachmanson 3237bd9243 better tracing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-29 15:03:46 -07:00
Nikolaj Bjorner 7086a7c26a fix #3531 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 11:15:01 -07:00
Nikolaj Bjorner 1155db383e fix #3540 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 10:55:47 -07:00
Nikolaj Bjorner 9f386306ef na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 10:55:47 -07:00
Nikolaj Bjorner 1a995da0ae fix #3538, turn on proof checking assertions in goal.cpp for earlier coverage 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 10:55:47 -07:00
Lev Nachmanson 907d310600 get rid of arith.nla parameter 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 14:33:40 -07:00
Lev Nachmanson f9151a7a8e correct the default options: smt.arith.nla=False 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-27 13:55:23 -07:00
Nikolaj Bjorner 4b7bd3a881 fix #3536 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-27 12:59:24 -07:00
Nikolaj Bjorner f8dcaa8885 'na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-27 10:23:00 -07:00
Lev Nachmanson 352f4b5b37 use u_set in random_update() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-26 18:11:32 -07:00
Nikolaj Bjorner 12f62e73d5 fix ordering of delayed assume eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 16:24:34 -07:00
Nikolaj Bjorner 7a04e52c41 fix ordering of delayed assume eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 16:22:24 -07:00
Nikolaj Bjorner 499843ae7f remove verbose 0 output, #3527 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 14:49:14 -07:00
Arie Gurfinkel 5673ec046b qe_term_graph fix for #3526 2020-03-26 16:45:06 -04:00
Nikolaj Bjorner d4699b181d fix assertion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 12:49:44 -07:00
Nikolaj Bjorner 73ab95d338 remove canonize in seq solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 12:47:30 -07:00
Nikolaj Bjorner 0fa04179d0 fix #3522 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 11:06:04 -07:00
Nikolaj Bjorner 5da2169a0e fix #3524 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 10:38:13 -07:00
Nikolaj Bjorner ee2e81b696 fix #3517 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 10:02:41 -07:00
Nikolaj Bjorner 493671aa72 fix #3520 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:58:06 -07:00
Nikolaj Bjorner 868a6b3594 fix #3521 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Nikolaj Bjorner 37f080b877 fix #3523 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Nikolaj Bjorner c165f69248 fix #3525 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Lev Nachmanson fd219abe8c fix test build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b34f841421 setting the old defaul options for nla 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson f5b62015fc change the return type of ival.var() to tv 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 119a491b17 tracking stats for max columns in theore_arith_core.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 96cc58f67c instrument the tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 09467ba677 restore some class names by replacing u_set to int_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner ab34ef9daf fix crash exposed by #3503 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson ea964e5c3b rename int_set to u_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson bc5b68b16e convert term indices to columns in lar_solver::add_equality() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson e2538afd32 better diagnostics in lar_solver and more efficient int_set::resize() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 50db22b2b2 fix #3407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 98dfb1ba86 get rid of m_resize_buffer 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 2975873b91 ensure encapsulation boundaries 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner eac5070a2e remove stdout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson c16d90307b more careful resize in int_set 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 0ec12f497c reduce use of m_core as attribute reference, instead pass as parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 6b9e1e936d correcting invariant, fix #3482 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson e0b95979e6 detect the status change in lar_solver::add_equality() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner ee8aa50750 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner e16c62d6e2 don't reset core after it has been populated for the cut #3451 and presumably other bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 38eca3b66a fixes in order lemmas and printing terms 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 4b8a063996 convert seg fault to assertion violation #3456 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b964976b3f remove debug code from theory_lra.cpp and restore gomory.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 8a665e25ed reverting signed mon_eq, try to rely on canonization state during add/pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 6877840342 port from master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner cc74dd6373 emonics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 316f2194e0 rename 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b52150de22 cleanup 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner c88d5e6468 remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 2b98c7e157 tidy^2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 2e2c42f7c8 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 49ac118a18 tidy tv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner e50082b484 add tv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson d758a08497 do not create inf var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 6c5d7fbe96 fixes in max term with tableau 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner b14f5aab83 fix #3393 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 45980694b7 fetch explanations earlier than setting the bound 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 146489ff14 fix the signs for factorns in tangent lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 4c5c17c7d8 fixes for #3376 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 51ffaae396 fix build of tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner eb0f318686 fix #3361 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 46c6a5492e fix assertion in emonics, exposed by #3318 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson c2e7dd3378 catch the possible infeasible column when adding an equality 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 562be531e9 fix #3317 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson a6941a3e75 accept terms indices in core::explain_coeff_upper_bound() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 687c487746 accept terms indices in core::explain_coeff_upper_bound() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 4683c3f241 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 4dfc0d6d88 fix #3334 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner af4e1fa010 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner b41b83cd63 fix #3314 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner e7960e63da fix #3298 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner d3a7ebee02 fix #3338 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 31e2a9b163 add scoping for variable equivalences between new monomials 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 919f687df6 expose settings, not all of core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 56584922e9 if it isn't used, it isn't templatized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner e8c3324c3f reduce number of redundant arguments and pointers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 44d2f6da6c fix #3261 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 8af245a410 use a simpler encoding for term indices 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 1c0e583abc avoid calling del on memory not owned by object allocator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 0b785cc942 track variables used by nla_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 31937f0b91 round the bound for columns and terms when it can be deduced that they are integral 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 79d4d13b14 fix in gomory: revert some changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 29b9dfe326 fix in gomory cut 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 4917475f9e remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 8dcec5c4ad add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson dcb81f0ad2 introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 5556b82989 introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson fc62ecb8d1 relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson c284e153f3 fix in gomory: revert some changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 91d9a5bc83 fix in gomory cut 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 1b92400801 remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 3b10318183 add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 981aafa59c introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 5dbe4a6c8b introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson a80b48a597 relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 252eb5e856 remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson db94109827 add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson f9f1960c73 introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson d39d64176e introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 84933c4435 relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 3224febd0e remove double shrink 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner c68d15f441 build of template 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 1aaf6d879f use same interval manager in pdd_interval as caller 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner f76432933f avoid calling del on memory not owned by object allocator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner abc4c5962b fix #3269 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner f1f974638d track variables used by nla_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner a7158772ad move to scoped intervals for memory management 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 79fefe5fb3 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 906d52ca1c accept term indices as columns in some lar_solver queries 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner f43f1629cf fix #3273 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson f28c80e3b1 reorder fields in lar_solver constructor to avoid a warning 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner b67d136849 hide flag on registering variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 3e84d04719 fix internalize for multiplication #3119 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 846a9fc25f consistent 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 26631ce38d add a unit test for monics, plus some cosmetic changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 0207878f5f fix #3183 - change relevancy propagation to ensure that div/mod axioms are picked up 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 1e9013fe6d cleanup in var_register 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 719603f185 register inner terms with null var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson a0251ac745 do not register equality terms created in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 285ff9540d make sure that the term external index has not been used 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner f00c026272 fix #3173 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner 0f779c9c0d fix #3185 - move handling of to_real within def conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson f636a481d3 fixes in bound setting in cube, and in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson a80eb13420 fixes in bound setting in cube, and in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 9cce01e632 fix in order lemma 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 6ea0bcb454 round the bound for columns and terms when it can be deduced that they are integral 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b403b96d38 remove an assert 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 77ca63db90 fix in gomory: revert some changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson cbefa8d2b0 fix in gomory cut 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson fad08454c1 remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 2b4de6ebbc add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 59a82a4482 introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson bf885bf9b3 introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 28c057fd7b relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 2ad94026a0 do not produce proportional lemma for non-integral vars 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 0ee541204f fix in gomory: revert some changes 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b8d7af59f4 fix in gomory cut 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 6396857ee2 remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 87f80ce022 add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 8e55a77ee7 introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 406bd98a39 introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 3e4720abbd relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 0229ab2811 remove debug code 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 66dd93a035 fix a bug in nla_intervals - add explanations when getting intervals from a term 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson ab92c20106 add option branch_flip to lp_settings 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson b9bfa950f6 introduce a bug int theory_array.cpp - look for a counter example 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 37c72b71f5 introduce a bug into theory_array - looking for a counterexample 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson c0b49e95c4 use lar_solver directly to compare variable values in assume_eqs() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 6549984dd4 call init_variable_values() from assume_eqs 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson c469ea2717 do not call get_model() from assume_eqs() 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 0db112ef8f Update nla_core.cpp 2020-03-25 19:43:55 -07:00
Lev Nachmanson 697fd37d26 relax the literal check in theory_lra 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Lev Nachmanson 762f265616 merge with master 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-03-25 19:43:55 -07:00
Nikolaj Bjorner cf86e6ef73 disable dubious eq adapter code causing perf hit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 16:41:01 -07:00
Nikolaj Bjorner 73d73e6c95 enhance rewriting for indexof based on #3516 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 13:29:36 -07:00
Nikolaj Bjorner f92050c7e5 fix #3515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 13:21:02 -07:00
Nikolaj Bjorner 145ec8f248 pick up log configuration consistently #3513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 10:51:55 -07:00
Nikolaj Bjorner e5e6f481f9 update bounds and assert values during initialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 04:05:58 -07:00
Nikolaj Bjorner 477fd3fba0 remove model initialization all-together because assumption literals are not connected with model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 04:00:21 -07:00
Nikolaj Bjorner a7495876fd fix #3506 fix #3505 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 03:06:02 -07:00
Nikolaj Bjorner 504a7550b3 fix #3509 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 02:42:30 -07:00
Nikolaj Bjorner ea396a008a fix #3504 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 02:30:51 -07:00
Nikolaj Bjorner 0609408fd7 fix #3510 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 01:50:30 -07:00
Nikolaj Bjorner b8c25ac20b fix #2909 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 01:43:20 -07:00
Nikolaj Bjorner 41c68d64d4 avoid deref on null 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-24 17:06:06 -07:00
Nikolaj Bjorner 69783db5e8 print roots as part of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-24 15:28:51 -07:00
Nikolaj Bjorner af51d98a32 avoid unintialized value build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-24 15:02:31 -07:00
Nikolaj Bjorner a557913307 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-24 12:45:16 -07:00