mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

disable selected functionality in SINGLE_THREAD mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-18 14:47:33 -07:00
parent 1072bf1536
commit d603bd7e3b
1 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/tactic/tactical.cpp
View file

@ -20,7 +20,9 @@ Notes:
#include "util/cancel_eh.h" #include "util/cancel_eh.h"
#include "util/scoped_ptr_vector.h" #include "util/scoped_ptr_vector.h"
#include "tactic/tactical.h" #include "tactic/tactical.h"
#ifndef SINGLE_THREAD
#include <thread> #include <thread>
#endif
#include <vector> #include <vector>
class binary_tactical : public tactic { class binary_tactical : public tactic {
@ -361,6 +363,14 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
return or_else(10, ts); return or_else(10, ts);
} }
#ifdef SINGLE_THREAD
tactic * par(unsigned num, tactic * const * ts) {
throw default_exception("par_tactical is unavailable in single threaded mode");
}
#else
enum par_exception_kind { enum par_exception_kind {
TACTIC_EX, TACTIC_EX,
DEFAULT_EX, DEFAULT_EX,
@ -489,6 +499,8 @@ tactic * par(unsigned num, tactic * const * ts) {
return alloc(par_tactical, num, ts); return alloc(par_tactical, num, ts);
} }
#endif
tactic * par(tactic * t1, tactic * t2) { tactic * par(tactic * t1, tactic * t2) {
tactic * ts[2] = { t1, t2 }; tactic * ts[2] = { t1, t2 };
return par(2, ts); return par(2, ts);
@ -504,6 +516,12 @@ tactic * par(tactic * t1, tactic * t2, tactic * t3, tactic * t4) {
return par(4, ts); return par(4, ts);
} }
#ifdef SINGLE_THREAD
tactic * par_and_then(tactic * t1, tactic * t2) {
throw default_exception("par_and_then is not available in single threaded mode");
}
#else
class par_and_then_tactical : public and_then_tactical { class par_and_then_tactical : public and_then_tactical {
public: public:
par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {} par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {}
@ -741,6 +759,7 @@ public:
tactic * par_and_then(tactic * t1, tactic * t2) { tactic * par_and_then(tactic * t1, tactic * t2) {
return alloc(par_and_then_tactical, t1, t2); return alloc(par_and_then_tactical, t1, t2);
} }
#endif
tactic * par_and_then(unsigned num, tactic * const * ts) { tactic * par_and_then(unsigned num, tactic * const * ts) {
unsigned i = num - 1; unsigned i = num - 1;