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
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 also has a more user-friendly mode for interactive use. To use yices interactively, give 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
yices -v 2 -st input.ys
-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:
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
(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
-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 instructs yices to use a SMT-LIB parser. Example:
yices -smt < file.smt
-smt is used.
Better error messages are produced when the option
-tc is used with SMT-LIB benchmarks.