diff options
Diffstat (limited to 'lib/Core/Executor.cpp')
| -rw-r--r-- | lib/Core/Executor.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e0ab9f84..e5a6bc9c 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -488,7 +488,8 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)}, replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), inhibitForking(false), haltExecution(false), - ivcEnabled(false), debugLogBuffer(debugBufferString) { + ivcEnabled(false), debugLogBuffer(debugBufferString), + visitorA{'a', arrayCache}, visitorB{'b', arrayCache} { const time::Span maxTime{MaxTime}; @@ -3953,6 +3954,13 @@ void Executor::searchDifferentiators(ExecutionState* latest) { continue; } for (const auto& state : rev.second) { + // TODO: implement symbdiff natively + std::set<ref<Expr>> combination; + for (auto const& constraint : state->constraints) + combination.insert(this->visitorA.visit(constraint)); + for (auto const& constraint : latest->constraints) + combination.insert(this->visitorB.visit(constraint)); + auto hashPair = std::make_pair(hashFn(state->formula), hashFn(latest->formula)); if (hashPair.first == hashPair.second || this->compared[hashPair]) @@ -3964,7 +3972,6 @@ void Executor::searchDifferentiators(ExecutionState* latest) { this->compared[hashPair] = true; // File I/O is expensive but SMT solving is even more expensive (-; - // Seriously though, FIXME: implement symbdiff natively const auto& smt2_name = hash(state->formula) + ".smt2"; std::ofstream smt2_file; smt2_file.open(smt2_name); |