Home	•	Intro	•	Docs	•	Wiki	•	FAQ	•	Download	-	Mail	•	Awards	•	Status	•	FM Tools

Running Yices 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

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	•	Intro	•	Docs	•	Wiki	•	FAQ	•	Download	-	Mail	•	Awards	•	Status	•	FM Tools

Last modified: Mon 28 Aug 2006 19:19 PDT