Fix reconstruction of UCT proofs.

giomasce · Jul 3, 2018 · afa90e9 · afa90e9
1 parent dd7f486
commit afa90e9
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/provers/uct.cpp b/provers/uct.cpp
@@ -603,8 +603,16 @@ int uct_main(int argc, char *argv[]) {
         if (res == PROVED) {
             std::cout << "Found proof after " << i+1 << " visits:";
             CreativeProofEngineImpl< Sentence > engine(tb, false);
+            std::vector< std::function< void() > > children_cb;
+            for (const auto &hyp : problem.second) {
+                LabTok hyp_lab = engine.create_new_hypothesis(tb.reconstruct_sentence(pt2_to_pt(hyp), tb.get_turnstile()));
+                children_cb.emplace_back([hyp_lab,&engine]() {
+                    engine.process_label(hyp_lab);
+                });
+            }
+            prover->set_children_callbacks(std::move(children_cb));
             try {
-                    prover->replay_proof(engine);
+                prover->replay_proof(engine);
             } catch (ProofException< Sentence > &pe) {
                 std::cout << "Failed with exception:" << std::endl;
                 tb.dump_proof_exception(pe, std::cout);

diff --git a/resources/tests.txt b/resources/tests.txt
@@ -31,3 +31,6 @@
  |- A = B
 
 |- ( -. x e. (/) /\ ( ph -> ph ) )
+
+|- ( ph /\ A. x y = y )
+ |- ph