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
14       input.
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
50                  assertions after check  is  allowed.   Commands  (push)  and
51                  (pop) 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
82       developers are  Bruno  Dutertre  <bruno@csl.sri.com>,  Dejan  Jovanovic
83       <dejan@csl.sri.com>,  Ian A. Mason <iam@csl.sri.com>, and Stephane Gra‐
84       ham-Lengrand <stephane.graham-lengrand@sri.com>.
85
86
87
88Yices 2.6.2                       Marc h 2020                         YICES(1)
Impressum