mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
remove unneded #pragma once
This commit is contained in:
parent
1d199b707b
commit
458572323a
|
@ -14,7 +14,6 @@ Author:
|
|||
Nikolaj Bjorner (nbjorner) 2020-09-29
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/ast_trail.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
|
@ -26,7 +25,7 @@ Author:
|
|||
|
||||
namespace q {
|
||||
|
||||
mbqi::mbqi(euf::solver& ctx, solver& s):
|
||||
mbqi::mbqi(euf::solver& ctx, solver& s):
|
||||
ctx(ctx), qs(s), m(s.get_manager()), m_fresh_trail(m) {}
|
||||
|
||||
|
||||
|
|
|
@ -14,7 +14,6 @@ Author:
|
|||
Nikolaj Bjorner (nbjorner) 2020-09-29
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
#include "sat/smt/q_solver.h"
|
||||
|
@ -23,7 +22,7 @@ Author:
|
|||
|
||||
|
||||
namespace q {
|
||||
|
||||
|
||||
solver::solver(euf::solver& ctx):
|
||||
th_euf_solver(ctx, ctx.get_manager().get_family_id(name())),
|
||||
m_mbqi(ctx, *this)
|
||||
|
@ -47,7 +46,7 @@ namespace q {
|
|||
switch (m_mbqi()) {
|
||||
case l_true: return sat::check_result::CR_DONE;
|
||||
case l_false: return sat::check_result::CR_CONTINUE;
|
||||
case l_undef: return sat::check_result::CR_GIVEUP;
|
||||
case l_undef: return sat::check_result::CR_GIVEUP;
|
||||
}
|
||||
return sat::check_result::CR_GIVEUP;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue