Add interactive "Run" buttons to SMT-LIBv2 code blocks

appjs/index.html

@@ -588,6 +588,36 @@ <h2>CVC5 SMT Solver</h2>
         }
     </script>
     <script async src="cvc5.js"></script>
+
+    <script>
+        (function () {
+            // Parse #smt=... from the URL hash
+            var hash = window.location.hash;
+            if (!hash || hash.indexOf('#smt=') !== 0) return;
+
+            var code;
+            try {
+            code = decodeURIComponent(hash.slice(5)); // strip leading "#smt="
+            } catch (e) {
+            return; // malformed encoding — do nothing
+            }
+            if (!code) return;
+
+            // Fill the editor immediately (even before WASM is ready)
+            var editor = document.getElementById('smt-editor');
+            if (editor) editor.value = code;
+
+            // Wait for the WASM module, then run
+            function tryRun() {
+            if (typeof moduleLoaded === 'undefined' || !moduleLoaded) {
+                setTimeout(tryRun, 50);
+                return;
+            }
+            runSolver();
+            }
+            tryRun();
+        })();
+    </script>
 </body>
 
 </html>

tutorials/beginners/static/js/theme.js

@@ -1 +1,168 @@
-!function(n){var e={};function t(i){if(e[i])return e[i].exports;var o=e[i]={i:i,l:!1,exports:{}};return n[i].call(o.exports,o,o.exports,t),o.l=!0,o.exports}t.m=n,t.c=e,t.d=function(n,e,i){t.o(n,e)||Object.defineProperty(n,e,{enumerable:!0,get:i})},t.r=function(n){"undefined"!=typeof Symbol&&Symbol.toStringTag&&Object.defineProperty(n,Symbol.toStringTag,{value:"Module"}),Object.defineProperty(n,"__esModule",{value:!0})},t.t=function(n,e){if(1&e&&(n=t(n)),8&e)return n;if(4&e&&"object"==typeof n&&n&&n.__esModule)return n;var i=Object.create(null);if(t.r(i),Object.defineProperty(i,"default",{enumerable:!0,value:n}),2&e&&"string"!=typeof n)for(var o in n)t.d(i,o,function(e){return n[e]}.bind(null,o));return i},t.n=function(n){var e=n&&n.__esModule?function(){return n.default}:function(){return n};return t.d(e,"a",e),e},t.o=function(n,e){return Object.prototype.hasOwnProperty.call(n,e)},t.p="",t(t.s=0)}([function(n,e,t){t(1),n.exports=t(3)},function(n,e,t){(function(){var e="undefined"!=typeof window?window.jQuery:t(2);n.exports.ThemeNav={navBar:null,win:null,winScroll:!1,winResize:!1,linkScroll:!1,winPosition:0,winHeight:null,docHeight:null,isRunning:!1,enable:function(n){var t=this;void 0===n&&(n=!0),t.isRunning||(t.isRunning=!0,e((function(e){t.init(e),t.reset(),t.win.on("hashchange",t.reset),n&&t.win.on("scroll",(function(){t.linkScroll||t.winScroll||(t.winScroll=!0,requestAnimationFrame((function(){t.onScroll()})))})),t.win.on("resize",(function(){t.winResize||(t.winResize=!0,requestAnimationFrame((function(){t.onResize()})))})),t.onResize()})))},enableSticky:function(){this.enable(!0)},init:function(n){n(document);var e=this;this.navBar=n("div.wy-side-scroll:first"),this.win=n(window),n(document).on("click","[data-toggle='wy-nav-top']",(function(){n("[data-toggle='wy-nav-shift']").toggleClass("shift"),n("[data-toggle='rst-versions']").toggleClass("shift")})).on("click",".wy-menu-vertical .current ul li a",(function(){var t=n(this);n("[data-toggle='wy-nav-shift']").removeClass("shift"),n("[data-toggle='rst-versions']").toggleClass("shift"),e.toggleCurrent(t),e.hashChange()})).on("click","[data-toggle='rst-current-version']",(function(){n("[data-toggle='rst-versions']").toggleClass("shift-up")})),n("table.docutils:not(.field-list,.footnote,.citation)").wrap("<div class='wy-table-responsive'></div>"),n("table.docutils.footnote").wrap("<div class='wy-table-responsive footnote'></div>"),n("table.docutils.citation").wrap("<div class='wy-table-responsive citation'></div>"),n(".wy-menu-vertical ul").not(".simple").siblings("a").each((function(){var t=n(this);expand=n('<button class="toctree-expand" title="Open/close menu"></button>'),expand.on("click",(function(n){return e.toggleCurrent(t),n.stopPropagation(),!1})),t.prepend(expand)}))},reset:function(){var n=encodeURI(window.location.hash)||"#";try{var e=$(".wy-menu-vertical"),t=e.find('[href="'+n+'"]');if(0===t.length){var i=$('.document [id="'+n.substring(1)+'"]').closest("div.section");0===(t=e.find('[href="#'+i.attr("id")+'"]')).length&&(t=e.find('[href="#"]'))}if(t.length>0){$(".wy-menu-vertical .current").removeClass("current").attr("aria-expanded","false"),t.addClass("current").attr("aria-expanded","true"),t.closest("li.toctree-l1").parent().addClass("current").attr("aria-expanded","true");for(let n=1;n<=10;n++)t.closest("li.toctree-l"+n).addClass("current").attr("aria-expanded","true");t[0].scrollIntoView()}}catch(n){console.log("Error expanding nav for anchor",n)}},onScroll:function(){this.winScroll=!1;var n=this.win.scrollTop(),e=n+this.winHeight,t=this.navBar.scrollTop()+(n-this.winPosition);n<0||e>this.docHeight||(this.navBar.scrollTop(t),this.winPosition=n)},onResize:function(){this.winResize=!1,this.winHeight=this.win.height(),this.docHeight=$(document).height()},hashChange:function(){this.linkScroll=!0,this.win.one("hashchange",(function(){this.linkScroll=!1}))},toggleCurrent:function(n){var e=n.closest("li");e.siblings("li.current").removeClass("current").attr("aria-expanded","false"),e.siblings().find("li.current").removeClass("current").attr("aria-expanded","false");var t=e.find("> ul li");t.length&&(t.removeClass("current").attr("aria-expanded","false"),e.toggleClass("current").attr("aria-expanded",(function(n,e){return"true"==e?"false":"true"})))}},"undefined"!=typeof window&&(window.SphinxRtdTheme={Navigation:n.exports.ThemeNav,StickyNav:n.exports.ThemeNav}),function(){for(var n=0,e=["ms","moz","webkit","o"],t=0;t<e.length&&!window.requestAnimationFrame;++t)window.requestAnimationFrame=window[e[t]+"RequestAnimationFrame"],window.cancelAnimationFrame=window[e[t]+"CancelAnimationFrame"]||window[e[t]+"CancelRequestAnimationFrame"];window.requestAnimationFrame||(window.requestAnimationFrame=function(e,t){var i=(new Date).getTime(),o=Math.max(0,16-(i-n)),r=window.setTimeout((function(){e(i+o)}),o);return n=i+o,r}),window.cancelAnimationFrame||(window.cancelAnimationFrame=function(n){clearTimeout(n)})}()}).call(window)},function(n,e){n.exports=jQuery},function(n,e,t){}]);
+! function(n) {
+    var e = {};
+
+    function t(i) {
+        if (e[i]) return e[i].exports;
+        var o = e[i] = {
+            i: i,
+            l: !1,
+            exports: {}
+        };
+        return n[i].call(o.exports, o, o.exports, t), o.l = !0, o.exports
+    }
+    t.m = n, t.c = e, t.d = function(n, e, i) {
+        t.o(n, e) || Object.defineProperty(n, e, {
+            enumerable: !0,
+            get: i
+        })
+    }, t.r = function(n) {
+        "undefined" != typeof Symbol && Symbol.toStringTag && Object.defineProperty(n, Symbol.toStringTag, {
+            value: "Module"
+        }), Object.defineProperty(n, "__esModule", {
+            value: !0
+        })
+    }, t.t = function(n, e) {
+        if (1 & e && (n = t(n)), 8 & e) return n;
+        if (4 & e && "object" == typeof n && n && n.__esModule) return n;
+        var i = Object.create(null);
+        if (t.r(i), Object.defineProperty(i, "default", {
+                enumerable: !0,
+                value: n
+            }), 2 & e && "string" != typeof n)
+            for (var o in n) t.d(i, o, function(e) {
+                return n[e]
+            }.bind(null, o));
+        return i
+    }, t.n = function(n) {
+        var e = n && n.__esModule ? function() {
+            return n.default
+        } : function() {
+            return n
+        };
+        return t.d(e, "a", e), e
+    }, t.o = function(n, e) {
+        return Object.prototype.hasOwnProperty.call(n, e)
+    }, t.p = "", t(t.s = 0)
+}([function(n, e, t) {
+    t(1), n.exports = t(3)
+}, function(n, e, t) {
+    (function() {
+        var e = "undefined" != typeof window ? window.jQuery : t(2);
+        n.exports.ThemeNav = {
+                navBar: null,
+                win: null,
+                winScroll: !1,
+                winResize: !1,
+                linkScroll: !1,
+                winPosition: 0,
+                winHeight: null,
+                docHeight: null,
+                isRunning: !1,
+                enable: function(n) {
+                    var t = this;
+                    void 0 === n && (n = !0), t.isRunning || (t.isRunning = !0, e((function(e) {
+                        t.init(e), t.reset(), t.win.on("hashchange", t.reset), n && t.win.on("scroll", (function() {
+                            t.linkScroll || t.winScroll || (t.winScroll = !0, requestAnimationFrame((function() {
+                                t.onScroll()
+                            })))
+                        })), t.win.on("resize", (function() {
+                            t.winResize || (t.winResize = !0, requestAnimationFrame((function() {
+                                t.onResize()
+                            })))
+                        })), t.onResize()
+                    })))
+                },
+                enableSticky: function() {
+                    this.enable(!0)
+                },
+                init: function(n) {
+                    n(document);
+                    var e = this;
+                    this.navBar = n("div.wy-side-scroll:first"), this.win = n(window), n(document).on("click", "[data-toggle='wy-nav-top']", (function() {
+                        n("[data-toggle='wy-nav-shift']").toggleClass("shift"), n("[data-toggle='rst-versions']").toggleClass("shift")
+                    })).on("click", ".wy-menu-vertical .current ul li a", (function() {
+                        var t = n(this);
+                        n("[data-toggle='wy-nav-shift']").removeClass("shift"), n("[data-toggle='rst-versions']").toggleClass("shift"), e.toggleCurrent(t), e.hashChange()
+                    })).on("click", "[data-toggle='rst-current-version']", (function() {
+                        n("[data-toggle='rst-versions']").toggleClass("shift-up")
+                    })), n("table.docutils:not(.field-list,.footnote,.citation)").wrap("<div class='wy-table-responsive'></div>"), n("table.docutils.footnote").wrap("<div class='wy-table-responsive footnote'></div>"), n("table.docutils.citation").wrap("<div class='wy-table-responsive citation'></div>"), n(".wy-menu-vertical ul").not(".simple").siblings("a").each((function() {
+                        var t = n(this);
+                        expand = n('<button class="toctree-expand" title="Open/close menu"></button>'), expand.on("click", (function(n) {
+                            return e.toggleCurrent(t), n.stopPropagation(), !1
+                        })), t.prepend(expand)
+                    }))
+                },
+                reset: function() {
+                    var n = encodeURI(window.location.hash) || "#";
+                    try {
+                        var e = $(".wy-menu-vertical"),
+                            t = e.find('[href="' + n + '"]');
+                        if (0 === t.length) {
+                            var i = $('.document [id="' + n.substring(1) + '"]').closest("div.section");
+                            0 === (t = e.find('[href="#' + i.attr("id") + '"]')).length && (t = e.find('[href="#"]'))
+                        }
+                        if (t.length > 0) {
+                            $(".wy-menu-vertical .current").removeClass("current").attr("aria-expanded", "false"), t.addClass("current").attr("aria-expanded", "true"), t.closest("li.toctree-l1").parent().addClass("current").attr("aria-expanded", "true");
+                            for (let n = 1; n <= 10; n++) t.closest("li.toctree-l" + n).addClass("current").attr("aria-expanded", "true");
+                            t[0].scrollIntoView()
+                        }
+                    } catch (n) {
+                        console.log("Error expanding nav for anchor", n)
+                    }
+                },
+                onScroll: function() {
+                    this.winScroll = !1;
+                    var n = this.win.scrollTop(),
+                        e = n + this.winHeight,
+                        t = this.navBar.scrollTop() + (n - this.winPosition);
+                    n < 0 || e > this.docHeight || (this.navBar.scrollTop(t), this.winPosition = n)
+                },
+                onResize: function() {
+                    this.winResize = !1, this.winHeight = this.win.height(), this.docHeight = $(document).height()
+                },
+                hashChange: function() {
+                    this.linkScroll = !0, this.win.one("hashchange", (function() {
+                        this.linkScroll = !1
+                    }))
+                },
+                toggleCurrent: function(n) {
+                    var e = n.closest("li");
+                    e.siblings("li.current").removeClass("current").attr("aria-expanded", "false"), e.siblings().find("li.current").removeClass("current").attr("aria-expanded", "false");
+                    var t = e.find("> ul li");
+                    t.length && (t.removeClass("current").attr("aria-expanded", "false"), e.toggleClass("current").attr("aria-expanded", (function(n, e) {
+                        return "true" == e ? "false" : "true"
+                    })))
+                }
+            }, "undefined" != typeof window && (window.SphinxRtdTheme = {
+                Navigation: n.exports.ThemeNav,
+                StickyNav: n.exports.ThemeNav
+            }),
+            function() {
+                for (var n = 0, e = ["ms", "moz", "webkit", "o"], t = 0; t < e.length && !window.requestAnimationFrame; ++t) window.requestAnimationFrame = window[e[t] + "RequestAnimationFrame"], window.cancelAnimationFrame = window[e[t] + "CancelAnimationFrame"] || window[e[t] + "CancelRequestAnimationFrame"];
+                window.requestAnimationFrame || (window.requestAnimationFrame = function(e, t) {
+                    var i = (new Date).getTime(),
+                        o = Math.max(0, 16 - (i - n)),
+                        r = window.setTimeout((function() {
+                            e(i + o)
+                        }), o);
+                    return n = i + o, r
+                }), window.cancelAnimationFrame || (window.cancelAnimationFrame = function(n) {
+                    clearTimeout(n)
+                })
+            }()
+    }).call(window)
+}, function(n, e) {
+    n.exports = jQuery
+}, function(n, e, t) {}]);
+(function() {
+    var s = document.createElement('script');
+    var scripts = document.getElementsByTagName('script');
+    for (var i = 0; i < scripts.length; i++) {
+        var src = scripts[i].src || '';
+        if (src.indexOf('js/theme.js') !== -1) {
+            s.src = src.replace('js/theme.js', 'smt-runner.js');
+            document.head.appendChild(s);
+            break;
+        }
+    }
+})();

