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
109
110
111

/*
 * 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 "Kernel/Clause.hpp"
#include "Kernel/EqHelper.hpp"
#include "Kernel/SubstHelper.hpp"
#include "Kernel/Term.hpp"
#include "Kernel/Ordering.hpp"
#include "Kernel/TermIterators.hpp"
#include "Kernel/Ordering.hpp"

#include "Shell/Options.hpp"

#include "DemodulationHelper.hpp"

namespace Inferences {

using namespace Kernel;

DemodulationHelper::DemodulationHelper(const Options& opts, const Ordering* ord)
: _redundancyCheck(opts.demodulationRedundancyCheck() != Options::DemodulationRedundancyCheck::OFF),
  _encompassing(opts.demodulationRedundancyCheck() == Options::DemodulationRedundancyCheck::ENCOMPASS),
  _ord(ord)
{
}

bool DemodulationHelper::redundancyCheckNeededForPremise(Clause* rwCl, Literal* rwLit, TermList rwTerm) const
{
  if (!_redundancyCheck) {
    return false;
  }

  if (!rwLit->isEquality() || (rwTerm!=*rwLit->nthArgument(0) && rwTerm!=*rwLit->nthArgument(1))) {
    return false;
  }

  // check is needed if encompassment demodulation is off or we demodulate a positive unit
  return !_encompassing || (rwLit->isPositive() && (rwCl->length() == 1));
}

/**
 * Test whether the @param applicator is a renaming on the variables of @param t.
 */
bool DemodulationHelper::isRenamingOn(const SubstApplicator* applicator, TermList t)
{
  DHSet<TermList> renamingDomain;
  DHSet<TermList> renamingRange;

  VariableIterator it(t);
  while(it.hasNext()) {
    TermList v = it.next();
    ASS(v.isVar());
    if (!renamingDomain.insert(v)) {
      continue;
    }

    TermList vSubst = (*applicator)(v.var());
    if (!vSubst.isVar()) {
      return false;
    }
    if (!renamingRange.insert(vSubst)) {
      return false;
    }
  }
  return true;
}

bool DemodulationHelper::isPremiseRedundant(Clause* rwCl, Literal* rwLit, TermList rwTerm,
  TermList tgtTerm, TermList eqLHS, const SubstApplicator* eqApplicator) const
{
  ASS(redundancyCheckNeededForPremise(rwCl, rwLit, rwTerm));

  TermList other=EqHelper::getOtherEqualitySide(rwLit, rwTerm);
  if (_ord->compare(tgtTerm, other) == Ordering::LESS) {
    return true;
  }

  if (_encompassing) {
    // under _encompassing, we know there are no other literals in rwCl
    return !isRenamingOn(eqApplicator,eqLHS);
  }

  // return early to avoid creation of eqLitS
  if (rwCl->length()==1) {
    return false;
  }

  TermList eqSort = SortHelper::getEqualityArgumentSort(rwLit);
  Literal* eqLitS=Literal::createEquality(true, rwTerm, tgtTerm, eqSort);

  // The demodulation which does not preserve completeness:
  // s = t     s = t1 \/ C
  // ---------------------
  //      t = t1 \/ C
  // where t > t1 and s = t > C.
  //
  // Hence we need to check if there are any literals
  // in rwCl greater than eqLitS.
  return rwCl->iterLits().any([rwLit,this,eqLitS](Literal* lit) {
    return lit != rwLit && _ord->compare(eqLitS, lit)==Ordering::LESS;
  });
}

}  // namespace Inferences