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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 contextindependent 
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 