3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-02 10:43:53 -07:00
parent 116390833b
commit daf7e9e3ef

37
src/sat/smt/sat_th.cpp Normal file
View file

@ -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));
}
}