cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fixing remaining issues

Browse Source
This commit is contained in:
Mate Soos 2022-03-21 18:04:01 +01:00
parent 3e0f4cd7bb
commit a7a6475f6f
2 changed files with 11 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libsolutil/CDCL.cpp
View File

@ -309,7 +309,9 @@ void CDCL::cancelUntil(size_t _backtrackLevel)
m_reason.erase(l); m_reason.erase(l);
// TODO maybe could do without. // TODO maybe could do without.
m_levelForVariable.erase(l.variable); m_levelForVariable.erase(l.variable);
order.insert((int)l.variable); if (!order.inHeap((int)l.variable)) {
order.insert((int)l.variable);
}
} }
m_decisionPoints.resize(_backtrackLevel); m_decisionPoints.resize(_backtrackLevel);
m_assignmentQueuePointer = m_assignmentTrail.size(); m_assignmentQueuePointer = m_assignmentTrail.size();

16
tools/satsolver-main.cpp
View File

@ -98,6 +98,8 @@ std::pair<vector<vector<Literal>>, size_t> readCNFFile(const string& fname)
{ {
if (line.empty()) if (line.empty())
continue; continue;
if (line[0] == 'c')
continue;
if (line[0] == 'p') { if (line[0] == 'p') {
assert(line.substr(0,6) == string("p cnf ")); assert(line.substr(0,6) == string("p cnf "));
line = line.substr(6); line = line.substr(6);
@ -166,18 +168,16 @@ int main(int argc, char** argv)
if (model) { if (model) {
const size_t line_break_after = 80; const size_t line_break_after = 80;
size_t last_line_break = 0;
stringstream ss; stringstream ss;
ss << "v"; ss << "v";
for (size_t i = 0; i < model->size(); i++) { for(auto const& m: *model) {
if (ss.str().size() > line_break_after) { if (ss.str().size()-last_line_break > line_break_after) {
cout << ss.str() << endl; ss << endl;
ss.clear(); last_line_break = ss.str().size();
ss << "v"; ss << "v";
} }
// if (model->at(i) != TriState::t_unset()) { ss << " " << (m.second ? "" : "-") << m.first;
// ss << " " << (model->at(i) == TriState::t_true() ? "" : "-") << i+1;
// }
} }
cout << ss.str() << " 0" << endl; cout << ss.str() << " 0" << endl;
cout << "s SATISFIABLE" << endl; cout << "s SATISFIABLE" << endl;