docs/rosette: More intro of SMT-LIB backend

As the intro paragraph (now) says:
> This section will introduce the SMT-LIB functional backend and what changes are needed...

The example is intended to be read without prior knowledge of the SMT-LIB backend, but the previous version glossed over a lot and instead focused on *just* what was changed.
This version should now be easier to follow without prior knowledge, while still being able to learn enough about the `Smt` version to adapt it to a different s-expression target that isn't Rosette.
Also adds a few `literalinclude`s of smtlib.cc, which is now copied to `docs/source/generated` along with producing the rosette diff on the fly (which now also has up to 20 lines of context, enabling the full `Module::write()` diff to be literal included).

Makefile

@@ -996,6 +996,18 @@ docs/source/cell/word_add.rst: $(TARGETS) $(EXTRA_TARGETS)
 docs/source/generated/cells.json: docs/source/generated $(TARGETS) $(EXTRA_TARGETS)
 	$(Q) ./$(PROGRAM_PREFIX)yosys -p 'help -dump-cells-json $@'
 
+docs/source/generated/%.cc: backends/%.cc
+	$(Q) mkdir -p $(@D)
+	$(Q) cp $< $@
+
+# diff returns exit code 1 if the files are different, but it's not an error
+docs/source/generated/functional/rosette.diff: backends/functional/smtlib.cc backends/functional/smtlib_rosette.cc
+	$(Q) mkdir -p $(@D)
+	$(Q) diff -U 20 $^ > $@ || exit 0
+
+PHONY: docs/gen/functional_ir
+docs/gen/functional_ir: docs/source/generated/functional/smtlib.cc docs/source/generated/functional/rosette.diff
+
 PHONY: docs/gen docs/usage docs/reqs
 docs/gen: $(TARGETS)
 	$(Q) $(MAKE) -C docs gen
@@ -1031,7 +1043,7 @@ docs/reqs:
 	$(Q) $(MAKE) -C docs reqs
 
 .PHONY: docs/prep
-docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage
+docs/prep: docs/source/cmd/abc.rst docs/source/generated/cells.json docs/gen docs/usage docs/gen/functional_ir
 
 DOC_TARGET ?= html
 docs: docs/prep