mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

add_value

Browse source
This commit is contained in:
Jakob Rath 2023-07-18 11:22:55 +02:00
parent 0d80e47350
commit 5e5164ed2c
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -707,9 +707,11 @@ namespace polysat {
} }
} }
void slicing::add_value(pvar v, rational const& value) { void slicing::add_value(pvar v, rational const& val) {
// go through all existing nodes, and evaluate v? enode* const sv = var2slice(v);
// can do that externally enode* const sval = mk_value_slice(val, width(sv));
(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 {