Skip to content

Commit 750dd68

Browse files
enable par_then and par_or even if single threaded - fall back to sequential mode
1 parent f64d077 commit 750dd68

File tree

1 file changed

+3
-23
lines changed

1 file changed

+3
-23
lines changed

src/tactic/tactical.cpp

+3-23
Original file line numberDiff line numberDiff line change
@@ -444,20 +444,10 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
444444
return or_else(10, ts);
445445
}
446446

447-
class no_par_tactical : public tactic {
448-
public:
449-
char const* name() const override { return "par"; }
450-
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
451-
throw default_exception("par_tactical is unavailable in single threaded mode");
452-
}
453-
tactic * translate(ast_manager & m) override { return nullptr; }
454-
void cleanup() override {}
455-
};
456-
457447
#ifdef SINGLE_THREAD
458448

459-
tactic * par(unsigned num, tactic * const * ts) {
460-
return alloc(no_par_tactical);
449+
tactic* par(unsigned num, tactic* const* ts) {
450+
return alloc(or_else_tactical, num, ts);
461451
}
462452

463453
#else
@@ -606,21 +596,11 @@ tactic * par(tactic * t1, tactic * t2, tactic * t3, tactic * t4) {
606596
return par(4, ts);
607597
}
608598

609-
class no_par_and_then_tactical : public tactic {
610-
public:
611-
char const* name() const override { return "par_then"; }
612-
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
613-
throw default_exception("par_and_then is not available in single threaded mode");
614-
}
615-
tactic * translate(ast_manager & m) override { return nullptr; }
616-
void cleanup() override {}
617-
};
618-
619599

620600
#ifdef SINGLE_THREAD
621601

622602
tactic * par_and_then(tactic * t1, tactic * t2) {
623-
return alloc(no_par_and_then_tactical);
603+
return alloc(and_then_tactical, t1, t2);
624604
}
625605

626606
#else

0 commit comments

Comments
 (0)