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

12335 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev 4f2eb0b4eb remove an unused field 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson bc9edac913 fix in sign lemma for the zero case 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev Nachmanson abbf8c587b introduce mon_to_rooted_mon 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 14a8612779 fix a bug in order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev f57f6138b4 fix a bug in order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev fe05d1a1e8 fix the tests 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 8c876b48a7 fix the tests 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev a1851db4d5 implement order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev b948091665 implement order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 979593e2f1 create a test for order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev ea02231ef8 create a test for order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 54edea4f37 work on monotonicity lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev ad1aaebb89 proportional lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 76d516d42c proportional lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev ace8fb6d95 improve printouts and diagnostics 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 3192db64a1 Nikolaj's changes is mk_eq 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev ad98594447 disable a check 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 267457aaf4 fix a bug in factorization 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev ef87054fe0 take ast.cpp from Z3Prover master 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev cd33550f32 build fix 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 489da283bb avoid adding constantly false statements to the lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev dbfa3fc84a fix in order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 47d7331dd5 fix in neutral lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 5b786c428d avoid cleaning m_var_to_its_monomial 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 09f5ae7521 add a clear() method to nla_solver, fix a bug in abs values tables, add assertions, fix newtral lemma generation 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 0ff07aed3f add equivalence explanations 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 7c05d5e5d3 bug fix in order lemma, add more asserts 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 1c190c401b simplify order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 89c2ecbace add a test with equivalent variales for order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 70612fb109 more tests and fixes in order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 261c664654 improve the test for order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev f3f9372eac fixes after the rebase 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 98823ef8ac move some functionality from nla_solver to rooted_mons 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 00acf408bf move some functionality from nla_solver to rooted_mons 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 64a7231079 move some functionality from nla_solver to rooted_mons 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev b43a0e184c introduce rooted monomial table 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 4aa5fe1a46 cleanup 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 95ee5fa681 passing test solver::test_order_lemma() 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 5c0f76a702 fix a bug in nla_solver's divide 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev c30190f941 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 7775afdcc3 order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev fc277f5648 order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev cebee656bd order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 99e21e0977 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 28732b1def toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 254a40535e call order_lemma_on_ac_and_bd 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 4db4a8da3f toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev a5c146a740 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev 82589ad325 toward order lemma 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00
Lev f211be1e49 introduce factor 
Signed-off-by: Lev <levnach@hotmail.com>
 2020-01-28 10:04:21 -08:00