mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

cr

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-17 14:27:47 -07:00
parent 4b35c75712
commit 0d65b19c20
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/dd/dd_bdd.h
View file

@ -304,9 +304,11 @@ namespace dd {
unsigned bdd_size() const { return m->bdd_size(*this); }
/** Checks whether the integer val is contained in the BDD when viewed as set of integers (see also mk_int). */
// NSB code review: this API needs to be changed: bit-position to variable mapping is external
bool contains_int(rational const& val, unsigned w) { return m->contains_int(root, val, w); }
/** Returns an integer contained in the BDD, if any, and whether the BDD is a singleton. */
// NSB code review: this API needs to be changed: bit-position to variable mapping is external
find_int_t find_int(unsigned w, rational& val) { return m->find_int(root, w, val); }
};