vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50

/*
 * This file is part of the source code of the software program
 * Vampire. It is protected by applicable
 * copyright laws.
 *
 * This source code is distributed under the licence found here
 * https://vprover.github.io/license.html
 * and in the source directory
 */
/**
 * @file ProofExtra.cpp
 * Various objects that include "extra information" about an inference,
 * e.g. selected literals, unifier, etc.
 *
 * @since 09/09/2024 Oxford
 */

#include "ProofExtra.hpp"

namespace Inferences {

void LiteralInferenceExtra::output(std::ostream &out) const {
  out << "selected=(" << selectedLiteral->toString() << ')';
}

void TwoLiteralInferenceExtra::output(std::ostream &out) const {
  selectedLiteral.output(out);
  out << ",other=(" << otherLiteral->toString() << ')';
  if (synthesisExtra.condition) {
    out << ",condition=(" << synthesisExtra.condition->toString() << ")";
  }
  if (synthesisExtra.thenLit) {
    out << ",thenLit=(" << synthesisExtra.thenLit->toString() << "," << synthesisExtra.thenLit << ")";
  }
  if (synthesisExtra.elseLit) {
    out << ",elseLit=(" << synthesisExtra.elseLit->toString() << "," << synthesisExtra.elseLit << ")";
  }
}

void RewriteInferenceExtra::output(std::ostream &out) const {
  out << "lhs=" << lhs << ",target=" << rewritten;
}

void TwoLiteralRewriteInferenceExtra::output(std::ostream &out) const {
  selected.output(out);
  out << ',';
  rewrite.output(out);
}

} // namespace Inferences