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

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

#include "DistinctProcessor.hpp"

#include "Lib/Environment.hpp"

#include "Kernel/Formula.hpp"
#include "Kernel/FormulaUnit.hpp"
#include "Kernel/Signature.hpp"
#include "Kernel/Unit.hpp"

#include <cstring>

namespace Shell
{

//TODO: add expansion of non-top-level and negative distinct predicates

/**
 * True if 
 */
bool DistinctProcessor::isDistinctPred(Literal* l)
{
  //this is a hacky way to check for disctnct predicates,
  //needs to be fixed once we have a proper support for
  //these in the signature

  //Moreover, this check turned out to be bottleneck, so it
  //had to be optimized. The original was:
  //return l->predicateName().substr(0,9)=="$distinct"
  const char* n = l->predicateName().c_str();
  return n[0]=='$' && memcmp(n+1,"distinct",8)==0;
}

bool DistinctProcessor::apply(FormulaUnit* unit, Unit*& res)
{
  Formula* form = unit->formula();


  static Stack<unsigned> distConsts;
  if(form->connective()==LITERAL) {
    Literal* tlLit = form->literal();
    if(isDistinctPred(tlLit) && tlLit->isPositive()) {
      distConsts.reset();
      bool justConsts = true;
      Literal::Iterator argIt(tlLit);
      while(argIt.hasNext()) {
	TermList a = argIt.next();
	if(!a.isTerm() || a.term()->arity()!=0) {
	  justConsts = false;
	  break;
	}
	distConsts.push(a.term()->functor());
      }

      if(justConsts) {
	unsigned grpIdx = env.signature->createDistinctGroup(unit);
	while(distConsts.isNonEmpty()) {
	  env.signature->addToDistinctGroup(distConsts.pop(), grpIdx);
	}
      }else{
        USER_ERROR("$distinct should only be used positively with constants");
      }
    }
  }

  return false;
}

bool DistinctProcessor::apply(Clause* cl, Unit*& res) {
  return false;
}

}