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

/*
 * 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 PairUtils.hpp
 * Defines class PairUtils.
 */


#ifndef __PairUtils__
#define __PairUtils__

#include "Metaiterators.hpp"

namespace Lib {

template<typename P>
struct FirstOfPairFn
{
  typename P::first_type operator()(P p) { return p.first; }
};

template<typename P>
struct SecondOfPairFn
{
  typename P::second_type operator()(P p) { return p.second; }
};

template<typename C, typename D>
struct PairRightPushingFn
{
  PairRightPushingFn(C c) : _c(c) {}
  std::pair<C,D> operator()(D d) { return std::pair<C,D>(_c,d); }
private:
  C _c;
};

template<typename C, class D>
struct PairLeftPushingFn
{
  PairLeftPushingFn(D d): _d(d) {}
  std::pair<C,D> operator()(C c) { return std::pair<C,D>(c,_d); }
private:
  D _d;
};


///@addtogroup Iterators
///@{

/**
 * Given pair of an object A and an iterator I, return
 * an iterator J, that yields pairs (A,C), where C are
 * objects returned by iterator I. This virtually pushes
 * the pair structure into the iterator I.
 */
template<typename C, typename DIt>
MappingIterator<DIt,PairRightPushingFn<C,ELEMENT_TYPE(DIt)> >
  pushPairIntoRightIterator(std::pair<C, DIt > obj)
{
  return getMappingIterator(obj.second, PairRightPushingFn<C,ELEMENT_TYPE(DIt)>(obj.first));
}

template<typename C, typename DIt>
MappingIterator<DIt,PairRightPushingFn<C,ELEMENT_TYPE(DIt)> >
  pushPairIntoRightIterator(C c, DIt dit)
{
  return getMappingIterator(std::move(dit), PairRightPushingFn<C,ELEMENT_TYPE(DIt)>(c));
}

template<typename C, typename D>
class RightPushedPair
{
public:
  DECL_ELEMENT_TYPE(std::pair<C,ELEMENT_TYPE(D)>);
  DECL_ITERATOR_TYPE(MappingIterator<ITERATOR_TYPE(D),PairRightPushingFn<C,ELEMENT_TYPE(D)> >);
  RightPushedPair(std::pair<C,D> p) : _p(p) {}
  std::pair<C,D> get() { return _p; }
private:
  std::pair<C,D> _p;
};

/** See VirtualIterator.hpp */
template<typename C, typename DItb>
MappingIterator<ITERATOR_TYPE(DItb),PairRightPushingFn<C,ELEMENT_TYPE(DItb)> >
  getContentIterator(RightPushedPair<C,DItb> obj)
{
  return pushPairIntoRightIterator(obj.get().first,
	  getContentIterator(obj.get().second) );
}

///@}

};

#endif /* __PairUtils__ */