Revision b5c43319c7bf98bf39593fde909d1379d12cbe21 authored by Alexander Nadel on 26 April 2022, 10:39:57 UTC, committed by Alexander Nadel on 26 April 2022, 10:39:57 UTC
1 parent 4006699
Main.cc
// Copyright(C) 2021 Intel Corporation
// SPDX - License - Identifier: MIT
#include <iostream>
#include <cassert>
#include <fstream>
#include <vector>
#include <array>
#include <string>
#include <filesystem>
#include <functional>
#include <cstring>
#include <iterator>
#include <cstdio>
#include <type_traits>
#ifdef __CYGWIN__
extern "C" FILE * popen(const char* command, const char* mode);
extern "C" void pclose(FILE * pipe);
#endif
#ifndef SKIP_ZLIB
#ifdef WIN32
# include "win/zlib.h"
#else
# include <zlib.h>
#endif
#endif
#include "SetInScope.h"
#ifdef WIN32
#define popen _popen
#define pclose _pclose
#define fileno _fileno
#endif
template<char delimiter>
class WordDelimitedBy : public std::string
{};
namespace fs = std::filesystem;
#include "Topor.hpp"
using namespace std;
using namespace Topor;
// Converts enum class to the underlying type
template <typename E>
constexpr auto U(E e) noexcept
{
return static_cast<std::underlying_type_t<E>>(e);
}
// The supported archive file types
enum class TArchiveFileType : uint8_t
{
XZ = 0,
LZMA = 1,
BZ = 2,
GZ = 3,
SevenZ = 4,
None = 5
};
// The supported archive file types' file signatures
constexpr uint8_t MaxSigLength = 7;
constexpr static array<array<int, MaxSigLength + 1>, U(TArchiveFileType::None)> fileSig = { {
{ 0xFD, 0x37, 0x7A, 0x58, 0x5A, 0x00, 0x00, EOF},
{ 0x5D, 0x00, 0x00, 0x80, 0x00, EOF, EOF, EOF},
{ 0x42, 0x5A, 0x68, EOF, EOF, EOF, EOF, EOF },
{ 0x1F, 0x8B, EOF, EOF, EOF, EOF, EOF, EOF },
{ 0x37, 0x7A, 0xBC, 0xAF, 0x27, 0x1C, EOF, EOF }
} };
static constexpr bool AllSigsDifferByFirstInt()
{
for (size_t i = 0; i < fileSig.size(); ++i)
{
for (size_t j = i + 1; j < fileSig.size(); ++j)
{
if (fileSig[i][0] == fileSig[j][0])
{
return false;
}
}
}
return true;
}
// We count all signatures' first integer being different in the code, which determines the file's type
static_assert(AllSigsDifferByFirstInt());
// Strings before and after the command for each archive type
static array<pair<string, string>, U(TArchiveFileType::None)> commandStringBeforeAndAfter = {
make_pair("xz -c -d",""),
make_pair("lzma -c -d",""),
make_pair("bzip2 -c -d",""),
make_pair("gzip -c -d",""),
make_pair("7z x -so","2>/dev/null"),
};
static constexpr int BadRetVal = -1;
int OnFinishingSolving(CTopor& topor, TToporReturnVal ret, bool printModel)
{
CApplyFuncOnExitFromScope<> printStatusExplanation([&]()
{
const string expl = topor.GetStatusExplanation();
if (!expl.empty())
{
cout << "c " << expl << endl;
}
});
switch (ret)
{
case Topor::TToporReturnVal::RET_SAT:
cout << "s SATISFIABLE" << endl;
if (printModel)
{
cout << "v";
for (TLit v = 1; v <= topor.GetStatistics().m_MaxUserVar; ++v)
{
const auto vVal = topor.GetLitValue(v);
assert(vVal != TToporLitVal::VAL_UNASSIGNED);
cout << " " << (vVal != TToporLitVal::VAL_UNSATISFIED ? v : -v);
}
cout << " 0" << endl;
}
return 10;
case Topor::TToporReturnVal::RET_UNSAT:
cout << "s UNSATISFIABLE" << endl;
return 20;
case Topor::TToporReturnVal::RET_TIMEOUT_LOCAL:
cout << "s TIMEOUT_LOCAL" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_CONFLICT_OUT:
cout << "s CONFLICT_OUT" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_MEM_OUT:
cout << "s MEMORY_OUT" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_USER_INTERRUPT:
cout << "s USER_INTERRUPT" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_INDEX_TOO_NARROW:
cout << "s INDEX_TOO_NARROW" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_PARAM_ERROR:
cout << "s PARAM_ERROR" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_TIMEOUT_GLOBAL:
cout << "s TIMEOUT_GLOBAL" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_DRAT_FILE_PROBLEM:
cout << "s DRAT_FILE_PROBLEM" << endl;
return BadRetVal;
case Topor::TToporReturnVal::RET_EXOTIC_ERROR:
cout << "s EXOTIC_ERROR" << endl;
return BadRetVal;
default:
cout << "s UNEXPECTED_ERROR" << endl;
return BadRetVal;
}
}
int main(int argc, char** argv)
{
if (argc == 1 || strcmp(argv[1], "-help") == 0 || strcmp(argv[1], "--help") == 0 || strcmp(argv[1], "-h") == 0)
{
cout << print_as_color <ansi_color_code::red>("c Usage:") << endl;
cout << "\tc topor_tool/topor_static/topor_debug/topor <CNF> OPTIONAL: <Param1> <Val1> <Param2> <Val2> ... <ParamN> <ValN>" << endl;
cout << "\tc <CNF> can either be a text file or an archive file in one of the following formats: .xz, .lzma, .bz2, .gz, .7z (the test is based on the file signature)" << endl;
cout << "\tc <CNF> is expected to be in simplified DIMACS format, used at SAT Competitions (http://www.satcompetition.org/2011/format-benchmarks2011.html) with the following optional extension to support incrementality:" << endl;
cout << "\tc The following Intel(R) SAT Solver-specific commands are also legal (ignore \"c \" below): " << endl;
cout << "\tc r <ParamName> <ParamVal>" << endl;
cout << "\tc ot <TimeOut> <IsCpuTimeOut>" << endl;
cout << "\tc oc <ConflictThreshold>" << endl;
cout << "\tc lb <BoostScoreLit> <Mult>" << endl;
cout << "\tc lf <FixPolarityLit> <OnlyOnce>" << endl;
cout << "\tc lc <ClearUserPolarityInfoLit>" << endl;
cout << "\tc b <BacktrackLevel>" << endl;
cout << "\tc s <Lit1 <Lit2> ... <Litn>: solve under the assumptions {<Lit1 <Lit2> ... <Litn>}" << endl;
cout << "\tc The solver parses the p cnf vars clss line, but it ignores the number of clauses and uses the number of variables as a non-mandatory hint" << endl;
cout << print_as_color <ansi_color_code::red>("c Intel(R) SAT Solver parameters:") << endl;
cout << "\tc " << print_as_color <ansi_color_code::cyan>("/topor_tool/bin_drat_file") << " : string; default = " << print_as_color<ansi_color_code::green>("\"\"") << " : " << "path to a file to write down a binary DRAT proof\n";
cout << "\tc " << print_as_color <ansi_color_code::cyan>("/topor_tool/text_drat_file") << " : string; default = " << print_as_color<ansi_color_code::green>("\"\"") << " : " << "path to a file to write down a text DRAT proof (if more than one /topor_tool/bin_drat_file and /topor_tool/text_drat_file parameters provided, only the last one is applied, rest are ignored)\n";
cout << "\tc " << print_as_color <ansi_color_code::cyan>("/topor_tool/print_model") << " : bool (0 or 1); default = " << print_as_color<ansi_color_code::green>("1") << " : " << "print the models for satisfiable invocations?\n";
cout << "\tc " << print_as_color <ansi_color_code::cyan>("/topor_tool/verify_model") << " : bool (0 or 1); default = " << print_as_color<ansi_color_code::green>("0") << " : " << "verify the models for satisfiable invocations?\n";
CTopor topor;
cout << topor.GetParamsDescr();
return 0;
}
cout << "c Intel(R) SAT Solver started" << endl;
if (argc & 1)
{
cout << "c topor_tool ERROR: the number of arguments (excluding the executable name) must be odd. Run without parameters for more information." << endl;
return BadRetVal;
}
bool isDratBinary = true;
string dratName("");
bool printModel = true;
bool verifyModel = false;
auto ParseParameters = [&](CTopor& topor)
{
// Parse parameters
for (int currArgNum = 2; currArgNum < argc; currArgNum += 2)
{
const string paramNameStr = (string)argv[currArgNum];
const string paramValStr = (string)argv[currArgNum + 1];
auto ReadBoolParam = [&](string& errMsg)
{
int intVal = 0;
stringstream ss;
try
{
intVal = stoi(paramValStr);
}
catch (...)
{
ss << "c ERROR: couldn't convert " << paramValStr << " to an integer" << endl;
}
if (intVal != 0 && intVal != 1)
{
ss << "c ERROR: " << paramValStr << " must be 0 or 1" << endl;
}
errMsg = move(ss.str());
return (bool)intVal;
};
// /topor_tool/ prefix length
static constexpr size_t ttPrefixLen = 12;
if (paramNameStr.substr(0, ttPrefixLen) == "/topor_tool/")
{
const string param = paramNameStr.substr(ttPrefixLen, paramNameStr.size() - ttPrefixLen);
if (param == "bin_drat_file")
{
dratName = paramValStr;
isDratBinary = true;
cout << "c /topor_tool/bin_drat_file " << dratName << endl;
}
else if (param == "text_drat_file")
{
dratName = paramValStr;
isDratBinary = false;
cout << "c /topor_tool/text_drat_file " << dratName << endl;
}
else if (param == "print_model")
{
cout << "c /topor_tool/print_model " << paramValStr << endl;
string errMsg;
printModel = ReadBoolParam(errMsg);
if (!errMsg.empty())
{
cout << errMsg;
return true;
}
}
else if (param == "verify_model")
{
cout << "c /topor_tool/verify_model " << paramValStr << endl;
string errMsg;
verifyModel = ReadBoolParam(errMsg);
if (!errMsg.empty())
{
cout << errMsg;
return true;
}
}
else
{
cout << "c ERROR: unrecognized /topor_tool/ parameter: " << paramNameStr << endl;
return true;
}
}
else
{
auto [paramName, paramValue] = make_pair(paramNameStr, (double)0.0);
try
{
paramValue = std::stod(paramValStr);
}
catch (...)
{
cout << "c topor_tool ERROR: could not convert " << argv[currArgNum + 1] << " to double" << endl;
return true;
}
topor.SetParam(paramName, paramValue);
const bool isError = topor.IsError();
if (isError)
{
const string errorDescr = topor.GetStatusExplanation();
cout << "c ERROR in Topor parameter: " << errorDescr << endl;
return true;
}
}
}
return false;
};
/*
* Identify the input file type, read it, read the parameters too
*/
const string inputFileName = argv[1];
if (!filesystem::exists(inputFileName))
{
cout << "c topor_tool ERROR: the input file " << inputFileName << " doesn't exist" << endl;
return BadRetVal;
}
// Does the signature match one of the archive types we support?
FILE* tmp = fopen(inputFileName.c_str(), "r");
if (tmp == nullptr)
{
cout << "c topor_tool ERROR: couldn't open the input file " << inputFileName << " to verify the signature" << endl;
return BadRetVal;
}
TArchiveFileType aFileType = TArchiveFileType::None;
int c = getc(tmp);
for (size_t currType = 0; c != EOF && currType < fileSig.size() && aFileType == TArchiveFileType::None; ++currType)
{
const auto& currSig = fileSig[currType];
if (c == currSig[0])
{
bool rightType = true;
c = getc(tmp);
for (uint8_t i = 1; c != EOF && currSig[i] != EOF; ++i, c = getc(tmp))
{
if (c != currSig[i])
{
rightType = false;
break;
}
}
if (rightType)
{
aFileType = (TArchiveFileType)currType;
cout << "c topor_tool: file type determined to an archive file.";
#ifndef SKIP_ZLIB
if (aFileType != TArchiveFileType::GZ)
{
cout << " The following command will be used to read it through a pipe : " <<
commandStringBeforeAndAfter[U(aFileType)].first << " " << inputFileName << " " << commandStringBeforeAndAfter[U(aFileType)].second;
}
else
{
cout << " It will be read using gzlib.";
}
#else
cout << " The following command will be used to read it through a pipe : " <<
commandStringBeforeAndAfter[U(aFileType)].first << " " << inputFileName << " " << commandStringBeforeAndAfter[U(aFileType)].second;
#endif
cout << endl;
}
}
}
fclose(tmp);
// Open the input file: it can be an archive file, in which case it is read as a pipe
// or a plain text file, which is read as a file
#ifndef SKIP_ZLIB
const auto useZlib = aFileType == TArchiveFileType::GZ || aFileType == TArchiveFileType::None;
FILE* f = useZlib ? (FILE*)gzopen(inputFileName.c_str(), "r") :
popen((commandStringBeforeAndAfter[U(aFileType)].first + " " + inputFileName + " " + commandStringBeforeAndAfter[U(aFileType)].second).c_str(), "r");
#else
const auto useFopen = aFileType == TArchiveFileType::None;
FILE* f = useFopen ? (FILE*)fopen(inputFileName.c_str(), "r") : popen((commandStringBeforeAndAfter[U(aFileType)].first + " " + inputFileName + " " + commandStringBeforeAndAfter[U(aFileType)].second).c_str(), "r");
#endif
if (f == nullptr)
{
cout << "c topor_tool ERROR: couldn't open the input file" << endl;
return BadRetVal;
}
CTopor* topor = nullptr;
TToporReturnVal ret = TToporReturnVal::RET_EXOTIC_ERROR;
ofstream dratFile;
CApplyFuncOnExitFromScope<> onExit([&]()
{
#ifndef SKIP_ZLIB
useZlib ? gzclose(gzFile(f)) : pclose(f);
#else
pclose(f);
#endif
if (dratName != "")
{
dratFile.close();
if (ret == TToporReturnVal::RET_SAT)
{
remove(dratName.c_str());
}
}
delete topor;
});
/*
* File reading loop
*/
// Inside the loop, we expect to read either:
// c...: a comment
// p cnf vars clss: the header (must appear before clauses; handled as recommendation only)
// Lit1 Lit2 ... LitN 0: 0-ended clause
// "s Lit1 Lit2 ... LitN": solve under the given assumption
uint64_t lineNum = 1;
bool pLineRead = false;
int retValBasedOnLatestSolve = BadRetVal;
auto CreateToporInst = [&](TLit varsNumHint = 0)
{
topor = new CTopor(varsNumHint);
if (topor == nullptr)
{
cout << "c topor_tool ERROR: couldn't create Topor instance" << endl;
return BadRetVal;
}
pLineRead = true;
if (ParseParameters(*topor)) return BadRetVal;
if (dratName != "")
{
dratFile.open(dratName.c_str());
if (dratFile.bad())
{
cout << "c topor_tool ERROR: couldn't open DRAT file " << dratName << endl;
return BadRetVal;
}
topor->DumpDrat(dratFile, isDratBinary);
}
return 0;
};
// Populated if verify_model is on
vector<vector<TLit>> vmClss;
// Returns 10 upon success and BadRetVal upon failure
auto VerifyModel = [&](vector<TLit>* assumps = nullptr)
{
// Verify the model
cout << "c topor_tool: before verifying that the model satisfies " << (assumps == nullptr ? "the clauses" : "the assumptions and the clauses") << endl;
if (assumps != nullptr)
{
// Verify the assumptions first
for (TLit a : *assumps)
{
if (a != 0)
{
TToporLitVal v = topor->GetLitValue(a);
if (v != TToporLitVal::VAL_SATISFIED && v != TToporLitVal::VAL_DONT_CARE)
{
cout << "c ERROR: assumptions " << a << " is not satisfied!" << endl;
return BadRetVal;
}
}
}
cout << "c topor_tool: assumptions verified!" << endl;
}
for (vector<TLit>& cls : vmClss)
{
bool isVerified = false;
for (TLit l : cls)
{
if (l != 0)
{
TToporLitVal v = topor->GetLitValue(l);
if (v == TToporLitVal::VAL_SATISFIED || v == TToporLitVal::VAL_DONT_CARE)
{
isVerified = true;
break;
}
}
}
if (!isVerified)
{
cout << "c ERROR: the following clause is not satisfied:";
for (TLit l : cls)
{
cout << " " << l;
}
cout << endl;
return BadRetVal;
}
}
cout << "c topor_tool: clauses verified!" << endl;
return 10;
};
const size_t maxSz = (size_t)1 << 28;
char* line = (char*)malloc(maxSz);
if (line == nullptr)
{
cout << "c topor_tool ERROR: couldn't allocate " + to_string(maxSz) + " bytes for reading the lines" << endl;
return BadRetVal;
}
auto ReadLine = [&](FILE* f, char* l, size_t maxChars)
{
#ifndef SKIP_ZLIB
return useZlib ? gzgets((gzFile)f, line, maxSz) : fgets(line, maxSz, f);
#else
return fgets(line, maxSz, f);
#endif
};
pair<double, bool> nextSolveToInSecIsCpuTime = make_pair(numeric_limits<double>::max(), false);
uint64_t nextSolveConfThr = numeric_limits<uint64_t>::max();
while (ReadLine(f, line, maxSz) != nullptr)
{
const size_t len = strlen(line);
CApplyFuncOnExitFromScope<> beforeNextLoop([&]() { ++lineNum; });
size_t currLineI = 0;
auto SkipWhitespaces = [&]()
{
while (line[currLineI] == ' ' && currLineI < len)
{
++currLineI;
}
};
SkipWhitespaces();
if (currLineI >= len)
{
// Empty line
continue;
}
if (line[currLineI] == 'c')
{
// A comment
continue;
}
if (line[currLineI] == 'r')
{
string lStr = line;
const size_t paramNameStart = 2;
const size_t paramNameEnd = lStr.find(' ', 2);
if (paramNameEnd == string::npos)
{
throw logic_error("c topor_tool ERROR: expected <paramName> never ended at line number " + to_string(lineNum));
}
const string paramName = lStr.substr(paramNameStart, paramNameEnd - paramNameStart);
const string paramVal = lStr.substr(paramNameEnd + 1);
double paramValDouble = numeric_limits<double>::infinity();
try
{
paramValDouble = stod(paramVal);
}
catch (...)
{
throw logic_error("c topor_tool ERROR: couldn't convert the parameter value to double at line number " + to_string(lineNum));
}
topor->SetParam(paramName, paramValDouble);
continue;
}
if (line[currLineI] == 'o')
{
string lStr = line;
// cout << "\tc ot <TimeOut> <IsCpuTimeOut>" << endl;
// cout << "\tc oc <ConflictThreshold>" << endl;
if (lStr[1] != 't' && lStr[1] != 'c')
{
throw logic_error("c topor_tool ERROR: The 2nd character must be either t or c at line number " + to_string(lineNum));
}
if (lStr[2] != ' ')
{
throw logic_error("c topor_tool ERROR: The 3nd character must be a space at line number " + to_string(lineNum));
}
if (lStr[1] == 't')
{
const size_t toNameStart = 2;
const size_t toNameEnd = lStr.find(' ', 3);
if (toNameEnd == string::npos)
{
throw logic_error("c topor_tool ERROR: expected <TimeOut> <IsCpuTimeOut> at line number " + to_string(lineNum));
}
const string toStr = lStr.substr(toNameStart, toNameEnd - toNameStart);
double to = numeric_limits<double>::infinity();
try
{
to = stod(toStr);
}
catch (...)
{
throw logic_error("c topor_tool ERROR: couldn't convert <TimeOut> to double at line number " + to_string(lineNum));
}
const string isCpuTimeOutStr = lStr.substr(toNameEnd + 1);
int isCpuTimeOut = numeric_limits<int>::max();
try
{
isCpuTimeOut = stoi(isCpuTimeOutStr);
}
catch (...)
{
throw logic_error("c topor_tool ERROR: couldn't convert <IsCpuTimeOut> to int at line number " + to_string(lineNum));
}
if (isCpuTimeOut < 0 || isCpuTimeOut > 1)
{
throw logic_error("c topor_tool ERROR: couldn't convert <IsCpuTimeOut> to 0 or 1 at line number " + to_string(lineNum));
}
nextSolveToInSecIsCpuTime = make_pair(to, (bool)isCpuTimeOut);
}
else
{
assert(lStr[1] == 'c');
const string cThrStr = lStr.substr(3);
try
{
nextSolveConfThr = (uint64_t)stoull(cThrStr);
}
catch (...)
{
throw logic_error("c topor_tool ERROR: couldn't convert <ConflictThreshold> to uint64_t at line number " + to_string(lineNum));
}
}
continue;
}
auto ParseNumber = [&]()
{
SkipWhitespaces();
if (currLineI >= len)
{
throw logic_error("c topor_tool ERROR: no number after skipping white-spaces at line number " + to_string(lineNum));
}
bool isNeg = line[currLineI] == '-';
if (isNeg)
{
++currLineI;
}
if (!isdigit(line[currLineI]))
{
throw logic_error("c topor_tool ERROR: the first character is expected to be a digit at line number " + to_string(lineNum));
}
long long res = 0;
while (isdigit(line[currLineI]))
{
const auto currDigit = line[currLineI++] - '0';
res = res * 10 + (long long)(currDigit);
}
if (isNeg)
{
res = -res;
}
return res;
};
if (line[currLineI] == 'l')
{
string lStr = line;
// cout << "\tc lb <BoostScoreLit> <Mult>" << endl;
// cout << "\tc lf <FixPolarityLit> <OnlyOnce>" << endl;
// cout << "\tc lc <ClearUserPolarityInfoLit>" << endl;
if (lStr[1] != 'b' && lStr[1] != 'f' && lStr[1] != 'c')
{
throw logic_error("c topor_tool ERROR: The 2nd character must be either b or f or c at line number " + to_string(lineNum));
}
if (lStr[2] != ' ')
{
throw logic_error("c topor_tool ERROR: The 3nd character must be a space at line number " + to_string(lineNum));
}
currLineI += 2;
TLit lit = (TLit)ParseNumber();
if (lStr[1] == 'c')
{
topor->ClearUserPolarityInfo(lit);
}
else if (lStr[1] == 'f')
{
const string isOnlyOnceStr = lStr.substr(currLineI + 1);
int isOnlyOnce = numeric_limits<int>::max();
try
{
isOnlyOnce = stoi(isOnlyOnceStr);
}
catch (...)
{
throw logic_error("c topor_tool ERROR: couldn't convert <FixPolarityLit> to int at line number " + to_string(lineNum));
}
if (isOnlyOnce < 0 || isOnlyOnce > 1)
{
throw logic_error("c topor_tool ERROR: couldn't convert <FixPolarityLit> to 0 or 1 at line number " + to_string(lineNum));
}
topor->FixPolarity(lit, (bool)isOnlyOnce);
}
else
{
assert(lStr[1] == 'b');
const string multStr = lStr.substr(currLineI + 1);
double mult = numeric_limits<double>::infinity();
try
{
mult = stod(multStr);
}
catch (...)
{
throw logic_error("c topor_tool ERROR: couldn't convert the <Mult> value to double at line number " + to_string(lineNum));
}
topor->BoostScore(lit, mult);
}
continue;
}
if (line[currLineI] == 'b')
{
// cout << "\tc b <BacktrackLevel>" << endl;
if (line[1] != ' ')
{
throw logic_error("c topor_tool ERROR: The 2nd character must be a space at line number " + to_string(lineNum));
}
++currLineI;
auto dl = ParseNumber();
topor->Backtrack((TLit)dl);
continue;
}
if (line[currLineI] == 'p')
{
if (pLineRead)
{
cout << "c topor_tool ERROR: second line starting with p at line number " << lineNum << endl;
return BadRetVal;
}
currLineI += 6;
// currLineI should be at the first number now
if (line[currLineI - 5] != ' ' || line[currLineI - 4] != 'c' || line[currLineI - 3] != 'n' || line[currLineI - 2] != 'f' || line[currLineI - 1] != ' ')
{
cout << "c topor_tool ERROR: couldn't parse the p-line as 'p cnf <VARS> <CLSS>' at line number " << lineNum << endl;
return BadRetVal;
}
TLit vars = 0;
try
{
long long varsLL = ParseNumber();
long long clssLL = ParseNumber();
cout << "c topor_tool: suggested #variables : " << varsLL << "; suggested #clauses : " << clssLL << endl;
if (varsLL > numeric_limits<TLit>::max() || varsLL <= 0)
{
cout << "c topor_tool warning: the suggested #variables " << varsLL << " is greater than the maximal number or is <=0, thus it will be ignored" << endl;
}
else
{
vars = (TLit)varsLL;
}
}
catch (const logic_error& le)
{
cout << "c topor_tool ERROR: couldn't parse the p-line as 'p cnf <VARS> <CLSS>': " << le.what() << " at line number " << lineNum << endl;
return BadRetVal;
}
catch (...)
{
cout << "c topor_tool ERROR: couldn't parse the p-line as 'p cnf <VARS> <CLSS>': couldn't read the variables or the clauses at line number " << lineNum << endl;
return BadRetVal;
}
SkipWhitespaces();
if (line[currLineI] != '\n')
{
cout << "c topor_tool ERROR: couldn't parse the p-line as 'p cnf <VARS> <CLSS>': new-line wasn't found where expected at line number " << lineNum << endl;
return BadRetVal;
}
assert(topor == nullptr);
if (CreateToporInst(vars) == BadRetVal)
{
return BadRetVal;
}
continue;
}
// If we're here and topor is still missing, create it without the number-of-variables hint -- no p-line is expected anymore
if (topor == nullptr)
{
if (CreateToporInst() == BadRetVal)
{
return BadRetVal;
}
}
vector<TLit> lits;
auto BufferToLits = [&]()
{
string errorString = "";
lits.clear();
long long currLit = numeric_limits<long long>::max();
while (currLit != 0)
{
try
{
currLit = ParseNumber();
if (currLit > numeric_limits<TLit>::max() || currLit < numeric_limits<TLit>::min())
{
errorString = "c topor_tool ERROR: the literal " + to_string(currLit) + " is too big or too small\n";
lits.clear();
break;
}
lits.push_back(TLit(currLit));
}
catch (...)
{
errorString = "c topor_tool ERROR: couldn't translate the following line or parts of it into a vector of literals at line number " + to_string(lineNum) + "\n";
lits.clear();
break;
}
}
return make_pair(errorString, lits);
};
if (line[currLineI] == 's')
{
++currLineI;
SkipWhitespaces();
auto [errString, assumps] = BufferToLits();
if (!errString.empty())
{
cout << errString;
return BadRetVal;
}
ret = topor->Solve(assumps, nextSolveToInSecIsCpuTime, nextSolveConfThr);
nextSolveToInSecIsCpuTime = make_pair(numeric_limits<double>::max(), false);
nextSolveConfThr = numeric_limits<uint64_t>::max();
retValBasedOnLatestSolve = topor ? OnFinishingSolving(*topor, ret, printModel) : BadRetVal;
if (verifyModel && retValBasedOnLatestSolve == 10)
{
if (VerifyModel(&assumps) == BadRetVal) return BadRetVal;
}
continue;
}
// New clause
auto [errString, cls] = BufferToLits();
if (!errString.empty())
{
cout << errString;
return BadRetVal;
}
if (verifyModel)
{
vmClss.push_back(cls);
}
topor->AddClause(cls);
}
free(line);
if (topor && topor->GetStatistics().m_SolveInvs == 0)
{
ret = topor->Solve();
retValBasedOnLatestSolve = OnFinishingSolving(*topor, ret, printModel);
if (verifyModel && retValBasedOnLatestSolve == 10)
{
if (VerifyModel() == BadRetVal) return BadRetVal;
}
}
return retValBasedOnLatestSolve;
}
Computing file changes ...