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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108

/*
 * 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
 */

#include "KBO.hpp"
#include "Term.hpp"

#include "TermOrderingDiagramKBO.hpp"

namespace Kernel {

using namespace std;
using namespace Lib;
using namespace Shell;

void TermOrderingDiagramKBO::processTermNode()
{
  const auto& kbo = static_cast<const KBO&>(_ord);

  // weight and variable balances first

  // we only care about the non-zero weights and counts
  bool varInbalance = false;
  auto state = kbo._state.get();
#if VDEBUG
  // we make sure kbo._state is not used while we're using it
  auto __state = std::move(kbo._state);
#endif
  auto w = state->_weightDiff;
  decltype(state->_varDiffs)::Iterator vit(state->_varDiffs);
  Stack<VarCoeffPair> nonzeros;
  while (vit.hasNext()) {
    unsigned v;
    int cnt;
    vit.next(v,cnt);
    if (cnt!=0) {
      nonzeros.push({ v, cnt });
      w-=cnt; // we have to remove the variable weights from w
    }
    if (cnt<0) {
      varInbalance = true;
    }
  }
#if VDEBUG
  kbo._state = std::move(__state);
#endif

  auto node = _curr->node();
  ASS(node->lhs.isTerm() && node->rhs.isTerm());
  auto lhs = node->lhs.term();
  auto rhs = node->rhs.term();

  auto eqBranch = node->eqBranch;
  auto gtBranch = node->gtBranch;
  auto ngeBranch = node->ngeBranch;

  auto curr = _curr;
  bool weightAdded = (w < 0 || varInbalance);
  if (weightAdded) {
    // we mutate the original node
    curr->node()->tag = Node::T_POLY;
    curr->node()->poly = Polynomial::get(w, nonzeros);
    curr->node()->gtBranch = gtBranch;
    curr->node()->ngeBranch = ngeBranch;
    curr = &curr->node()->eqBranch;
  }

  switch (kbo.comparePrecedences(lhs,rhs))
  {
    case Ordering::LESS: {
      *curr = ngeBranch;
      break;
    }
    case Ordering::GREATER: {
      *curr = gtBranch;
      break;
    }
    case Ordering::EQUAL: {
      for (unsigned i = 0; i < lhs->arity(); i++) {
        auto lhsArg = *lhs->nthArgument(i);
        auto rhsArg = *rhs->nthArgument(i);
        // we mutate the original node in the first iteration
        if (!weightAdded && i==0) {
          curr->node()->lhs = lhsArg;
          curr->node()->rhs = rhsArg;
        } else {
          *curr = Branch(lhsArg,rhsArg);
          curr->node()->gtBranch = gtBranch;
          curr->node()->ngeBranch = ngeBranch;
        }
        curr = &curr->node()->eqBranch;
      }
      *curr = eqBranch;
      break;
    }
    default: {
      ASSERTION_VIOLATION;
    }
  }
}

}