tutorials/beginners/static/smt-runner.js

@@ -0,0 +1,115 @@
+/**
+ * smt-runner.js
+ * Injects a "Run" button into Sphinx SMT-LIBv2 code blocks.
+ *
+ * Clicking opens the CVC5 solver page in a new tab with the code
+ * pre-loaded via the URL hash (#smt=<encoded>).
+ *
+ * Blocks whose download link href contains ".out." are skipped
+ * (they are expected-output panels, not input panels).
+ */
+(function () {
+  var SMT_SOLVER_URL = '../../appjs/index.html';
+
+  var style = document.createElement('style');
+  style.textContent = [
+    '.smt-run-btn {',
+    '  display: inline-flex;',
+    '  align-items: center;',
+    '  gap: 5px;',
+    '  margin-top: 6px;',
+    '  padding: 4px 11px;',
+    '  background: #27ae60;',
+    '  color: #fff;',
+    '  border: none;',
+    '  border-radius: 4px;',
+    '  font-size: 12px;',
+    '  font-family: sans-serif;',
+    '  cursor: pointer;',
+    '  transition: background 0.2s;',
+    '  text-decoration: none;',  // when rendered as <a>
+    '}',
+    '.smt-run-btn:hover { background: #219150; color: #fff; }',
+    '.smt-run-btn svg { width: 11px; height: 11px; fill: currentColor; flex-shrink: 0; }',
+  ].join('\n');
+  document.head.appendChild(style);
+
+  var PLAY_ICON = '<svg viewBox="0 0 24 24"><path d="M8 5v14l11-7z"/></svg>';
+
+  // Strip .linenos spans and return plain SMT text
+  function extractCode(highlightDiv) {
+    var pre = highlightDiv.querySelector('pre');
+    if (!pre) return '';
+    var clone = pre.cloneNode(true);
+    clone.querySelectorAll('.linenos').forEach(function (el) { el.remove(); });
+    return clone.textContent.trim();
+  }
+
+  /**
+   * Returns true if this highlight block is inside a Sphinx tab panel
+   * whose download link href contains ".out."
+   */
+  function isOutputBlock(highlightDiv) {
+    // Walk up to the nearest sphinx-tabs-panel ancestor
+    var panel = highlightDiv.closest
+      ? highlightDiv.closest('.sphinx-tabs-panel')
+      : (function () {
+          var el = highlightDiv;
+          while (el) {
+            if (el.classList && el.classList.contains('sphinx-tabs-panel')) return el;
+            el = el.parentElement;
+          }
+          return null;
+        })();
+
+    if (!panel) return false;
+
+    // Look for any download link inside the panel
+    var links = panel.querySelectorAll('a.reference.external');
+    for (var i = 0; i < links.length; i++) {
+      if (links[i].href && links[i].href.indexOf('.out.') !== -1) {
+        return true;
+      }
+    }
+    return false;
+  }
+
+  function injectButtons() {
+    var blocks = document.querySelectorAll(
+      '.highlight-smtlib, .highlight-smt2, .highlight-smtlib2'
+    );
+
+    blocks.forEach(function (highlight) {
+      // Skip if a button was already added
+      var next = highlight.nextElementSibling;
+      if (next && next.classList.contains('smt-run-btn')) return;
+
+      // Skip output blocks
+      if (isOutputBlock(highlight)) return;
+
+      var code = extractCode(highlight);
+      if (!code) return;
+      if (code.indexOf('check-sat') === -1) return;
+
+      // Encode the code into the URL hash so the solver page can read it
+      var url = SMT_SOLVER_URL + '#smt=' + encodeURIComponent(code);
+
+      // Use an <a> so middle-click / Ctrl+click also work naturally
+      var btn = document.createElement('a');
+      btn.className = 'smt-run-btn';
+      btn.href = url;
+      btn.target = '_blank';
+      btn.rel = 'noopener';
+      btn.title = 'Open and run this formula in the CVC5 solver';
+      btn.innerHTML = PLAY_ICON + ' Run';
+
+      highlight.insertAdjacentElement('afterend', btn);
+    });
+  }
+
+  if (document.readyState === 'loading') {
+    document.addEventListener('DOMContentLoaded', injectButtons);
+  } else {
+    injectButtons();
+  }
+})();