Merge pull request #432 from ethereum/smt_readme

Add smtCallback to README

README.md

@@ -44,11 +44,14 @@ There are two ways to use `solc`:
 
 The high-level API consists of a single method, `compile`, which expects the [Compiler Standard Input and Output JSON](https://solidity.readthedocs.io/en/v0.5.0/using-the-compiler.html#compiler-input-and-output-json-description).
 
-It also accepts an optional callback function to resolve unmet dependencies. This callback receives a path and must synchronously return either an error or the content of the dependency as a string.
-It cannot be used together with callback-based, asynchronous, filesystem access. A workaround is to collect the names of dependencies, return an error, and keep re-running the compiler until all
-of them are resolved.
+It also accepts an optional set of callback functions, which include the ``import`` and the ``smtSolver`` callbacks.
+Starting 0.6.0 it only accepts an object in place of the callback to supply the callbacks.
 
-Starting 0.5.12 it also accepts an object in place of the callback to supply different kind of callbacks, however only file imports are supported.
+The ``import`` callback function is used to resolve unmet dependencies.
+This callback receives a path and must synchronously return either an error or the content of the dependency
+as a string.  It cannot be used together with callback-based, asynchronous,
+filesystem access. A workaround is to collect the names of dependencies, return
+an error, and keep re-running the compiler until all of them are resolved.
 
 #### Example usage without the import callback
 
@@ -115,10 +118,7 @@ function findImports(path) {
   else return { error: 'File not found' };
 }
 
-// Current syntax
-var output = JSON.parse(solc.compile(JSON.stringify(input), findImports));
-
-// New syntax (supported from 0.5.12)
+// New syntax (supported from 0.5.12, mandatory from 0.6.0)
 var output = JSON.parse(
   solc.compile(JSON.stringify(input), { import: findImports })
 );
@@ -133,6 +133,37 @@ for (var contractName in output.contracts['test.sol']) {
 }
 ```
 
+The ``smtSolver`` callback function is used to solve SMT queries generated by
+Solidity's SMTChecker.  If you have an SMT solver installed locally, it can
+be used to solve the given queries, where the callback must synchronously
+return either an error or the result from the solver.  A default
+``smtSolver`` callback is distributed by ``solc-js``, which relies on either
+Z3 or CVC4 being installed locally.
+
+#### Example usage with smtSolver callback
+
+```javascript
+var solc = require('solc');
+var smt = require('smtsolver');
+// Note that this example only works via node and not in the browser.
+
+var input = {
+  language: 'Solidity',
+  sources: {
+    'test.sol': {
+      content: 'pragma experimental SMTChecker; contract C { function f(uint x) public { assert(x > 0); } }'
+    }
+  }
+};
+
+var output = JSON.parse(
+  solc.compile(JSON.stringify(input), { smtSolver: smt.smtSolver })
+);
+
+```
+The assertion is clearly false, and an ``assertion failure`` warning
+should be returned.
+
 #### Low-level API
 
 The low-level API is as follows: