Skip to content

Commit 6dba340

Browse files
Encapsulate context push/pop to track statistics
1 parent d9774b7 commit 6dba340

File tree

2 files changed

+8
-3
lines changed

2 files changed

+8
-3
lines changed

src/engine/SmtCore.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -148,7 +148,7 @@ void SmtCore::applyTrailEntry( TrailEntry &te, bool isDecision )
148148
if ( isDecision )
149149
{
150150
_engine->preContextPushHook();
151-
_context.push();
151+
pushContext();
152152
_decisions.push_back( te );
153153
}
154154

@@ -246,7 +246,6 @@ void SmtCore::pushContext()
246246
}
247247
}
248248

249-
bool SmtCore::popSplit()
250249
bool SmtCore::popDecisionLevel( TrailEntry &lastDecision )
251250
{
252251
ASSERT( static_cast<size_t>( _context.getLevel() ) == _decisions.size() );
@@ -255,7 +254,7 @@ bool SmtCore::popDecisionLevel( TrailEntry &lastDecision )
255254

256255
SMT_LOG( "Popping trail ..." );
257256
lastDecision = _decisions.back();
258-
_context.pop();
257+
popContext();
259258
_engine->postContextPopHook();
260259
SMT_LOG( Stringf( "to %d DONE", _context.getLevel() ).ascii() );
261260
return true;

src/engine/SmtCore.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -186,6 +186,12 @@ class SmtCore
186186
*/
187187
bool popSplit();
188188

189+
/*
190+
Encapsulations of _context.push/pop calls for statistics purposes.
191+
*/
192+
void pushContext();
193+
void popContext();
194+
189195
/*
190196
Pop a context level - lazily backtracking trail, bounds, etc.
191197
Return true if successful, false if the stack is empty.

0 commit comments

Comments
 (0)