3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Commit graph

18017 commits

Author SHA1 Message Date
Lev Nachmanson d77c91b1aa trying to get else on a new line
with clang-formatter
2023-09-19 15:46:59 -07:00
Lev Nachmanson c5cfd62e0a remove dead code related to nla unit propagation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-19 10:56:09 -07:00
Lev Nachmanson cf63e75898 using structures from util in lp_bound_propagator
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-18 13:25:24 -07:00
Lev Nachmanson af8d192392 add an include 2023-09-17 13:14:36 -07:00
Lev Nachmanson 10095a30b7 add an include file 2023-09-17 12:25:11 -07:00
Lev Nachmanson 66f6a0327f change type of m_ibounds to std::vector 2023-09-17 11:00:48 -07:00
Lev Nachmanson 30b743d7b3 refactor propagat_monic 2023-09-17 10:45:54 -07:00
Lev Nachmanson 7353d7fb4d fix dep calculations in lp_bound_propagator 2023-09-17 06:48:12 -07:00
Lev Nachmanson 77e56b0a69 debug 2023-09-16 13:54:14 -07:00
Lev Nachmanson c240f62ca8 is_linear does not check for is_big 2023-09-15 17:44:10 -07:00
Lev Nachmanson b621c9fa1c remove an extrac check in bound_is_interesting 2023-09-15 17:42:18 -07:00
Lev Nachmanson 4cfba9787b debug lp_bound_propagator 2023-09-15 17:41:10 -07:00
Lev Nachmanson 762ade2a79 check m_unassigned_bounds in bound_is_interesting 2023-09-15 06:15:22 -07:00
Lev Nachmanson a55aa1a648 add a comment 2023-09-14 19:29:48 -07:00
Lev Nachmanson b3673d491e fix the build for gcc 2023-09-14 19:20:47 -07:00
Lev Nachmanson cbad61ba2e propagate monics with lp_bound_propagator 2023-09-13 14:27:34 -07:00
Lev Nachmanson c309d52283 runs a simple test 2023-09-13 08:12:00 -07:00
Lev Nachmanson c050af922f fixing the bugs 2023-09-07 15:59:20 -07:00
Lev Nachmanson c43b99daae renaming
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-07 11:57:20 -07:00
Lev Nachmanson 47b64e689c restore the lemma scheme
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-07 11:33:14 -07:00
Lev Nachmanson 288e66de59 restore m_crossed* and create lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-09-06 09:27:30 -07:00
Lev Nachmanson 41f59cb1ed propagate monomial is nla 2023-09-05 18:49:59 -07:00
Lev Nachmanson 318d7d7564 fixes a bug 2023-09-01 11:32:26 -07:00
Lev Nachmanson d3258e7084 propagate lineal monomial 2023-09-01 11:18:03 -07:00
Lev Nachmanson 5509b468e9 handle monomial_bounds::unit_propagate() 2023-08-31 17:35:41 -07:00
Nikolaj Bjorner ff3268e636 move unit propagation into monomial_bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-31 14:32:05 -07:00
Nikolaj Bjorner c2cbe72b64 sketch linear monomial propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-31 11:49:05 -07:00
Nikolaj Bjorner 38b131386d add stubs for monomial unit propagation 2023-08-30 17:21:48 -07:00
Nuno Lopes 00593609c5 minor code simplification 2023-08-30 12:50:29 +01:00
Nikolaj Bjorner 09f911d8a8 include rewriter for recursive functions in model-evaluator
fixes bug reported by Tahina and Nick, @tahina-pro
2023-08-28 11:31:40 -07:00
Hari Govind V K 5ba06f4e28
print deq in lits2pure. fix #6877 (#6878) 2023-08-26 20:53:15 -07:00
Nikolaj Bjorner 63467f9dfa fix #6876
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-25 17:14:35 -07:00
Nikolaj Bjorner e8929041b8 fixing calls, signs 2023-08-22 09:29:12 -07:00
Nikolaj Bjorner 818b1129a5 fix regression in sign of literals from new solver 2023-08-22 09:04:08 -07:00
Lev Nachmanson 4564752c2f
Merge pull request #6863 from Z3Prover/nl_branches
split free vars in nla
2023-08-21 18:19:21 -07:00
Lev Nachmanson 61a7c6b28d init m_literal_vec
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2023-08-21 17:11:55 -07:00
Lev Nachmanson 9aeaed8f53
Merge branch 'master' into nl_branches 2023-08-21 16:15:20 -07:00
Nikolaj Bjorner 1d9e0feb84 Merge branch 'master' of https://github.com/z3prover/z3 2023-08-21 09:19:16 -07:00
Nikolaj Bjorner 79aa317af4 remove if-def inside cpp file that should not be there #6869
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-21 09:19:06 -07:00
Hari Govind V K b8d8553c41
support or, and, implies, distinct in mbp_basic (#6867) 2023-08-20 15:36:22 -07:00
Nikolaj Bjorner 37ddaaef69 make destructors virtual
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-08-20 15:30:57 -07:00
Nuno Lopes dda0c8ff42 array theory: use expr_ref for mk_default() so it doesnt leak if internalize throws
like on timeout/memout
2023-08-20 22:28:57 +01:00
Lev Nachmanson 9b672bc5cc remove tracking of bounds 2023-08-20 10:10:48 -07:00
Nuno Lopes 57c667e355 remove unused code 2023-08-20 15:16:47 +01:00
Nuno Lopes a694d27557 revert removal of virtual destructor of relevancy_eh since clang doesnt play along 2023-08-20 14:20:20 +01:00
Nuno Lopes 8210aafb69 ast compare_nodes: fail faster when comparing quantifier expressions 2023-08-20 14:09:04 +01:00
Nuno Lopes c469c6e1d5 attempt to fix clang buildbots 2023-08-20 13:39:15 +01:00
Nuno Lopes 28884b398c remove unneeded virtual destructor (optimization) 2023-08-20 12:57:47 +01:00
Nuno Lopes 3b546b2348 smt_context: we can't assert that the resource limits were exceeded on cancel_exception
It happens sometimes that e.g. the internalizer goes above the soft memory limit
But since it's only by a small amount, when the exception propagates back to the context, some stuff
has been freed already and we are not longer above the memory threshold
Just delete these asserts
2023-08-20 10:34:28 +01:00
Nuno Lopes 5d33805c8b optimize ~relevancy_propagator_imp() so it just dec refs the exprs in the trail
It avoid doing all the funky watch stuff
One extreme Alive2 test case goes from 40s to 28s :)
2023-08-20 10:07:56 +01:00