diff --git a/appjs/index.html b/appjs/index.html index cecf050..8d9fe2f 100644 --- a/appjs/index.html +++ b/appjs/index.html @@ -588,6 +588,36 @@

CVC5 SMT Solver

} + + diff --git a/tutorials/beginners/static/js/theme.js b/tutorials/beginners/static/js/theme.js index 1fddb6e..8152913 100644 --- a/tutorials/beginners/static/js/theme.js +++ b/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("
"),n("table.docutils.footnote").wrap("
"),n("table.docutils.citation").wrap("
"),n(".wy-menu-vertical ul").not(".simple").siblings("a").each((function(){var t=n(this);expand=n(''),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"), n("table.docutils.footnote").wrap("
"), n("table.docutils.citation").wrap("
"), n(".wy-menu-vertical ul").not(".simple").siblings("a").each((function() { + var t = n(this); + expand = n(''), 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; + } + } +})(); \ No newline at end of file diff --git a/tutorials/beginners/static/smt-runner.js b/tutorials/beginners/static/smt-runner.js new file mode 100644 index 0000000..71c4491 --- /dev/null +++ b/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=). + * + * 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 + '}', + '.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 = ''; + + // 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 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(); + } +})(); \ No newline at end of file