mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 22:03:39 +00:00
Code Activity

move some todos

Browse source
This commit is contained in:
Jakob Rath 2023-07-18 15:11:46 +02:00
parent 4742985906
commit 68b151b0d2
1 changed files with 2 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/slicing.cpp
View file

@ -28,9 +28,11 @@ Example:
TODO: TODO:
- track disequalities
- track fixed bits along with enodes - track fixed bits along with enodes
- notify solver about equalities discovered by congruence - notify solver about equalities discovered by congruence
- implement query functions - implement query functions
- when solver assigns value of a variable v, add equations with v substituted by its value?
*/ */
@ -558,11 +560,6 @@ namespace polysat {
bool result = (xs == ys); bool result = (xs == ys);
xs.clear(); xs.clear();
ys.clear(); ys.clear();
if (result) {
// TODO: merge equivalence class of x, y (on upper level)? but can we always combine the sub-trees?
// need to add a congruence to track justification.
// adding virtual concat terms for x,y will do that automatically.
}
return result; return result;
} }
@ -661,7 +658,6 @@ namespace polysat {
} }
void slicing::add_constraint(signed_constraint c) { void slicing::add_constraint(signed_constraint c) {
// TODO: evaluate under current assignment? (no, do that externally)
if (!c->is_eq()) if (!c->is_eq())
return; return;
dep_t const d = c.blit(); dep_t const d = c.blit();
@ -711,7 +707,6 @@ namespace polysat {
enode* const sv = var2slice(v); enode* const sv = var2slice(v);
enode* const sval = mk_value_slice(val, width(sv)); enode* const sval = mk_value_slice(val, width(sv));
(void)merge(sv, sval, v); (void)merge(sv, sval, v);
// TODO: go through all existing nodes, and evaluate v? (no, better do that externally)
} }
std::ostream& slicing::display(std::ostream& out) const { std::ostream& slicing::display(std::ostream& out) const {