From 4b1a730f4612bc8d123ddf1a2000e1dd05ca81a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 12:47:16 -0700 Subject: [PATCH] API method for translating context Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 605d23876..be496f6bf 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1338,6 +1338,11 @@ namespace smt { */ context * mk_fresh(symbol const * l = 0, smt_params * p = 0); + /** + \brief Translate context to use new manager m. + */ + context * translate(ast_manager& m); + app * mk_eq_atom(expr * lhs, expr * rhs); bool set_logic(symbol logic) { return m_setup.set_logic(logic); }