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
118
119
120
121
122
123
124
125
126
127
128
129
130

/*
 * 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
 */

namespace VariablePowerGeneralizationImpl {

/**
*  Rule 4)
*    generalize variable multiplication (REALS only)
*    C[X ⋅ X ⋅ ... ⋅ X ] 
*    ------------ 
*    C[X]
*    where 
*    - all occurrences of X are in terms of the form `X ⋅ X ⋅ ... ⋅ X`
*    - sound due to substitution { X -> X^(0/n) }
*    - obviously a generalization 
*/

using IntLattice = FlatMeetLattice<int>;
using PowerMap = Map<Variable, IntLattice, StlHash>;
template<class Num>
using EnableIfNotReal = typename std::enable_if<!std::is_same<Num, RealTraits>::value, int>::type;

/** 
 * Polymorphic closure for preprocessing for the rule application.
 *
 * Collects for each variable the power in which it occurs or Bot when the variable occurs in different powers
 */
struct Preprocess 
{
  PowerMap &powers;

  void operator()(Perfect<Polynom<RealTraits>> p) 
  {
    for (auto summand : p->iterSummands()) {
      for (auto factor : summand.factors->iter()) {
        auto var = factor.term.tryVar();
        if (var.isSome()) {


          auto current = factor.power == 0 || factor.power == 1  /* <- power 0 should never happen. 
                                                                       power 1 yields a nop-generalization */
            ? IntLattice::bot()
            : IntLattice(factor.power);

          powers.updateOrInit(var.unwrap(),
              [&](IntLattice old) { return current.meet(old); },
              [&]() { return current; }
            );
        }
      }
    }
  }


  template<class Num, EnableIfNotReal<Num> = 0> 
  void operator()(Perfect<Polynom<Num>> p) 
  { }

};

struct Generalize 
{
  PowerMap& powers;
  bool doOrderingCheck;

  Monom<RealTraits> operator()(Monom<RealTraits> p, PolyNf* evaluatedArgs)  
  {
    unsigned i = 0;
    return Monom<RealTraits>(
        p.numeral, 
        perfect(MonomFactors<RealTraits>(
          p.factors->iter()
           .map([&](MonomFactor<RealTraits> m) 
             { 
                auto var = m.term.tryVar();
                if (var.isSome() && !powers.get(var.unwrap()).isBot()) {
                  ASS_EQ(evaluatedArgs[i], var.unwrap());
                  return MonomFactor<RealTraits>(evaluatedArgs[i++], 2 - ( m.power % 2 ));
                } else {
                  return MonomFactor<RealTraits>(evaluatedArgs[i++], m.power); 
                }
              })
           .template collect<Stack>())));
  }

  template<class Num, EnableIfNotReal<Num> = 0>
  Monom<Num> operator()(Monom<Num> p, PolyNf* evaluatedArgs)  
  { return Monom<Num>(p.numeral, perfect(p.factors->replaceTerms(evaluatedArgs))); }

};


/** 
 * applies the rule
 */ 
SimplifyingGeneratingInference1::Result applyRule(Clause* cl, bool doOrderingCheck) 
{
  DEBUG("input clause: ", *cl);
  PowerMap powers;

  /* preprocessing. finds all products `X ⋅ X ⋅ ... ⋅ X` such that the rule is applicable */
  for (auto poly : iterPolynoms(cl)) {
    poly.apply(Preprocess { powers, });
  }

  bool applicable = 
    iterTraits(powers.iter())
      .find([](PowerMap::Entry& e) { return !e.value().isBot() && e.value().unwrap() >= 3; })
      .isSome();

  DEBUG("generalizations: ", powers);

  if (applicable) {
    return generalizeBottomUp(cl, EvaluateMonom<Generalize> { Generalize { powers, doOrderingCheck } });
  } else {
    return SimplifyingGeneratingInference1::Result::nop(cl);
  }
}


} // namespace VariablePowerGeneralizationImpl