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

/*
 * 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 "Lib/Stack.hpp"
#include "Lib/DHMap.hpp"
#include "Lib/Backtrackable.hpp"

namespace Lib {

  template<class C>
  struct BdStack : public Stack<C> {
    using Stack<C>::Stack;

    C swapRemove(unsigned idx, BacktrackData& bd)
    {
      auto removed = Stack<C>::swapRemove(idx);
      bd.addClosure([this,removed,idx]() mutable {
          Stack<C>::push(std::move(removed));
          std::swap((*this)[idx], this->top());
      });
      return removed;
    }


    void push(C val, BacktrackData& bd)
    {
      Stack<C>::push(std::move(val));
      bd.addClosure([this] { this->pop(); });
    }
  };

  template<class K, class V>
  struct BdDHMap : public DHMap<K, V> {
    using Super = DHMap<K,V>;
    using DHMap<K,V>::DHMap;

    using Super::remove;

    Option<std::pair<K, V>> remove(K const& key, BacktrackData& bd)
    {
      auto removed = Super::remove(key);
      bd.addClosure([this,removed]() mutable {
          if (removed) {
            Super::insert(std::move(removed->first), std::move(removed->second));
          }
      });
      return removed;
    }


    V replace(K const& key, V val, BacktrackData& bd)
    {
      auto old = Super::find(key);
      ASS(old);
      std::swap(val, *old);
      bd.addClosure([this,key,val]() mutable {
          std::swap(*Super::find(key), val);
      });
      return val;
    }



  };
} // namespace Lib