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
112
113
114
115
116
117

/*
 * 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 ShortConflictMetaDP.cpp
 * Implements class ShortConflictMetaDP.
 */

#include "ShortConflictMetaDP.hpp"

namespace DP
{

using namespace std;

/**
 * Computes number of literals in core not implied at the zero level
 * of the SAT solver i.e. those that have not been fully decided and
 * can be backtracked.
 */
unsigned ShortConflictMetaDP::getCoreSize(const LiteralStack& core)
{
  // ASS_EQ(_solver.getStatus(), SATSolver::SATISFIABLE);

  unsigned res = 0;
  LiteralStack::ConstIterator cit(core);
  while(cit.hasNext()) {
    Literal* lit = cit.next();
    SATLiteral sl = _sat2fo.toSAT(lit);
    ASS(_solver.trueInAssignment(sl));
    bool zeroImplied = _solver.isZeroImplied(sl.var());
    if(!zeroImplied) {
      res++;
    }
  }
  return res;
}

/**
 * Gets status of inner. If this is unsat then filter unsat cores so that we only
 * keep cores that are the smallest or one larger than the smallest.
 */
DecisionProcedure::Status ShortConflictMetaDP::getStatus(bool getMultipleCores)
{
  Status iStatus = _inner->getStatus(getMultipleCores);

  _unsatCores.reset();
  if(iStatus!=DecisionProcedure::UNSATISFIABLE) {
    return iStatus;
  }

  unsigned ucCnt = _inner->getUnsatCoreCount();
  ASS_G(ucCnt,0);
  if(ucCnt==1) {
    _unsatCores.push(LiteralStack());
    _inner->getUnsatCore(_unsatCores.top(), 0);
    return DecisionProcedure::UNSATISFIABLE;
  }

  unsigned minSz = UINT_MAX;

  typedef pair<LiteralStack,unsigned> CoreWithSize;
  static Stack<CoreWithSize> cores;
  ASS(cores.isEmpty());

  // Record cores with their sizes in cores stack and
  // keep track of smallest core size in minSz
  for(unsigned i=0; i<ucCnt; i++) {
    cores.push(CoreWithSize());
    LiteralStack& core = cores.top().first;
    unsigned& sz = cores.top().second;
    _inner->getUnsatCore(core, i);
    sz = getCoreSize(core);

    if(sz<minSz) {
      minSz = sz;
    }
  }

  // Only keep cores that are at most one literal larger than the smallest size
  while(cores.isNonEmpty()) {
    LiteralStack& core = cores.top().first;
    unsigned& sz = cores.top().second;

    //this is perhaps the most important line, contains condition that restricts the acceptable core size
    if(sz<=minSz+1) {
      //we keep this core as it's small enough
      _unsatCores.push(LiteralStack());
      std::swap(core, _unsatCores.top());
      ASS(core.isEmpty());
    }

    cores.pop();
  }

  ASS(_unsatCores.isNonEmpty());
  return DecisionProcedure::UNSATISFIABLE;
}

/**
 * Get the unsat core (literal stack) at coreIndex
 */
void ShortConflictMetaDP::getUnsatCore(LiteralStack& res, unsigned coreIndex)
{
  ASS(res.isEmpty());
  ASS_L(coreIndex, _unsatCores.size());

  res = _unsatCores[coreIndex];
}

}