Linux and UNIX Man Pages

Linux & Unix Commands - Search Man Pages

cvc3(1) [debian man page]

CVC3(1) 						      General Commands Manual							   CVC3(1)

NAME
cvc3 - automatic SMT theorem prover SYNOPSIS
cvc3 [option]... [filename] DESCRIPTION
CVC3 is an automated validity checker for a many-sorted (typed) first-order logic with built-in theories, including some support for quan- tifiers, partial functions, and predicate subtypes. The current built-in theories are the theories of o equality over free (aka uninterpreted) function and predicate symbols, o real and integer linear arithmetic (with some support for non-linear arithmetic), o bit vectors, o arrays, o tuples, o records, o user-defined inductive datatypes. CVC3 operates on files in the CVC Presentation Input Language or the SMTLIB input language. If no input file is given on the command line, CVC3 reads standard input. OPTIONS
Only a few of the most frequently used options are given below. For more details, see CVC3's built-in help (cvc3 -help) or the CVC3 web- site. -h[elp] List all of the options for controlling CVC3. Boolean options are marked (b). They are enabled by prefixing with + and disabled by prefixing with -. In the help output, the current setting is given. For example, the output lists (b) -interactive Interactive mode Indicating that interactive mode is disabled. to enable interactive mode, the option +interactive is therefore used. Other options are marked (s) for string arguments, or (i) for integer arguments. -version Print the version of CVC3 and exit. -lang (presentation|smtlib|internal) Select the input language used. The default is presentation. +int[eractive] Enable interactive mode. Commands are read from standard input and processed immediately. +stats Print run-time statistics. -timeout t Automatically terminate CVC3 after t seconds. SEE ALSO
CVC3 website: http://www.cs.nyu.edu/acsys/cvc3/ SMTLIB website: http://combination.cs.uiowa.edu/smtlib/ AUTHOR
CVC3 was written by Clark Barrett, Cesare Tinelli, Alexander Fuchs, Yeting Ge, George Hagen, Dejan Jovanovic, Sergey Berezin, Cristian Cadar, Jake Donham, Vijay Ganesh, Deepak Goyal, Ying Hu, Sean McLaughlin, Mehul Trivedi, Michael Veksler, Daniel Wichs, Mark Zavislak, and Jim Zhuang. This manual page was written by Dan Sheridan <djs@adelard.com>, for Ubuntu (but may be used by others). January 16, 2008 CVC3(1)

Check Out this Related Man Page

jrunscript(1)						      General Commands Manual						     jrunscript(1)

NAME
jrunscript - command line script shell SYNOPSIS
jrunscript [ options ] [ arguments... ] PARAMETERS
options Options, if used, should follow immediately after the command name. arguments Arguments, if used, should follow immediately after options or command name. DESCRIPTION
jrunscript is a command line script shell. jrunscript supports both an interactive (read-eval-print) mode and a batch (-f option) mode of script execution. This is a scripting language independent shell. By default, JavaScript is the language used, but the -l option can be used to specify a different language. Through Java to scripting language communication, jrunscript supports "exploratory programming" style. NOTE: This tool is experimental and may not be available in future versions of the JDK. OPTIONS
-classpath path Specify where to find the user's .class files that are accessed by the script. -cp path This is a synonym for -classpath path -Dname=value Set a Java system property. -Jflag Pass flag directly to the Java virtual machine on which jrunscript is run. -l language Use the specified scripting language. By default, JavaScript is used. Note that to use other scripting languages, you also need to spec- ify the corresponding script engine's jar file using -cp or -classpath option. -e script Evaluate the given script. This option can be used to run "one liner" scripts specified completely on the command line. -encoding encoding Specify the character encoding used while reading script files. -f script-file Evaluate the given script file (batch mode). -f - Read and evaluate a script from standard input (interactive mode). -help Output help message and exit. -? Output help message and exit. -q List all script engines available and exit. ARGUMENTS
If [arguments...] are present and if no -e or -f option is used, then the first argument is the script file and the rest of the arguments, if any, are passed as script arguments. If [arguments..] and -e or -f option are used, then all [arguments..] are passed as script argu- ments. If [arguments..], -e and -f are missing, interactive mode is used. Script arguments are available to a script in an engine variable named "arguments" of type String array. EXAMPLES
Executing inline scripts jrunscript -e "print('hello world')" jrunscript -e "cat('http://java.sun.com')" Use specified language and evaluate given script file jrunscript -l js -f test.js Interactive mode jrunscript js>print('hello world'); hello world js>34 + 55 89 js> thread(function() { print('hello world'); } hello world js> Run script file with script arguments jrunscript test.js arg1 arg2 arg3 test.js is script file to execute and arg1, arg2 and arg3 are passed to script as script arguments. Script can access these using "argu- ments" array. SEE ALSO
If JavaScript is used, then before evaluating any user defined script, jrunscript initializes certain built-in functions and objects. These JavaScript built-ins are documented in jsdocs. 06 Aug 2006 jrunscript(1)
Man Page

Featured Tech Videos