mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

add placeholder for factor equality

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-07 20:12:19 -08:00
parent 437f826e8b
commit acbd60799d
2 changed files with 18 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -43,6 +43,8 @@ namespace polysat {
return true;
if (try_parity(v, core, i))
return true;
if (try_factor_equality(v, core, i))
return true;
if (try_ugt_x(v, core, i))
return true;
if (try_ugt_y(v, core, i))
@ -761,6 +763,21 @@ namespace polysat {
return false;
}
/**
* [x] ax + p <= q, ax + r = 0 => -r + p <= q
* [x] p <= ax + q, ax + r = 0 => p <= -r + q
* generalizations
* [x] abx + p <= q, ax + r = 0 => -rb + p <= q
* [x] p <= abx + q, ax + r = 0 => p <= -rb + q
*/
bool saturation::try_factor_equality(pvar x, conflict& core, inequality const& a_l_b) {
// search for abx+p pattern in a_l_b.lhs()
// search for ax + r = 0 equality in core (or in search but maybe not needed)
// replace abx by -rb in patterns on either a_l_b.lhs() or a_l_b.rhs() or both if available to form new implied
// literal wtihout occurrence of x
return false;
}
/*
* TODO
*

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

@ -48,6 +48,7 @@ namespace polysat {
bool try_parity(pvar x, conflict& core, inequality const& axb_l_y);
bool try_mul_bounds(pvar x, conflict& core, inequality const& axb_l_y);
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_odd(pvar x, conflict& core, inequality const& axb_l_y);
bool try_tangent(pvar v, conflict& core, inequality const& c);