Project

General

Profile

wrt. "Pushing to the Top" (Ivrii et al., 2015) on
'Generating Proof Obligations' part are described 4 'moments' in the
code in which POs are managed:

- Candidate
picks a bad state & adds it as a MUST-po

where in the repository-code?>
-this is happens on first on PDR::getBadCube() (pick a bad state)
& later within the call to PDR::recBlockCube(po) at PDR::addToPoQueue(po)
(adds it as a MUST-po). The must PO is defined in the call to recBlockCube.

- Predecessor
adds a CTI m0 for an already existing m1
as a new PO, at the level one lower than
that of m1

where in the repository-code?>
-within PDR::recBlockCube(po) on the call to PDR::isBlocked(po) & after
getting a different result to FRAME_NULL to the call 'solveRelative'
-there are two possible outcomes SAT-case & UNSAT-case, the one
used by Predecessor is SAT-case where 'CTI found'

- ReQueue
moves a blocked MUST-po to the next level

- MayEnqueue
picks a (not bad)lemma that is not yet established at level i+1
and adds its negation as a MAY-po at level i+1