mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

add stub

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-18 22:02:42 -08:00
parent 1c884c8d72
commit 30bbb5399f
2 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/saturation.cpp
View file

@ -651,6 +651,12 @@ namespace polysat {
} }
// bench 5
bool saturation::try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y) {
set_rule("[x] 2^k*x = 2^k*y & x < 2^N-k => y = x or y >= 2^{N-k}");
return false;
}
/* /*
* x*y = 1 & ~ovfl(x,y) => x = 1 * x*y = 1 & ~ovfl(x,y) => x = 1
* x*y = -1 & ~ovfl(-x,y) => -x = 1 * x*y = -1 & ~ovfl(-x,y) => -x = 1

1
src/math/polysat/saturation.h
View file

@ -54,6 +54,7 @@ namespace polysat {
bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b); bool try_factor_equality(pvar x, conflict& core, inequality const& a_l_b);
bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y); bool try_mul_eq_1(pvar x, conflict& core, inequality const& axb_l_y);
bool try_mul_odd(pvar x, conflict& core, inequality const& axb_l_y); bool try_mul_odd(pvar x, conflict& core, inequality const& axb_l_y);
bool try_mul_eq_bound(pvar x, conflict& core, inequality const& axb_l_y);
bool try_transitivity(pvar x, conflict& core, inequality const& axb_l_y); bool try_transitivity(pvar x, conflict& core, inequality const& axb_l_y);
bool try_tangent(pvar v, conflict& core, inequality const& c); bool try_tangent(pvar v, conflict& core, inequality const& c);