Package org.smtlib.solvers

Class Solver_simplify

java.lang.Object
org.smtlib.AbstractSolver
org.smtlib.solvers.Solver_simplify
All Implemented Interfaces:
ISolver
public class Solver_simplify extends AbstractSolver implements ISolver
The adapter that drives the Simplify solver.

Note on implementation. Simplify allows only either pushing an assertion to the background or checking that it is valid. Assertions that are pushed (via BG_PUSH) appear to be filtered out of counterexamples. Thus for now we will only use BG_PUSH for background theory axioms; for the rest we will accumulate all assertions into one giant AND (in the conjunction field) and then assert them all at once to Simplify when check-sat is called. The usual push and pop will not be sent to Simplify - rather we save the state of 'conjunction' ourselves. This implements the letter if not the spirit of push and pop, and it may have performance implications. If it does, we'll optimize the implementation then.

Several methods (declare_fun, define_fun, pop, push) send an auxiliary command (BG_PUSH/BG_POP) to the Simplify process and don't inspect its raw response: unlike the main protocol commands (assert, check-sat, ...), nothing in this project's test suite or documentation records what Simplify's failure response for one of these auxiliary commands actually looks like, so there's no format to parse against without guessing (see issue #68).

Extends AbstractSolver (for its real-process plumbing: the shared solverProcess field, options/checkSatStatus), not Solver_test (issue #97): Simplify's real process speaks its own bespoke, non-SMT-LIB Lisp-like protocol (BG_PUSH/an accumulated conjunction sent with check-sat -- see above), so AbstractSolver's generic defaults (which translate a command to standard SMT-LIB concrete syntax and send that directly) are not usable for Simplify at all -- every operation below is either genuinely Simplify-specific (talks to the real process in its own protocol) or a client-side simulation transplanted directly from Solver_test (the operations Simplify's real process cannot itself be asked about at all: get-model/get-proof/get-unsat-core/etc., reset/reset-assertions, and the declare/define-sort family, none of which the real BG_PUSH-based protocol below has any way to express). symTable/assertionSetStack/logicSet are this class's own copies of exactly what Solver_test tracks, for exactly the same reason: this class has no real process to ask instead.