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

Remove error output.

Browse Source
This commit is contained in:
chriseth 2022-07-01 14:11:30 +02:00
parent bfc9c91539
commit 1e9206e01a
4 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolutil/BooleanLP.cpp
View File

@ -306,7 +306,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
else else
{ {
cerr << _expr.toString() << endl; cerr << _expr.toString() << endl;
cerr << "Expected linear arguments." << endl; cerr << "; Expected linear arguments." << endl;
solAssert(false); solAssert(false);
} }
} }
@ -372,7 +372,7 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
} }
else else
{ {
cerr << "Unknown operator " << _expr.name << endl; cerr << "; Unknown operator " << _expr.name << endl;
solAssert(false); solAssert(false);
} }
} }
@ -558,7 +558,7 @@ Literal BooleanLPSolver::negate(Literal const& _lit)
Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr) Literal BooleanLPSolver::parseLiteralOrReturnEqualBoolean(Expression const& _expr)
{ {
if (_expr.sort->kind != Kind::Bool) if (_expr.sort->kind != Kind::Bool)
cerr << "expected bool: " << _expr.toString() << endl; cerr << "; expected bool: " << _expr.toString() << endl;
solAssert(_expr.sort->kind == Kind::Bool); solAssert(_expr.sort->kind == Kind::Bool);
// TODO when can this fail? // TODO when can this fail?
if (optional<Literal> literal = parseLiteral(_expr)) if (optional<Literal> literal = parseLiteral(_expr))

2
libsolutil/CDCL.cpp
View File

@ -84,10 +84,12 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
if (conflictClause) if (conflictClause)
{ {
conflicts++; conflicts++;
#ifdef DEBUG
m_sumConflicts++; m_sumConflicts++;
if (m_sumConflicts % 1000 == 999) { if (m_sumConflicts % 1000 == 999) {
cerr << "c confl: " << m_sumConflicts << std::endl; cerr << "c confl: " << m_sumConflicts << std::endl;
} }
#endif
if (currentDecisionLevel() == 0) if (currentDecisionLevel() == 0)
{ {
// cout << "Unsatisfiable" << endl; // cout << "Unsatisfiable" << endl;

2
libsolutil/CDCL.h
View File

@ -124,7 +124,9 @@ private:
std::map<size_t, size_t> m_levelForVariable; std::map<size_t, size_t> m_levelForVariable;
/// TODO wolud be good to not have to copy the clauses /// TODO wolud be good to not have to copy the clauses
std::map<Literal, Clause const*> m_reason; std::map<Literal, Clause const*> m_reason;
#ifdef DEBUG
uint64_t m_sumConflicts = 0; uint64_t m_sumConflicts = 0;
#endif
// Var activity // Var activity
Heap<VarOrderLt> order; Heap<VarOrderLt> order;

2
tools/solsmt.cpp
View File

@ -266,7 +266,9 @@ void SolSMT::run()
} }
else if (cmd == "define-fun") else if (cmd == "define-fun")
{ {
#ifdef DEBUG
cerr << "Ignoring 'define-fun'" << endl; cerr << "Ignoring 'define-fun'" << endl;
#endif
} }
else if (cmd == "assert") else if (cmd == "assert")
{ {