mirror of
https://github.com/Z3Prover/z3
synced 2025-04-14 21:08:46 +00:00
missing virtual functions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4f9ef12f34
commit
06771d1ac5
|
@ -49,6 +49,9 @@ class non_parallel_tactic : public tactic {
|
|||
void operator()(const goal_ref & g,goal_ref_buffer & result) override {
|
||||
throw default_exception("parallel tactic is disabled in single threaded mode");
|
||||
}
|
||||
tactic * translate(ast_manager & m) override { return nullptr; }
|
||||
void cleanup() override {}
|
||||
|
||||
};
|
||||
|
||||
#ifdef SINGLE_THREAD
|
||||
|
|
|
@ -429,7 +429,9 @@ public:
|
|||
char const* name() const override { return "par"; }
|
||||
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
|
||||
throw default_exception("par_tactical is unavailable in single threaded mode");
|
||||
}
|
||||
}
|
||||
tactic * translate(ast_manager & m) override { return nullptr; }
|
||||
void cleanup() override {}
|
||||
};
|
||||
|
||||
#ifdef SINGLE_THREAD
|
||||
|
@ -589,7 +591,9 @@ public:
|
|||
char const* name() const override { return "par_then"; }
|
||||
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
|
||||
throw default_exception("par_and_then is not available in single threaded mode");
|
||||
}
|
||||
}
|
||||
tactic * translate(ast_manager & m) override { return nullptr; }
|
||||
void cleanup() override {}
|
||||
};
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue