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
/*
* 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 "Test/UnitTesting.hpp"
#include "Test/SyntaxSugar.hpp"
#include "Test/GenerationTester.hpp"
#include "Inferences/EqualityResolution.hpp"
using namespace Test;
REGISTER_GEN_TESTER(Test::Generation::GenerationTester<Inferences::EqualityResolution>(EqualityResolution()))
/**
* NECESSARY: We need to tell the tester which syntax sugar to import for creating terms & clauses.
* See Test/SyntaxSugar.hpp for which kinds of syntax sugar are available
*/
#define MY_SYNTAX_SUGAR \
DECL_DEFAULT_VARS \
DECL_SORT(s) \
DECL_FUNC(f, {s}, s) \
DECL_FUNC(g, {s}, s) \
DECL_CONST(a, s) \
DECL_PRED (p, {s}) \
DECL_PRED (q, {s}) \
/** Defines a test case. */
TEST_GENERATION(test_01, // <- name
Generation::AsymmetricTest()
.input( clause({ selected(x != f(a)), p(x) })) // <- input clause
.expected(exactly( // <- a list of exactly which clauses are expected
clause({ p(f(a)) }) // to be returned. Order matters!
))
.premiseRedundant(false) // <- shall the premis be removed from the search
// space after the rule application ?
// (default value: false)
)
TEST_GENERATION(test_02,
Generation::AsymmetricTest()
.input( clause({ x != f(a), selected(p(x)) }))
.expected( exactly())
)
TEST_GENERATION(test_03,
Generation::AsymmetricTest()
.input( clause({ selected(x != f(a)), selected(p(x)) }))
.expected( exactly())
)
TEST_GENERATION(test_04,
Generation::AsymmetricTest()
.input( clause({ selected(g(x) != f(a)), p(x) }))
.expected( exactly())
)
TEST_GENERATION(test_05,
Generation::AsymmetricTest()
.input( clause({ selected(f(g(x)) != f(y)) }))
.expected( exactly( clause({})))
)
TEST_GENERATION(test_06,
Generation::AsymmetricTest()
.input( clause({ selected(f(g(x)) != f(x)) }))
.expected( exactly())
)
TEST_GENERATION(test_07,
Generation::AsymmetricTest()
.input( clause({ selected(x != f(a)), selected(x != a) }))
.expected( exactly( clause({ f(a) != a })))
)