diff options
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
| -rw-r--r-- | src/theory/arith/arith_utilities.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index f87a908b4..2d466f52f 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -335,6 +335,9 @@ void printRationalApprox(const char* c, Node cr, unsigned prec = 5); */ Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs); +/** Make the node u >= a ^ a >= l */ +Node mkBounded(Node l, Node a, Node u); + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |