the rosette guide

jamestiotio · Oct 26, 2014 · 076c43f · 076c43f
1 parent 298c24f
commit 076c43f
Show file tree

Hide file tree

Showing 76 changed files with 5,266 additions and 28 deletions.
diff --git a/LICENSE b/LICENSE
@@ -1,6 +1,8 @@
 Copyright (c) 2014, Regents of the University of California
 All rights reserved.
 
+Authored by Emina Torlak.
+
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
 

diff --git a/README.md b/README.md
@@ -3,7 +3,7 @@ rosette
 
 This repository includes the source code and default solver binaries
 for the Rosette solver-aided host language, as well as several example
-solver-aided DSLs and demos.
+solver-aided DSLs.
 
 ### Installing Rosette
 
@@ -21,31 +21,23 @@ solver-aided DSLs and demos.
 
   `$ git clone git@github.com:emina/rosette.git`
 
+* Use Racket's `raco` tool to install Rosette as one of your Racket collections:
+  `$ cd rosette`
+  `$ raco link rosette`
+  `$ raco setup -l rosette`
+
 * Rosette ships with the [Kodkod](http://alloy.mit.edu/kodkod/) solver 
-  binaries, but it also supports [Z3](http://z3.codeplex.com).  To use Z3, 
+  binaries, but it also supports [Z3](http://z3.codeplex.com) and 
+  [CVC4]{http://cvc4.cs.nyu.edu/web/}.  To use Z3 or CVC4, 
   download (or build) the binaries for your system and put them in the `rosette/bin` directory.
 
-  `$ ls rosette/bin`  
-  `kodkod z3`
-
-* Use Racket's raco tool to install Rosette as one of your Racket
-  collections:
-
-  `$ cd rosette`  
-  `$ raco link rosette`  
-
 ### Executing Rosette programs
 
 * Open the target program in DrRacket (e.g., [`rosette/sdsl/fsm/demo.rkt`](https://github.com/emina/rosette/blob/master/sdsl/fsm/demo.rkt))
   and hit run!
 
-* The first time you run any program in Rosette, DrRacket will have to
-  compile the Rosette implementation, which may take a few seconds.
-  Subsequent compilations should be fast.
-
 * DrRacket is the preferred way to execute Rosette programs.  If you
-  need to use the command line, make sure to first compile the program
-  (and the Rosette implementation):
+  need to use the command line, make sure to first compile the program:
 
   `$ raco make <your program>`  
   `$ racket -r <your program>`  
@@ -73,10 +65,12 @@ solver-aided DSLs and demos.
   unsafe constructs.  In the best case, such a program will fail with
   an exception if a symbolic value flows to a construct that does not
   support it.  In the worst case, it will continue executing with
-  incorrect semantics.
+  incorrect semantics or cause more serious problems (e.g., data loss if 
+  it writes to a file).
 
 * For more on Rosette, see:
 
+  - Emina Torlak.  [_The Rosette Guide_](https://github.com/emina/rosette/doc/guide/html/index.html).
   - Emina Torlak and Rastislav Bodik. [_A lightweight symbolic
   virtual machine for solver-aided host languages._](http://people.csail.mit.edu/emina/pubs/rosette.pldi14.pdf) In PLDI'14.
 

diff --git a/doc/guide/html/autobib.css b/doc/guide/html/autobib.css
@@ -0,0 +1,9 @@
+
+.AutoBibliography p {
+  padding-left: 1em;
+  text-indent: -1em;
+}
+
+.AutoBibliography td {
+  vertical-align: text-top;
+}
diff --git a/doc/guide/html/ch_built-in-datatypes.html b/doc/guide/html/ch_built-in-datatypes.html
@@ -0,0 +1,8 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"/><title>4&nbsp;Built-In Datatypes</title><link rel="stylesheet" type="text/css" href="scribble.css" title="default"/><link rel="stylesheet" type="text/css" href="manual-style.css" title="default"/><link rel="stylesheet" type="text/css" href="manual-racket.css" title="default"/><link rel="stylesheet" type="text/css" href="guide.css" title="default"/><script type="text/javascript" src="scribble-common.js"></script><script type="text/javascript" src="manual-racket.js"></script><!--[if IE 6]><style type="text/css">.SIEHidden { overflow: hidden; }</style><![endif]--></head><body id="scribble-racket-lang-org"><div class="tocset"><div class="tocview"><div class="tocviewlist tocviewlisttopspace"><div class="tocviewtitle"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,&quot;tocview_0&quot;);">&#9658;</a></td><td></td><td><a href="index.html" class="tocviewlink" data-pltdoc="x">The Rosette Guide</a></td></tr></table></div><div class="tocviewsublisttop" style="display: none;" id="tocview_0"><table cellspacing="0" cellpadding="0"><tr><td align="right">1&nbsp;</td><td><a href="ch_getting-started.html" class="tocviewlink" data-pltdoc="x">Getting Started</a></td></tr><tr><td align="right">2&nbsp;</td><td><a href="ch_essentials.html" class="tocviewlink" data-pltdoc="x">Rosette Essentials</a></td></tr><tr><td align="right">3&nbsp;</td><td><a href="ch_syntactic-forms.html" class="tocviewlink" data-pltdoc="x">Syntactic Forms</a></td></tr><tr><td align="right">4&nbsp;</td><td><a href="" class="tocviewselflink" data-pltdoc="x">Built-<wbr></wbr>In Datatypes</a></td></tr><tr><td align="right">5&nbsp;</td><td><a href="ch_programmer-defined-datatypes.html" class="tocviewlink" data-pltdoc="x">Programmer-<wbr></wbr>Defined Datatypes</a></td></tr><tr><td align="right">6&nbsp;</td><td><a href="ch_libraries.html" class="tocviewlink" data-pltdoc="x">Libraries</a></td></tr><tr><td align="right">7&nbsp;</td><td><a href="ch_symbolic-reflection.html" class="tocviewlink" data-pltdoc="x">Symbolic Reflection</a></td></tr><tr><td align="right">8&nbsp;</td><td><a href="ch_unsafe.html" class="tocviewlink" data-pltdoc="x">Unsafe Operations</a></td></tr><tr><td align="right">9&nbsp;</td><td><a href="refs.html" class="tocviewlink" data-pltdoc="x">References</a></td></tr><tr><td align="right"></td><td><a href="doc-index.html" class="tocviewlink" data-pltdoc="x">Index</a></td></tr></table></div></div><div class="tocviewlist"><table cellspacing="0" cellpadding="0"><tr><td style="width: 1em;"><a href="javascript:void(0);" title="Expand/Collapse" class="tocviewtoggle" onclick="TocviewToggle(this,&quot;tocview_1&quot;);">&#9660;</a></td><td>4&nbsp;</td><td><a href="" class="tocviewselflink" data-pltdoc="x">Built-<wbr></wbr>In Datatypes</a></td></tr></table><div class="tocviewsublistbottom" style="display: block;" id="tocview_1"><table cellspacing="0" cellpadding="0"><tr><td align="right">4.1&nbsp;</td><td><a href="sec_primitives.html" class="tocviewlink" data-pltdoc="x">Booleans and Numbers</a></td></tr><tr><td align="right">4.2&nbsp;</td><td><a href="sec_equality.html" class="tocviewlink" data-pltdoc="x">Equality</a></td></tr><tr><td align="right">4.3&nbsp;</td><td><a href="sec_pair.html" class="tocviewlink" data-pltdoc="x">Pairs and Lists</a></td></tr><tr><td align="right">4.4&nbsp;</td><td><a href="sec_vec.html" class="tocviewlink" data-pltdoc="x">Vectors</a></td></tr><tr><td align="right">4.5&nbsp;</td><td><a href="sec_box.html" class="tocviewlink" data-pltdoc="x">Boxes</a></td></tr><tr><td align="right">4.6&nbsp;</td><td><a href="sec_proc.html" class="tocviewlink" data-pltdoc="x">Procedures</a></td></tr><tr><td align="right">4.7&nbsp;</td><td><a href="sec_solvers-and-solutions.html" class="tocviewlink" data-pltdoc="x">Solvers and Solutions</a></td></tr></table></div></div></div></div><div class="maincolumn"><div class="main"><div class="versionbox"><span class="version">6.1</span></div><div class="navsettop"><span class="navleft"><div class="nosearchform"></div>&nbsp;&nbsp;</span><span class="navright">&nbsp;&nbsp;<a href="ch_syntactic-forms_rosette.html" title="backward to &quot;3.2 Solver-Aided Forms&quot;" data-pltdoc="x">&larr; prev</a>&nbsp;&nbsp;<a href="index.html" title="up to &quot;The Rosette Guide&quot;" data-pltdoc="x">up</a>&nbsp;&nbsp;<a href="sec_primitives.html" title="forward to &quot;4.1 Booleans and Numbers&quot;" data-pltdoc="x">next &rarr;</a></span>&nbsp;</div><h3>4<tt>&nbsp;</tt><a name="(part._ch~3abuilt-in-datatypes)"></a>Built-In Datatypes</h3><p>The <a href="ch_syntactic-forms.html" data-pltdoc="x">previous chapter</a> describes the
+Racket syntax forms that are <a href="ch_syntactic-forms.html#%28tech._lifted._construct%29" class="techoutside" data-pltdoc="x"><span class="techinside">lifted</span></a> by Rosette to
+work on symbolic values.
+This chapter describes the lifted datatypes and their corresponding operations. Most
+lifted operations retain their Racket semantics, with the exception of
+numeric functions (Section <a href="sec_primitives.html" data-pltdoc="x">4.1</a>) and
+equality predicates (Section <a href="sec_equality.html" data-pltdoc="x">4.2</a>).</p><table cellspacing="0" cellpadding="0"><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_primitives.html" class="toclink" data-pltdoc="x">4.1<span class="hspace">&nbsp;</span>Booleans and Numbers</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_equality.html" class="toclink" data-pltdoc="x">4.2<span class="hspace">&nbsp;</span>Equality</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_pair.html" class="toclink" data-pltdoc="x">4.3<span class="hspace">&nbsp;</span>Pairs and Lists</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_vec.html" class="toclink" data-pltdoc="x">4.4<span class="hspace">&nbsp;</span>Vectors</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_box.html" class="toclink" data-pltdoc="x">4.5<span class="hspace">&nbsp;</span>Boxes</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_proc.html" class="toclink" data-pltdoc="x">4.6<span class="hspace">&nbsp;</span>Procedures</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_solvers-and-solutions.html" class="toclink" data-pltdoc="x">4.7<span class="hspace">&nbsp;</span>Solvers and Solutions</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_solvers-and-solutions.html#%28part._.The_.Solver_.Interface_and_.Classes%29" class="toclink" data-pltdoc="x">4.7.1<span class="hspace">&nbsp;</span>The Solver Interface and Classes</a></p></td></tr><tr><td><p><span class="hspace">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;</span><a href="sec_solvers-and-solutions.html#%28part._.Satisfiable_and_.Unsatisfiable_.Solutions%29" class="toclink" data-pltdoc="x">4.7.2<span class="hspace">&nbsp;</span>Satisfiable and Unsatisfiable Solutions</a></p></td></tr></table><div class="navsetbottom"><span class="navleft"><div class="nosearchform"></div>&nbsp;&nbsp;</span><span class="navright">&nbsp;&nbsp;<a href="ch_syntactic-forms_rosette.html" title="backward to &quot;3.2 Solver-Aided Forms&quot;" data-pltdoc="x">&larr; prev</a>&nbsp;&nbsp;<a href="index.html" title="up to &quot;The Rosette Guide&quot;" data-pltdoc="x">up</a>&nbsp;&nbsp;<a href="sec_primitives.html" title="forward to &quot;4.1 Booleans and Numbers&quot;" data-pltdoc="x">next &rarr;</a></span>&nbsp;</div></div></div><div id="contextindicator">&nbsp;</div></body></html>