Is there a name for the SAT solving scenario where part of the formula is static (forming a propositional "theory") and serves as a static context for testing the satisfiability of relatively small sentence.
Many such tests need to be performed with different sentence, so evaluating the conjunction each small formula with the static part every time anew is suboptimal.
In contrast to incremental SAT, satisfiable sentences are not appended to the theory, but discarded after testing.
Is there a tool that could be adapted for such a case?
Not sure if this has an official name, but in the SMTLib parlance it is known as
check-sat-assuming. See Section 4.2.5 (page 64) of http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf