GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/witness_form.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file witness_form.h
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 "cvc4_private.h"
16
17
#ifndef CVC4__SMT__WITNESS_FORM_H
18
#define CVC4__SMT__WITNESS_FORM_H
19
20
#include <unordered_set>
21
22
#include "expr/proof.h"
23
#include "expr/proof_generator.h"
24
#include "expr/term_conversion_proof_generator.h"
25
26
namespace CVC4 {
27
namespace smt {
28
29
/**
30
 * The witness form proof generator, which acts as a wrapper around a
31
 * TConvProofGenerator for adding rewrite steps for witness introduction.
32
 *
33
 * The proof steps managed by this class are stored in a context-independent
34
 * manager, which matches how witness forms are managed in SkolemManager.
35
 */
36
class WitnessFormGenerator : public ProofGenerator
37
{
38
 public:
39
  WitnessFormGenerator(ProofNodeManager* pnm);
40
962
  ~WitnessFormGenerator() {}
41
  /**
42
   * Get proof for, which expects an equality of the form t = toWitness(t).
43
   * This returns a proof based on the term conversion proof generator utility.
44
   * This proof may contain open assumptions of the form:
45
   *   k = toWitness(k)
46
   * Each of these assumptions are included in the set getWitnessFormEqs()
47
   * below after returning this call.
48
   */
49
  std::shared_ptr<ProofNode> getProofFor(Node eq) override;
50
  /** Identify */
51
  std::string identify() const override;
52
  /**
53
   * Does the rewrite require witness form conversion?
54
   * When calling this method, it should be the case that:
55
   *   Rewriter::rewrite(toWitness(t)) == Rewriter::rewrite(toWitness(s))
56
   * The rule MACRO_SR_PRED_TRANSFORM concludes t == s if the above holds.
57
   * This method returns false if:
58
   *   Rewriter::rewrite(t) == Rewriter::rewrite(s)
59
   * which means that the proof of the above fact does not need to do
60
   * witness form conversion to prove conclusions of MACRO_SR_PRED_TRANSFORM.
61
   */
62
  bool requiresWitnessFormTransform(Node t, Node s) const;
63
  /**
64
   * Same as above, with s = true. This is intended for use with
65
   * MACRO_SR_PRED_INTRO.
66
   */
67
  bool requiresWitnessFormIntro(Node t) const;
68
  /**
69
   * Get witness form equalities. This returns a set of equalities of the form:
70
   *   k = toWitness(k)
71
   * where k is a skolem, containing all rewrite steps used in calls to
72
   * getProofFor during the entire lifetime of this generator.
73
   */
74
  const std::unordered_set<Node, NodeHashFunction>& getWitnessFormEqs() const;
75
76
 private:
77
  /**
78
   * Convert to witness form. This internally constructs rewrite steps that
79
   * suffice to show t = toWitness(t) using the term conversion proof generator
80
   * of this class (d_tcpg).
81
   */
82
  Node convertToWitnessForm(Node t);
83
  /**
84
   * Return a proof generator that can prove the given axiom exists.
85
   */
86
  ProofGenerator* convertExistsInternal(Node exists);
87
  /** The term conversion proof generator */
88
  TConvProofGenerator d_tcpg;
89
  /** The nodes we have already added rewrite steps for in d_tcpg */
90
  std::unordered_set<TNode, TNodeHashFunction> d_visited;
91
  /** The set of equalities added as proof steps */
92
  std::unordered_set<Node, NodeHashFunction> d_eqs;
93
  /** Lazy proof storing witness intro steps */
94
  LazyCDProof d_wintroPf;
95
  /** CDProof for justifying purification existentials */
96
  CDProof d_pskPf;
97
};
98
99
}  // namespace smt
100
}  // namespace CVC4
101
102
#endif