Home • Docs • Download • FM Tools
Yices

Yices 1 is no longer maintained. You can still download it and use it, but we do not provide support for Yices 1.

Our more recent Yices 2 solver is here

Running Yices1 from the Command Line

Introduction

The executable name is yices. It reads the input from standard input and prints the results on standard output. Errors and (progress) messages are sent to standard error. If a file is present in the command line, then yices reads the file instead of the standard input.

Reading from standard input: 

yices < input.ys

Reading from a file: 

yices input.ys

Yices also has a more user-friendly mode for interactive use. To use yices interactively, give the option -i: 

yices -i

The option -v num sets the amount of progress messages produced by yices. Example:

yices -v 2 input.ys

Statistics can be obtained using the option -st.

yices -v 2 -st input.ys

The option -e can be used to force yices to diplay models and unsatisfiable cores. Example:

yices -v 1 -e input.ys

Yices has many more options, to see a full list of all the options, type: 

yices --help

Type Checker

By default, Yices assumes the input is type correct. If this is not the case, Yices may print a type error message, or even produce a wrong result. Users should use the option -tc, when they are not sure whether their input is type correct or not. When this option is provided, Yices will execute a simple type checker to validate the input. Example:

yices -v 1 -tc input.ys

Limit on Recursive Function Expansion

Yices has limited support for recursive functions. For example, it is possible to define factorial as follows 
(define fact::(-> nat nat) (lambda (x::nat) (if (= 0 x) 1 (* x (fact (- x 1))))))

To prevent infinite loops, there's a limit on function expansion. By default, the limit is 30. With this limit, (fact 29) is fully expanded, but (fact 30) is not, which results in an error. Command-line option -nr can be used to change the recursion limit. Example: 

yices -nr 40

DIMACS

Yices can be used also as a regular SAT solver. The option -d instructs yices to use a parser for the DIMACS cnf format. Example:

yices -v 2 -d -e bw_large.c.cnf

Yices also supports the MaxWalkSAT wcnf format. The option -ms forces yices to compute the maximal satisfying assignment. If the option -ms is not provided, then yices ignores the weights associated with each clause. If the option -ms is provided, but the input file is not in the wcnf format, then yices assigns weight one to all clauses.

yices -v 2 -d -ms -e test.wcnf

If yices is interrupted during the computation of the maximal satisfying assignment, then it returns the best model found so far when the option -e is provided.

The user can specify hard constraints by defining an upper bound for the weights. That is, any weight greater than or equal to the given bound is considered to have infinite weight. The option -mw num sets this bound. Example:

yices -v 2 -d -ms -e -mw 200 test.wcnf

SMT-LIB format

Yices also supports the SMT-LIB format. The option -smt instructs yices to use a SMT-LIB parser. Example:

yices -smt < file.smt

Warning:
The models are displayed using Yices syntax even when the option -smt is used.
Remarks:
In Yices, SMT-LIB arrays are represented as functions.

Better error messages are produced when the option -tc is used with SMT-LIB benchmarks.

Home • Docs • Download • FM Tools