GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/witness_form.cpp Lines: 44 63 69.8 %
Date: 2021-03-23 Branches: 77 290 26.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file witness_form.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief The module for managing witness form conversion in proofs
13
 **/
14
15
#include "smt/witness_form.h"
16
17
#include "expr/skolem_manager.h"
18
#include "theory/rewriter.h"
19
20
namespace CVC4 {
21
namespace smt {
22
23
962
WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
24
    : d_tcpg(pnm,
25
             nullptr,
26
             TConvPolicy::FIXPOINT,
27
             TConvCachePolicy::NEVER,
28
             "WfGenerator::TConvProofGenerator",
29
             nullptr,
30
             true),
31
      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"),
32
962
      d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof")
33
{
34
962
}
35
36
6627
std::shared_ptr<ProofNode> WitnessFormGenerator::getProofFor(Node eq)
37
{
38
6627
  if (eq.getKind() != kind::EQUAL)
39
  {
40
    // expecting an equality
41
    return nullptr;
42
  }
43
13254
  Node lhs = eq[0];
44
13254
  Node rhs = convertToWitnessForm(eq[0]);
45
6627
  if (rhs != eq[1])
46
  {
47
    // expecting witness form
48
    return nullptr;
49
  }
50
13254
  std::shared_ptr<ProofNode> pn = d_tcpg.getProofFor(eq);
51
6627
  Assert(pn != nullptr);
52
6627
  return pn;
53
}
54
55
std::string WitnessFormGenerator::identify() const
56
{
57
  return "WitnessFormGenerator";
58
}
59
60
6627
Node WitnessFormGenerator::convertToWitnessForm(Node t)
61
{
62
6627
  Node tw = SkolemManager::getOriginalForm(t);
63
6627
  if (t == tw)
64
  {
65
    // trivial case
66
    return tw;
67
  }
68
6627
  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
69
13254
  std::vector<TNode> visit;
70
13254
  TNode cur;
71
13254
  TNode curw;
72
6627
  visit.push_back(t);
73
40450
  do
74
  {
75
47077
    cur = visit.back();
76
47077
    visit.pop_back();
77
47077
    it = d_visited.find(cur);
78
47077
    if (it == d_visited.end())
79
    {
80
19828
      d_visited.insert(cur);
81
19828
      curw = SkolemManager::getOriginalForm(cur);
82
      // if its witness form is different
83
19828
      if (cur != curw)
84
      {
85
13569
        if (cur.isVar())
86
        {
87
5246
          Node eq = cur.eqNode(curw);
88
          // equality between a variable and its original form
89
2623
          d_eqs.insert(eq);
90
          // ------- SKOLEM_INTRO
91
          // k = t
92
2623
          d_wintroPf.addStep(eq, PfRule::SKOLEM_INTRO, {}, {cur});
93
2623
          d_tcpg.addRewriteStep(
94
              cur, curw, &d_wintroPf, true, PfRule::ASSUME, true);
95
        }
96
        else
97
        {
98
          // A term whose witness form is different from itself, recurse.
99
          // It should be the case that cur has children, since the witness
100
          // form of constants are themselves.
101
10946
          Assert(cur.getNumChildren() > 0);
102
10946
          if (cur.hasOperator())
103
          {
104
10946
            visit.push_back(cur.getOperator());
105
          }
106
10946
          visit.insert(visit.end(), cur.begin(), cur.end());
107
        }
108
      }
109
    }
110
47077
  } while (!visit.empty());
111
6627
  return tw;
112
}
113
114
30564
bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const
115
{
116
30564
  return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s);
117
}
118
119
7099
bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const
120
{
121
14198
  Node tr = theory::Rewriter::rewrite(t);
122
14198
  return !tr.isConst() || !tr.getConst<bool>();
123
}
124
125
const std::unordered_set<Node, NodeHashFunction>&
126
WitnessFormGenerator::getWitnessFormEqs() const
127
{
128
  return d_eqs;
129
}
130
131
ProofGenerator* WitnessFormGenerator::convertExistsInternal(Node exists)
132
{
133
  Assert(exists.getKind() == kind::EXISTS);
134
  if (exists[0].getNumChildren() == 1 && exists[1].getKind() == kind::EQUAL
135
      && exists[1][0] == exists[0][0])
136
  {
137
    Node tpurified = exists[1][1];
138
    Trace("witness-form") << "convertExistsInternal: infer purification "
139
                          << exists << " for " << tpurified << std::endl;
140
    // ------ REFL
141
    // t = t
142
    // ---------------- EXISTS_INTRO
143
    // exists x. x = t
144
    // The concluded existential is then used to construct the witness term
145
    // via witness intro.
146
    Node teq = tpurified.eqNode(tpurified);
147
    d_pskPf.addStep(teq, PfRule::REFL, {}, {tpurified});
148
    d_pskPf.addStep(exists, PfRule::EXISTS_INTRO, {teq}, {exists});
149
    return &d_pskPf;
150
  }
151
  return nullptr;
152
}
153
154
}  // namespace smt
155
26685
}  // namespace CVC4