From daf7e9e3ef9b5c9584b516673e505e17511d2bdf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 2 Sep 2020 10:43:53 -0700
Subject: [PATCH] file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/sat_th.cpp | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 src/sat/smt/sat_th.cpp

diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp
new file mode 100644
index 000000000..429a7ec2b
--- /dev/null
+++ b/src/sat/smt/sat_th.cpp
@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sat_th.cpp
+
+Abstract:
+
+    Theory plugins
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+
+#include "sat/smt/sat_th.h"
+#include "sat/smt/euf_solver.h"
+
+namespace euf {
+
+
+    th_euf_solver::th_euf_solver(euf::solver& ctx, euf::theory_id id):
+        th_solver(ctx.get_manager(), id),
+        ctx(ctx)
+    {}
+
+    theory_var th_euf_solver::get_th_var(expr* e) const {
+        return get_th_var(ctx.get_enode(e));
+    }
+    
+
+
+
+
+}