Package org.smtlib.solvers

Class Solver_altergo

java.lang.Object

org.smtlib.AbstractSolver

org.smtlib.solvers.Solver_altergo

All Implemented Interfaces:

ISolver

public class Solver_altergo
extends AbstractSolver
implements ISolver

The adapter for Alt-Ergo (developed against 2.6.3 on Linux), run as alt-ergo --input smtlib2 --output smtlib2, reading the script from standard input.

Alt-Ergo writes nothing for a successful command and answers (set-option :print-success true) with unsupported, so solverPrintsSuccess() is false: each command is followed by an echo that marks the end of its response (see AbstractSolver). Alt-Ergo ignores, writing nothing, get-option, get-value, get-assertions, get-unsat-core, get-unsat-assumptions, get-proof and reset-assertions; those are answered here. It is run with --continue-on-error (by default it exits after any error), and in its default mode answers check-sat with unsat or unknown, never sat.

Timeout: Alt-Ergo's --timelimit=SECONDS is one value, applied whole-run or, with --timelimit-per-goal, per goal; see the constructor for how jSMTLIB's two timeouts map onto it.

Nested Class Summary

Nested classes/interfaces inherited from class org.smtlib.AbstractSolver

AbstractSolver.Pending, AbstractSolver.Shape, AbstractSolver.StackChange

Nested classes/interfaces inherited from interface org.smtlib.ISolver

ISolver.CreationException

Field Summary

Fields

Modifier and Type	Field	Description
protected String[]	cmds	The command-line arguments for launching the solver.

Fields inherited from class org.smtlib.AbstractSolver

checkSatStatus, END_WAIT_MILLIS, endedByTimeLimit, isMac, isWindows, linesOffset, options, printSuccess, printSuccessResponse, smtConfig, SOLVER_EXITED, solverProcess

Constructor Summary

Constructors

Constructor	Description
Solver_altergo(SMT.Configuration smtConfig, String executable)	Creates an instance of the solver
Solver_altergo(SMT.Configuration smtConfig, String[] command)	Launches the given command as is (a .command property, #147), without adding the flags the executable form adds

Method Summary

Modifier and Type	Method	Description
IResponse	exit()	Alt-Ergo is silent for exit, as for any successful command, but no echo can follow it, since the process ends; so success is answered once the process has ended.
IResponse	get_assertions()	Alt-Ergo ignores get-assertions, writing nothing; answered unsupported without sending it
IResponse	get_assignment()	Alt-Ergo answers get-assignment in assert mode after a check.
IResponse	get_model()	Alt-Ergo answers get-model in assert mode after a check
IResponse	get_option(IExpr.IKeyword key)	Alt-Ergo ignores get-option, writing nothing; answered from the values set (see set_option_impl) and the SMT-LIB defaults
IResponse	get_proof()	Alt-Ergo writes nothing for get-proof (it ignores it); answered unsupported without sending it
IResponse	get_unsat_assumptions()	Alt-Ergo ignores get-unsat-assumptions, writing nothing; answered unsupported without sending it
IResponse	get_unsat_core()	Alt-Ergo ignores get-unsat-core, writing nothing (with --sat-solver Tableaux it writes a non-SMT-LIB core after check-sat instead); answered unsupported without sending it
IResponse	get_value(IExpr... terms)	Alt-Ergo ignores get-value, writing nothing; answered unsupported without sending it
IResponse	reset_assertions()	Alt-Ergo ignores reset-assertions, writing nothing and keeping the assertions; answered unsupported without sending it
protected IResponse	set_option_impl(IExpr.IKeyword key, IAttributeValue value)	Sent to Alt-Ergo, and kept here for get_option when Alt-Ergo accepts it
protected boolean	solverPrintsSuccess()	Alt-Ergo writes nothing for a successful command and answers (set-option :print-success true) with unsupported; its commands are therefore sent as when pipelining, each followed by an echo that marks the end of its response
IResponse	start()	Starts the solver; this is not an SMT-LIB command, but it is convenient in some implementations to separate the starting and initialization from the construction of the solver instance.

Methods inherited from class org.smtlib.AbstractSolver

assertExpr, check_sat, check_sat_assuming, checkImmediateExit, checkPrintSuccess, checkSatStatus, checkShape, checkStatus, comment, correctResponse, declare_const, declare_datatype, declare_datatypes, declare_fun, declare_sort, declare_sort_parameter, define_const, define_fun, define_fun_rec, define_funs_rec, define_sort, earlierSourceLine, echo, errorStopsSolver, execute, executePipelined, exitedResponse, finishPipelined, forceExit, get_info, hasPending, inSatMode, interrupt, inUnsatMode, isFlatResponse, isTimeLimitResponse, lineNumberPatterns, logSolverDiagnostics, modelResponse, nextSolverLine, normalizeForTesting, outOfStep, parseResponse, pipelines, pop, proofResponse, push, readPipelined, recordChange, reportsEarlierLines, reportSeedIgnored, requireNoChangeSinceCheck, requireOptionEnabled, requireSatOrUnknown, requireUnsat, reset, responseEnd, selfReportsImmediateExit, sendChange, sendCommand, sendExitCommand, sendFailure, sendFailure, sendPipelined, sendScriptText, sendSeed, set_info, set_logic, set_option, setSourceLine, shapeOf, smt, solverName, successOrEmpty, timeLimitResponse, timeLimitResponseAfterExit, translate, unsatAssumptionsElements, unsatCoreElements, withSourceLines

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.smtlib.ISolver

assertExpr, check_sat, check_sat_assuming, checkSatStatus, comment, declare_const, declare_datatype, declare_datatypes, declare_fun, declare_sort, declare_sort_parameter, define_const, define_fun, define_fun_rec, define_funs_rec, define_sort, echo, execute, forceExit, get_info, pop, push, reset, set_info, set_logic, set_option, setSourceLine, smt, solverName

Field Details

cmds

protected String[] cmds

The command-line arguments for launching the solver.

Constructor Details

Solver_altergo

public Solver_altergo(SMT.Configuration smtConfig,
 String executable)

Creates an instance of the solver

Solver_altergo

public Solver_altergo(SMT.Configuration smtConfig,
 String[] command)

Launches the given command as is (a .command property, #147), without adding the flags the executable form adds

Method Details

start

public IResponse start()

Description copied from interface: ISolver

Starts the solver; this is not an SMT-LIB command, but it is convenient in some implementations to separate the starting and initialization from the construction of the solver instance.

Specified by:

start in interface ISolver

Overrides:

start in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.start()

solverPrintsSuccess

protected boolean solverPrintsSuccess()

Alt-Ergo writes nothing for a successful command and answers (set-option :print-success true) with unsupported; its commands are therefore sent as when pipelining, each followed by an echo that marks the end of its response

Overrides:

solverPrintsSuccess in class AbstractSolver

exit

public IResponse exit()

Alt-Ergo is silent for exit, as for any successful command, but no echo can follow it, since the process ends; so success is answered once the process has ended. If it had already ended (its output was read to its end) or does not end in time, the answer is as the base class gives it, or an error.

Specified by:

exit in interface ISolver

Overrides:

exit in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.exit()

set_option_impl

protected IResponse set_option_impl(IExpr.IKeyword key,
 IAttributeValue value)

Sent to Alt-Ergo, and kept here for get_option when Alt-Ergo accepts it

Overrides:

set_option_impl in class AbstractSolver

get_option

public IResponse get_option(IExpr.IKeyword key)

Alt-Ergo ignores get-option, writing nothing; answered from the values set (see set_option_impl) and the SMT-LIB defaults

Specified by:

get_option in interface ISolver

Overrides:

get_option in class AbstractSolver

Parameters:

key - the keyword naming the option

Returns:

the option value, or unsupported, or an SMT error response

See Also:

• ISolver.get_option(IExpr.IKeyword)

reset_assertions

public IResponse reset_assertions()

Alt-Ergo ignores reset-assertions, writing nothing and keeping the assertions; answered unsupported without sending it

Specified by:

reset_assertions in interface ISolver

Overrides:

reset_assertions in class AbstractSolver

Returns:

success or an SMT error response

See Also:

• ISolver.reset_assertions()

get_proof

public IResponse get_proof()

Alt-Ergo writes nothing for get-proof (it ignores it); answered unsupported without sending it

Specified by:

get_proof in interface ISolver

Overrides:

get_proof in class AbstractSolver

Returns:

a proof, unsupported, or an SMT error response

See Also:

• ISolver.get_proof()

get_value

public IResponse get_value(IExpr... terms)

Alt-Ergo ignores get-value, writing nothing; answered unsupported without sending it

Specified by:

get_value in interface ISolver

Overrides:

get_value in class AbstractSolver

Parameters:

terms - expressions to evaluate

Returns:

a list of term–value pairs, unsupported, or an SMT error response

See Also:

• ISolver.get_value(IExpr...)

get_assertions

public IResponse get_assertions()

Alt-Ergo ignores get-assertions, writing nothing; answered unsupported without sending it

Specified by:

get_assertions in interface ISolver

Overrides:

get_assertions in class AbstractSolver

Returns:

a sequence of asserted terms, unsupported, or an SMT error response

See Also:

• ISolver.get_assertions()

get_unsat_core

public IResponse get_unsat_core()

Alt-Ergo ignores get-unsat-core, writing nothing (with --sat-solver Tableaux it writes a non-SMT-LIB core after check-sat instead); answered unsupported without sending it

Specified by:

get_unsat_core in interface ISolver

Overrides:

get_unsat_core in class AbstractSolver

Returns:

a list of formula names, unsupported, or an SMT error response

See Also:

• ISolver.get_unsat_core()

get_unsat_assumptions

public IResponse get_unsat_assumptions()

Alt-Ergo ignores get-unsat-assumptions, writing nothing; answered unsupported without sending it

Specified by:

get_unsat_assumptions in interface ISolver

Overrides:

get_unsat_assumptions in class AbstractSolver

Returns:

a list of assumption literals, unsupported, or an SMT error response

See Also:

• ISolver.get_unsat_assumptions()

get_model

public IResponse get_model()

Alt-Ergo answers get-model in assert mode after a check

Specified by:

get_model in interface ISolver

Overrides:

get_model in class AbstractSolver

Returns:

a model, unsupported, or an SMT error response

See Also:

• ISolver.get_model()

get_assignment

public IResponse get_assignment()

Alt-Ergo answers get-assignment in assert mode after a check. Sent through sendCommand, which reads Alt-Ergo's reply up to the echo after it (the base class reads one line, which may be a blank line Alt-Ergo writes around replies)

Specified by:

get_assignment in interface ISolver

Overrides:

get_assignment in class AbstractSolver

Returns:

a list of name–Boolean pairs, unsupported, or an SMT error response

See Also:

• ISolver.get_assignment()