From 436fc5836a20baaacdcf1c27b1bd3fa066b58b6c Mon Sep 17 00:00:00 2001 From: Andrew Wu Date: Thu, 22 Aug 2024 15:34:22 -0400 Subject: [PATCH] add todos --- src/engine/DnCManager.cpp | 2 ++ src/engine/Marabou.cpp | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/engine/DnCManager.cpp b/src/engine/DnCManager.cpp index bae871e71..ff8e404c1 100644 --- a/src/engine/DnCManager.cpp +++ b/src/engine/DnCManager.cpp @@ -329,6 +329,8 @@ void DnCManager::printResult() { std::cout << "sat\n" << std::endl; + // TODO: update the variable assignment using NLR if possible and double-check that all the + // constraints are indeed satisfied. extractSolution( *_baseQuery ); printf( "Input assignment:\n" ); diff --git a/src/engine/Marabou.cpp b/src/engine/Marabou.cpp index f29ed113e..feed4d648 100644 --- a/src/engine/Marabou.cpp +++ b/src/engine/Marabou.cpp @@ -243,7 +243,8 @@ void Marabou::solveQuery() } } - + // TODO: update the variable assignment using NLR if possible and double-check that all the + // constraints are indeed satisfied. if ( _engine->getExitCode() == Engine::SAT ) _engine->extractSolution( _inputQuery ); }