diff options
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 5863a31fc..be08cfee7 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -119,6 +119,14 @@ public: */ void check(Effort level); + + /** + * Rewrites a node in the theory of uninterpreted functions. + * This is fairly basic and only ensures that atoms that are + * unsatisfiable or a valid are rewritten to false or true respectively. + */ + Node rewrite(TNode n); + /** * Propagates theory literals. Currently does nothing. * |