diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-28 19:48:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-28 19:48:53 -0600 |
| commit | 54ed528aa098625634856f53f0ceb6f69afdafbd (patch) | |
| tree | 1b965149d4aadbd5020b1bf43181522817c4da8d /src/theory/arith/arith_utilities.h | |
| parent | 723a45eb6e6d7c055d42130574298e68f690a74a (diff) | |
Improve the rewriter for SINE. (#1221)
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 */ |