Skip to content

Commit 45d3006

Browse files
committed
latest. hopefully good and interactive?
1 parent 2dc812c commit 45d3006

1 file changed

Lines changed: 20 additions & 5 deletions

File tree

patchVampireInteractive.sh

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -112,9 +112,9 @@ run_patch "Wire interactive input helper into vampire.cpp" '--- a/vampire.cpp
112112
run_patch "Use web-aware input in ManCSPassiveClauseContainer" '--- a/Saturation/ManCSPassiveClauseContainer.cpp
113113
+++ b/Saturation/ManCSPassiveClauseContainer.cpp
114114
@@ -13,6 +13,8 @@
115-
*/
116-
#include <iostream>
117-
#include <algorithm>
115+
*/
116+
#include <iostream>
117+
#include <algorithm>
118118
+#include <stdexcept>
119119
+#include "Lib/WebInteractive.hpp"
120120
#include "ManCSPassiveClauseContainer.hpp"
@@ -124,12 +124,27 @@ run_patch "Use web-aware input in ManCSPassiveClauseContainer" '--- a/Saturation
124124
@@ -49,7 +51,9 @@ Clause* ManCSPassiveClauseContainer::popSelected()
125125
// ask user to pick a clause id
126126
std::cout << "Pick a clause:\n";
127-
std::string id;
127+
std::string id;
128128
- std::cin >> id;
129129
+ if (!Lib::Web::readInteractiveLine(id)) {
130130
+ throw std::runtime_error("No input available for clause selection");
131131
+ }
132-
unsigned selectedId = std::stoi(id);
132+
unsigned selectedId = std::stoi(id);
133+
'
134+
135+
run_patch "Relax TermOrderingDiagram asserts for Emscripten" '--- a/Kernel/TermOrderingDiagram.hpp
136+
+++ b/Kernel/TermOrderingDiagram.hpp
137+
@@
138+
- static_assert(sizeof(uint64_t) == sizeof(Branch));
139+
- static_assert(sizeof(uint64_t) == sizeof(TermList));
140+
- static_assert(sizeof(uint64_t) == sizeof(void*));
141+
- static_assert(sizeof(uint64_t) == sizeof(intptr_t));
142+
+#ifndef __EMSCRIPTEN__
143+
+ static_assert(sizeof(uint64_t) == sizeof(Branch));
144+
+ static_assert(sizeof(uint64_t) == sizeof(TermList));
145+
+ static_assert(sizeof(uint64_t) == sizeof(void*));
146+
+ static_assert(sizeof(uint64_t) == sizeof(intptr_t));
147+
+#endif
133148
'
134149

135150
run_patch "List WebInteractive.cpp in sources" '--- a/cmake/sources.cmake

0 commit comments

Comments
 (0)