diff --git a/clasp/parser.h b/clasp/parser.h index cd8885a..5dbd7ac 100644 --- a/clasp/parser.h +++ b/clasp/parser.h @@ -151,9 +151,12 @@ class DimacsReader : public SatReader { virtual void addObjective(const WeightLitVec& vec); virtual void addAssumption(Literal x); private: + void parsePbConstraint(WeightLitVec& scratch, int64_t maxV); + void parseConstraintRhs(WeightLitVec& lhs); SatBuilder* program_; Var numVar_; bool wcnf_; + bool plus_; }; //! Parser for opb format. class OpbReader : public SatReader { diff --git a/src/parser.cpp b/src/parser.cpp index 8b265f6..bcc89d0 100644 --- a/src/parser.cpp +++ b/src/parser.cpp @@ -296,7 +296,7 @@ bool DimacsReader::doAttach(bool& inc) { require(match("p "), "missing problem line"); wcnf_ = match("w"); require(match("cnf", false), "unrecognized format, [w]cnf expected"); - if (stream()->peek() == '+') { stream()->get(); } + plus_ = match("+", false); require(stream()->get() == ' ', "invalid problem line: expected ' ' after format"); numVar_ = matchPos(ProgramParser::VAR_MAX, "#vars expected"); uint32 numC = matchPos("#clauses expected"); @@ -314,23 +314,27 @@ bool DimacsReader::doAttach(bool& inc) { bool DimacsReader::doParse() { LitVec cc; WeightLitVec wlc; const bool wcnf = wcnf_; + const bool card = plus_; const int64 maxV = static_cast(numVar_); for (int64 cw = (int64)options.isEnabled(ParserOptions::parse_maxsat), lit = 0; skipLines('c') && peek(true); cc.clear()) { if (wcnf) { require(stream()->match(cw) && cw > 0, "wcnf: positive clause weight expected"); } - for (lit = -1; stream()->match(lit) && lit != 0;) { - require(lit >= -maxV && lit <= maxV, "invalid variable in clause"); - cc.push_back(toLit(static_cast(lit))); + if (!card || peek(wcnf) != 'w') { + for (lit = -1; stream()->match(lit) && lit != 0;) { + require(lit >= -maxV && lit <= maxV, "invalid variable in clause"); + cc.push_back(toLit(static_cast(lit))); + } + if (lit == 0) { program_->addClause(cc, cw); } + else { + require(plus_, "invalid character in clause - '0' expected"); + wlc.clear(); + for (LitVec::const_iterator it = cc.begin(), end = cc.end(); it != end; ++it) { + wlc.push_back(WeightLiteral(*it, 1)); + } + parseConstraintRhs(wlc); + } } - if (lit == 0) { program_->addClause(cc, cw); } else { - require(!wcnf, "invalid character in clause"); - const int sign = match("<= ") ? -1 : int(require(match(">= "), "invalid constraint operator")); - const int bound = matchInt(CLASP_WEIGHT_T_MIN, CLASP_WEIGHT_T_MAX, "invalid constraint bound"); - wlc.clear(); - for (LitVec::const_iterator it = cc.begin(), end = cc.end(); it != end; ++it) { - wlc.push_back(WeightLiteral(*it, sign)); - } - program_->addConstraint(wlc, bound * sign); + parsePbConstraint(wlc, maxV); } } return require(!more(), "unrecognized format"); @@ -341,6 +345,32 @@ void DimacsReader::addObjective(const WeightLitVec& vec) { void DimacsReader::addAssumption(Literal x) { program_->addAssumption(x); } +void DimacsReader::parseConstraintRhs(WeightLitVec& lhs) { + char c = stream()->get(); + require((c == '<' || c == '>') && match("= "), "constraint operator '<=' or '>=' expected"); + int64_t bound; + require(stream()->match(bound), "constraint bound expected"); + require(bound >= CLASP_WEIGHT_T_MIN && bound <= CLASP_WEIGHT_T_MAX, "invalid constraint bound"); + if (c == '<') { + bound *= -1; + for (WeightLitVec::iterator it = lhs.begin(), end = lhs.end(); it != end; ++it) { + it->second *= -1; + } + } + program_->addConstraint(lhs, static_cast(bound)); +} +void DimacsReader::parsePbConstraint(WeightLitVec& constraint, int64_t maxV) { + constraint.clear(); + require(match("w"), "'w' expected"); + for (int64_t weight, lit; stream()->match(weight); ) { + require(weight >= CLASP_WEIGHT_T_MIN && weight <= CLASP_WEIGHT_T_MAX, "invalid constraint weight"); + match("*"); + require(stream()->match(lit), "literal expected"); + require(lit >= -maxV && lit <= maxV && lit != 0, "invalid variable in constraint"); + constraint.push_back(WeightLiteral(toLit(static_cast(lit)), static_cast(weight))); + } + parseConstraintRhs(constraint); +} ///////////////////////////////////////////////////////////////////////////////////////// // OpbReader ///////////////////////////////////////////////////////////////////////////////////////// diff --git a/tests/parser_test.cpp b/tests/parser_test.cpp index c0a7f07..96f0346 100644 --- a/tests/parser_test.cpp +++ b/tests/parser_test.cpp @@ -757,6 +757,17 @@ TEST_CASE("Dimacs parser", "[parser][sat]") { REQUIRE(ctx.numConstraints() == 3); } + SECTION("testCnf+Pb") { + prg << "p cnf+ 7 3\n" + "1 -2 3 5 -7 <= 3\n" + "w 1*4 2*5 1*6 3*-7 >= 2\n" + "3 5 7 0\n"; + REQUIRE((parse(api, prg) && api.endProgram())); + REQUIRE(ctx.numVars() == 7); + REQUIRE(ctx.output.size() == 7); + REQUIRE(ctx.numConstraints() == 3); + } + SECTION("testWcnf") { prg << "c comments Weighted Max-SAT\n" << "p wcnf 3 5\n" @@ -797,6 +808,17 @@ TEST_CASE("Dimacs parser", "[parser][sat]") { REQUIRE(wLits->lits[1].second == 4); REQUIRE(wLits->lits[2].second == 1); } + + SECTION("testWcnfPlus") { + prg << "p wcnf+ 7 3 10\n" + "10 1 -2 3 5 -7 <= 3\n" + "10 w 1*4 2*5 1*6 3*-7 >= 2\n"; + REQUIRE((parse(api, prg) && api.endProgram())); + REQUIRE(ctx.numVars() == 7); + REQUIRE(ctx.output.size() == 7); + REQUIRE(ctx.numConstraints() == 2); + } + SECTION("testDimacsExtSupportsGraph") { prg << "p cnf 4 3\n"