1YICES(1)                         User Commands                        YICES(1)
2
3
4

NAME

6       yices - the Yices SMT solver for the Yices language
7

SYNOPSIS

9       yices [ options ] [ file ]
10

DESCRIPTION

12       Runs the Yices SMT solver. The input must be in the Yices specification
13       language. If no file is given, Yices reads commands from  standard  in‐
14       put.
15

OPTIONS

17       --version, -V
18              Display version and exit.
19
20       --help, -h
21              Display a short help summary.
22
23       --verbosity=level, -v level
24              Set the verbosity level (default = 0).
25
26       --logic=name
27              Configure Yices for a specific logic.
28
29              The  name  must be either an SMT-LIB logic name (e.g., QF_UFLIA)
30              or the special symbol NONE to select propositional logic.
31
32       --arith-solver=solver
33              Select the arithmetic solver.
34
35              The solver may be either  simplex  or  floyd-warshall  or  auto.
36              This  option  is  ignored  unless  the logic is either QF_RDL or
37              QF_IDL.
38
39       --mode=mode
40              Select the usage mode.
41
42              The mode  maybe  one-shot  or  multi-checks  or  interactive  or
43              push-pop or ef.
44
45              •   one-shot:  only  one  call to (check) is allowed.  No asser‐
46                  tions are allowed after (check).  Commands (push) and  (pop)
47                  are not supported.
48
49              •   multi-checks: several calls (check) are allowed.  Adding as‐
50                  sertions after check is allowed.  Commands (push) and  (pop)
51                  are not supported.
52
53              •   push-pop:  like  multi-check but with support for (push) and
54                  (pop).
55
56              •   interactive: like push-pop.  In addition, Yices restores the
57                  context to a clean state if (check) is interrupted.
58
59              •   ef:   enable  the  exist-forall  solver,  that  is,  command
60                  (ef-solve) can be used.  This is like one-shot in that  only
61                  one call to (ef-solve) is allowed.
62
63              The default mode is push-pop.
64
65       --mcsat
66              Force use of the MCSAT solver.
67
68       --print-success
69              Print  ok  after  every  command  that  would  otherwise execute
70              silently.
71

SEE ALSO

73       yices-sat(1), yices-smt(1), yices-smt2(1)
74
75       To report  bugs  and  to  get  the  full  documentation,  please  visit
76       http://yices.csl.sri.com.
77

AUTHORS

79       Copyright (C) SRI International.
80
81       Yices  is  developed at SRI's Computer Science Laboratory. The main de‐
82       velopers are Bruno Dutertre <bruno@csl.sri.com>, Dejan  Jovanovic  <de‐
83       jan@csl.sri.com>,  Ian A. Mason <iam@csl.sri.com>, and Stephane Graham-
84       Lengrand <stephane.graham-lengrand@sri.com>.
85
86
87
88Yices 2.6.4                      October 2021                         YICES(1)
Impressum