*** ERROR: (clasp): Function requires valid conflict #85
Comments
|
I cannot reproduce the error. |
|
Mhm, this is very strange. I tried building Clasp from source, and now I also cannot reproduce the error. It only exists in the version of Clasp installed through my package manager ( |
|
The build file should set the cmake build type because otherwise it will automatically be set to release. You could set it to I'ld need both the flags and the compiler version to investigate further. |
|
Thanks for your quick repsonses @rkaminsk !
Isn't I'm not an expert on Cmake so you'll have to bear with me here. Here are the |
|
After further experimentation, the simplest way to reproduce the problem is as such (with Clang 14.0.6): |
Sure but the also have been replaced. The following could be used to enforce python and lua support. If lua and python are installed the build should still pick them up correctly because they default to
Thanks, I'll have a look. So it is maybe some ill-formed code in clasp or a compiler bug. |
I can reproduce with clang 14 and values 1 and 2 for |
|
It really looks like a compiler/library bug. With the patch below the code works as expected. The original code is perfectly fine though. diff --git a/src/solver.cpp b/src/solver.cpp
index 4bcc1d2..20a8f12 100644
--- a/src/solver.cpp
+++ b/src/solver.cpp
@@ -23,6 +23,7 @@
//
#include <clasp/solver.h>
#include <clasp/clause.h>
+
#include POTASSCO_EXT_INCLUDE(unordered_set)
namespace Clasp {
namespace {
@@ -1151,8 +1152,8 @@ bool Solver::resolveToFlagged(const LitVec& in, const uint8 vf, LitVec& out, uin
}
void Solver::resolveToCore(LitVec& out) {
POTASSCO_REQUIRE(hasConflict() && !hasStopConflict(), "Function requires valid conflict");
- cc_.clear();
std::swap(cc_, conflict_);
+ conflict_.clear();
if (searchMode() == SolverStrategies::no_learning) {
for (uint32 i = 1, end = decisionLevel() + 1; i != end; ++i) { cc_.push_back(decision(i)); }
or the following one works too: diff --git a/src/solver.cpp b/src/solver.cpp
index 4bcc1d2..08098e7 100644
--- a/src/solver.cpp
+++ b/src/solver.cpp
@@ -23,6 +23,7 @@
//
#include <clasp/solver.h>
#include <clasp/clause.h>
+
#include POTASSCO_EXT_INCLUDE(unordered_set)
namespace Clasp {
namespace {
@@ -1152,7 +1153,7 @@ bool Solver::resolveToFlagged(const LitVec& in, const uint8 vf, LitVec& out, uin
void Solver::resolveToCore(LitVec& out) {
POTASSCO_REQUIRE(hasConflict() && !hasStopConflict(), "Function requires valid conflict");
cc_.clear();
- std::swap(cc_, conflict_);
+ cc_.swap(conflict_);
if (searchMode() == SolverStrategies::no_learning) {
for (uint32 i = 1, end = decisionLevel() + 1; i != end; ++i) { cc_.push_back(decision(i)); }
} |
|
@BenKaufmann, isn't it inefficient to use std::swap here? Wouldn't just |
@rkaminsk Yes, it is completely brain-dead and breaks the (thin) abstraction of using std::swap; // pull in the "default" algorithm
swap(a, b); // allow ADL to find the "best" algorithmHowever, given that we are not in a generic context and that
I agree. While the original code is a little stupid, it is perfectly legal. Anyway, I'll fix this and #84 later today. Many thanks for investigating and solving this issue! |
* Call swap member function of LitVec directly instead of relying on std::swap, which does not call the container's own version in case LitVec is an alias for bk_lib::pod_vector<Literal>. * Coincidentally, this also prevents a code gen bug in clang 14 when clasp is built with option _FORTIFY_SOURCE. * NOTE: At this point, using bk_lib::pod_vector is probably a pessimization given that it was never updated to C++11 (rvalues and/or noexcept) - but this is a problem for another day.
|
Thanks for the quick investigation and fix! |
gringo.zip
Given the attached input file and the command
clasp --opt-strategy=usc --stats=2 gringo.outI get the following error:On the other hand, with the default
--opt-strategythere is no error. I was working with similar input files a few months ago, and I don't remember getting such problems. Any help would be appreciated!The text was updated successfully, but these errors were encountered: