Revision 613cbffb7e96f803f23141771593a583bb420279 authored by Pedro Orvalho on 28 April 2023, 12:39:23 UTC, committed by GitHub on 28 April 2023, 12:39:23 UTC
1 parent bab67fc
ParserMaxSAT.h
/*!
* \author Ruben Martins - rubenm@andrew.cmu.edu
*
* @section LICENSE
*
* MiniSat, Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
* Copyright (c) 2007-2010, Niklas Sorensson
* Open-WBO, Copyright (c) 2013-2022, Ruben Martins, Vasco Manquinho, Ines Lynce
* UpMax, Copyright (c) 2022, Pedro Orvalho, Vasco Manquinho, Ruben Martins
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in
* all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*
*/
#ifndef ParserMaxSAT_h
#define ParserMaxSAT_h
#include <stdio.h>
#include "MaxSATFormula.h"
#include "core/SolverTypes.h"
#include "utils/ParseUtils.h"
#ifdef HAS_EXTRA_STREAMBUFFER
#include "utils/StreamBuffer.h"
#endif
using NSPACE::mkLit;
using NSPACE::StreamBuffer;
namespace upmax {
//=================================================================================================
// DIMACS Parser:
template <class B> static uint64_t parseWeight(B &in) {
uint64_t val = 0;
while ((*in >= 9 && *in <= 13) || *in == 32)
++in;
if (*in < '0' || *in > '9')
fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
while (*in >= '0' && *in <= '9')
val = val * 10 + (*in - '0'), ++in;
return val;
}
template <class B, class MaxSATFormula>
static uint64_t readClause(B &in, MaxSATFormula *maxsat_formula,
vec<Lit> &lits) {
int parsed_lit, var;
int64_t weight = 1;
lits.clear();
if (maxsat_formula->getProblemType() == _WEIGHTED_)
weight = parseWeight(in);
assert(weight > 0);
for (;;) {
parsed_lit = parseInt(in);
if (parsed_lit == 0)
break;
var = abs(parsed_lit) - 1;
while (var >= maxsat_formula->nVars())
maxsat_formula->newVar();
lits.push((parsed_lit > 0) ? mkLit(var) : ~mkLit(var));
}
return weight;
}
template <class B, class MaxSATFormula>
static void parseMaxSAT(B &in, MaxSATFormula *maxsat_formula) {
vec<Lit> lits;
uint64_t hard_weight = UINT64_MAX;
for (;;) {
skipWhitespace(in);
if (*in == EOF)
break;
else if (*in == 'p') {
if (eagerMatch(in, "p cnf")) {
parseInt(in); // Variables
parseInt(in); // Clauses
} else if (eagerMatch(in, "wcnf")) {
maxsat_formula->setProblemType(_WEIGHTED_);
parseInt(in); // Variables
parseInt(in); // Clauses
if (*in != '\r' && *in != '\n') {
hard_weight = parseWeight(in);
maxsat_formula->setHardWeight(hard_weight);
}
} else
printf("c PARSE ERROR! Unexpected char: %c\n", *in),
printf("s UNKNOWN\n"), exit(_ERROR_);
} else if (*in == 'c' || *in == 'p')
skipLine(in);
else {
uint64_t weight = readClause(in, maxsat_formula, lits);
if (weight < hard_weight ||
maxsat_formula->getProblemType() == _UNWEIGHTED_) {
assert(weight > 0);
// Updates the maximum weight of soft clauses.
maxsat_formula->setMaximumWeight(weight);
// Updates the sum of the weights of soft clauses.
maxsat_formula->updateSumWeights(weight);
maxsat_formula->addSoftClause(weight, lits);
} else
maxsat_formula->addHardClause(lits);
}
}
}
// Inserts problem into solver.
//
template <class MaxSATFormula>
static void parseMaxSATFormula(gzFile input_stream,
MaxSATFormula *maxsat_formula) {
StreamBuffer in(input_stream);
parseMaxSAT(in, maxsat_formula);
if (maxsat_formula->getMaximumWeight() == 1)
maxsat_formula->setProblemType(_UNWEIGHTED_);
else
maxsat_formula->setProblemType(_WEIGHTED_);
// maxsat_formula->setInitialVars(maxsat_formula->nVars());
}
//=================================================================================================
} // namespace upmax
#endif
Computing file changes ...