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

SEE ALSO

66       yices-sat(1), yices-smt(1), yices-smt2(1)
67
68       To  report  bugs  and  to  get  the  full  documentation,  please visit
69       http://yices.csl.sri.com.
70

AUTHORS

72       Copyright (C) SRI International.
73
74       Yices is developed at  SRI's  Computer  Science  Laboratory.  The  main
75       developers  are  Bruno Dutertre <bruno@csl.sri.com> and Dejan Jovanovic
76       <dejan@csl.sri.com>.
77
78
79
80Yices 2.6.1                      October 2018                         YICES(1)
Impressum