diff options
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
| -rw-r--r-- | src/theory/arith/arith_utilities.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index cfaf6ac03..30db4ec42 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -297,6 +297,12 @@ inline Node mkOnZeroIte(Node n, Node q, Node if_zero, Node not_zero) { return n.eqNode(zero).iteNode(q.eqNode(if_zero), q.eqNode(not_zero)); } +inline Node mkPi() +{ + return NodeManager::currentNM()->mkNullaryOperator( + NodeManager::currentNM()->realType(), kind::PI); +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |