Commit 396c801f authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

Stasticial and debug output changes

parent f7c7fc0f
......@@ -212,80 +212,79 @@ SUBool::PCLearnComp::PrintStatistics(unsigned level) const
{
if (logs.CheckLevel(4))
{
logs.TLog(4) << "Final negatives list:" << std::endl;
logs.TLog(4) << "Final negatives list:" << '\n';
const auto &comp = mHypothesis.Compressor();
mNegatives.PrettyPrint(std::cout,
[&comp](const Literal &lit) { return comp.UncompressLiteral(lit); });
logs.TLog(4) << "Final negatives clauses:" << std::endl;
std::cout << comp.UncompressCNF(dual_rail_to_cnf(mNegatives))
<< std::endl;
logs.TLog(4) << "Final negatives clauses:" << '\n';
std::cout << comp.UncompressCNF(dual_rail_to_cnf(mNegatives)) << '\n';
}
logs.TLog(level) << ResultDesc() << std::endl;
logs.TLog(level) << "Total time: " << mRTime << std::endl;
logs.TLog(level) << "Total processor time: " << mCPUTime << std::endl;
logs.TLog(level) << ResultDesc() << '\n';
logs.TLog(level) << "Total time: " << mRTime << '\n';
logs.TLog(level) << "Total processor time: " << mCPUTime << '\n';
logs.TLog(level) << "Processor time until the last SAT based EQ check: "
<< mTimeTillTheLastSATEqCheck << std::endl;
<< mTimeTillTheLastSATEqCheck << '\n';
logs.TLog(level) << "Processor time of the last SAT based EQ check: "
<< mTimeOfLastSATEqCheck << std::endl;
<< mTimeOfLastSATEqCheck << '\n';
logs.TLog(level)
<< "Processor time of the last SAT solver call within an EQ check: "
<< mPCCheckerSAT.LastSolveTime() << std::endl;
<< mPCCheckerSAT.LastSolveTime() << '\n';
logs.TLog(level) << "Negatives added to the hypothesis: "
<< mNegativesAddedToHypothesis << std::endl;
<< mNegativesAddedToHypothesis << '\n';
logs.TLog(level) << "Clauses added to the hypothesis: "
<< mClausesAddedToHypothesis << std::endl;
<< mClausesAddedToHypothesis << '\n';
logs.TLog(level) << "Number of successful refinements: "
<< mSuccessfulRefinements << std::endl;
<< mSuccessfulRefinements << '\n';
logs.TLog(level) << "Number of initial candidates: "
<< mInitialCandidatesListSize << '\n';
logs.TLog(level) << "Total number of candidates with closure: "
<< mCandidatesWithClosureCount << std::endl;
<< mCandidatesWithClosureCount << '\n';
logs.TLog(level) << "Total number of candidates without closure: "
<< mCandidatesWithoutClosureCount << std::endl;
<< mCandidatesWithoutClosureCount << '\n';
logs.TLog(level) << "Total number of learned clauses considered: "
<< mLearnedClausesConsideredCount << std::endl;
<< mLearnedClausesConsideredCount << '\n';
logs.TLog(level) << "Total number of negative examples extracted from the "
"learned clauses: "
<< mLearnedClausesCandidatesCount << std::endl;
<< mLearnedClausesCandidatesCount << '\n';
logs.TLog(level) << "Total number of random empowering implicates: "
<< mRandomEmpoweringCount << std::endl;
<< mRandomEmpoweringCount << '\n';
logs.TLog(level) << "Total number of random bodies: " << mRandomBodyCount
<< std::endl;
<< '\n';
logs.TLog(level) << "Total number of learned clauses from random queries: "
<< mRandomLearnedCount << std::endl;
<< mRandomLearnedCount << '\n';
logs.TLog(level) << "Total number of random queries: " << mRandomQueriesCount
<< std::endl;
<< '\n';
logs.TLog(level) << "Candidates extracted from new negatives: "
<< mCandidatesFromNegativesCount << std::endl;
<< mCandidatesFromNegativesCount << '\n';
logs.TLog(level) << "Total number of empowering implicates found by SAT: "
<< mSATEmpoweringCount << std::endl;
<< mSATEmpoweringCount << '\n';
logs.TLog(level) << "Total time of SAT based equivalence queries: "
<< mPCCheckerSAT.TotalTime() << "s" << std::endl;
<< mPCCheckerSAT.TotalTime() << "s" << '\n';
logs.TLog(level) << "SAT based equivalence with result SAT (time/count): "
<< mPCCheckerSAT.TotalTimeSAT() << "s / "
<< mPCCheckerSAT.SolveCountSAT() << std::endl;
<< mPCCheckerSAT.SolveCountSAT() << '\n';
logs.TLog(level) << "SAT based equivalence with result UNSAT (time/count): "
<< mPCCheckerSAT.TotalTimeUNSAT() << "s / "
<< mPCCheckerSAT.SolveCountUNSAT() << std::endl;
<< mPCCheckerSAT.SolveCountUNSAT() << '\n';
logs.TLog(level) << "Maximum UP level: "
<< mPCCheckerSAT.CurrentUPLevelBound() << std::endl;
logs.TLog(level) << "Closure cache hit count: " << mCacheHitCount
<< std::endl;
logs.TLog(level) << "Closure cache miss count: " << mCacheMissCount
<< std::endl;
<< mPCCheckerSAT.CurrentUPLevelBound() << '\n';
logs.TLog(level) << "Closure cache hit count: " << mCacheHitCount << '\n';
logs.TLog(level) << "Closure cache miss count: " << mCacheMissCount << '\n';
logs.TLog(level) << "Closure cache find total time: " << mCacheFindTotalTime
<< std::endl;
<< '\n';
logs.TLog(level) << "Number of intersections: " << mIntersectionCount
<< std::endl;
<< '\n';
logs.TLog(level) << "Total time spent with intersections: "
<< mIntersectionTotalTime << std::endl;
<< mIntersectionTotalTime << '\n';
logs.TLog(level) << "Total time spent in RefinedNegative: "
<< mRefinedNegativeTotalTime << std::endl;
<< mRefinedNegativeTotalTime << '\n';
logs.TLog(level) << "Total time of semantic closure computation: "
<< mSemanticClosureTotalTime << std::endl;
<< mSemanticClosureTotalTime << '\n';
logs.TLog(level)
<< "Total number of SAT calls in semantic closure computation: "
<< mSemanticClosureSolveCount << std::endl;
<< mSemanticClosureSolveCount << '\n';
logs.TLog(level) << "Number of semantic closure computations: "
<< mSemanticClosureCount << std::endl;
<< mSemanticClosureCount << '\n';
double avg_semantic_closure_solve_count =
(mSemanticClosureCount > 0
? static_cast<double>(mSemanticClosureSolveCount)
......@@ -293,7 +292,7 @@ SUBool::PCLearnComp::PrintStatistics(unsigned level) const
: 0.0);
logs.TLog(level)
<< "Average number of SAT calls in semantic closure computations: "
<< avg_semantic_closure_solve_count << std::endl;
<< avg_semantic_closure_solve_count << '\n';
logs.TLog(level)
<< "CSV " << mRTime.Duration() << ';' << mCPUTime.TimeSpan() << ';'
<< mTimeTillTheLastSATEqCheck << ';' << mTimeOfLastSATEqCheck << ';'
......@@ -337,7 +336,8 @@ void
SUBool::PCLearnComp::MoveNegativesToCandidates(std::vector<LitImpl> negatives)
{
logs.TLog(2) << "Moving " << negatives.size()
<< " negative examples to candidates list" << std::endl;
<< " initial candidates to the queue" << std::endl;
mInitialCandidatesListSize = negatives.size();
if (logs.CheckLevel(4))
{
logs.TLog(4) << "Initial negatives list:" << std::endl;
......
......@@ -111,6 +111,7 @@ namespace SUBool
size_t mNegativesAddedToHypothesis{0};
size_t mClausesAddedToHypothesis{0};
size_t mSuccessfulRefinements{0};
size_t mInitialCandidatesListSize{0};
size_t mCandidatesWithClosureCount{0};
size_t mCandidatesWithoutClosureCount{0};
size_t mLearnedClausesConsideredCount{0};
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment