Package org.smtlib.solvers

Class Solver_yices2_2_6

java.lang.Object

org.smtlib.AbstractSolver

org.smtlib.solvers.Solver_smt

org.smtlib.solvers.Solver_yices2

org.smtlib.solvers.Solver_yices2_2_6

All Implemented Interfaces:

ISolver

public class Solver_yices2_2_6
extends Solver_yices2

yices2 2.6.5: by default it answers get-model in yices's own model format, not SMT-LIB's; with --smt2-model-format it answers (model (define-fun ...) ...), whose wrapper AbstractSolver#modelResponse removes. yices2 2.7.0 answers in SMT-LIB format and rejects the flag.

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 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_yices2_2_6(SMT.Configuration smtConfig, String command)
Solver_yices2_2_6(SMT.Configuration smtConfig, String[] command)

Method Summary

Modifier and Type	Method	Description
String[]	cmd(String exec)

Methods inherited from class org.smtlib.solvers.Solver_yices2

echo, get_assignment, get_info, get_model, get_unsat_assumptions, get_unsat_core, get_value, lineNumberPatterns, selfReportsImmediateExit, start

Methods inherited from class org.smtlib.solvers.Solver_smt

prompt, translate

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, errorStopsSolver, execute, executePipelined, exit, exitedResponse, finishPipelined, forceExit, get_assertions, get_option, get_proof, hasPending, inSatMode, interrupt, inUnsatMode, isFlatResponse, isTimeLimitResponse, logSolverDiagnostics, modelResponse, nextSolverLine, normalizeForTesting, outOfStep, parseResponse, pipelines, pop, proofResponse, push, readPipelined, recordChange, reportsEarlierLines, reportSeedIgnored, requireNoChangeSinceCheck, requireOptionEnabled, requireSatOrUnknown, requireUnsat, reset, reset_assertions, responseEnd, sendChange, sendCommand, sendExitCommand, sendFailure, sendFailure, sendPipelined, sendScriptText, sendSeed, set_info, set_logic, set_option, set_option_impl, setSourceLine, shapeOf, smt, solverName, solverPrintsSuccess, successOrEmpty, timeLimitResponse, timeLimitResponseAfterExit, 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, execute, exit, forceExit, get_assertions, get_option, get_proof, pop, push, reset, reset_assertions, set_info, set_logic, set_option, setSourceLine, smt, solverName

Constructor Details

Solver_yices2_2_6

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

Solver_yices2_2_6

public Solver_yices2_2_6(SMT.Configuration smtConfig,
 String command)

Method Details

cmd

public String[] cmd(String exec)

Overrides:

cmd in class Solver_yices2