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
131
132
133
134
135
136
137
|
/********************* */
/*! \file proof_skolem_cache.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief Proof skolem cache utility
**/
#include "cvc4_private.h"
#ifndef CVC4__EXPR__PROOF_SKOLEM_CACHE_H
#define CVC4__EXPR__PROOF_SKOLEM_CACHE_H
#include <string>
#include "expr/node.h"
namespace CVC4 {
/**
* A manager for skolems that can be used in proofs. This is designed to be
* trusted interface to NodeManager::mkSkolem, where one
* must provide a definition for the skolem they create in terms of a
* predicate that the introduced variable is intended to witness.
*
* It is implemented by mapping terms to an attribute corresponding to their
* "witness form" as described below. Hence, this class does not impact the
* reference counting of skolem variables which may be deleted if they are not
* used.
*/
class ProofSkolemCache
{
public:
ProofSkolemCache() {}
~ProofSkolemCache() {}
/**
* This makes a skolem of same type as bound variable v, (say its type is T),
* whose definition is (witness ((v T)) pred). This definition is maintained
* by this class.
*
* Notice that (exists ((v T)) pred) should be a valid formula. This fact
* captures the reason for why the returned Skolem was introduced.
*
* Take as an example extensionality in arrays:
*
* (declare-fun a () (Array Int Int))
* (declare-fun b () (Array Int Int))
* (assert (not (= a b)))
*
* To witness the index where the arrays a and b are disequal, it is intended
* we call this method on:
* Node k = mkSkolem( x, F )
* where F is:
* (=> (not (= a b)) (not (= (select a x) (select b x))))
* and x is a fresh bound variable of integer type. Internally, this will map
* k to the term:
* (witness ((x Int)) (=> (not (= a b))
* (not (= (select a x) (select b x)))))
* A lemma generated by the array solver for extensionality may safely use
* the skolem k in the standard way:
* (=> (not (= a b)) (not (= (select a k) (select b k))))
* Furthermore, notice that the following lemma does not involve fresh
* skolem variables and is valid according to the theory of arrays extended
* with support for witness:
* (let ((w (witness ((x Int)) (=> (not (= a b))
* (not (= (select a x) (select b x)))))))
* (=> (not (= a b)) (not (= (select a w) (select b w)))))
* This version of the lemma, which requires no explicit tracking of free
* Skolem variables, can be obtained by a call to getWitnessForm(...)
* below. We call this the "witness form" of the lemma above.
*
* @param v The bound variable of the same type of the Skolem to create.
* @param pred The desired property of the Skolem to create, in terms of bound
* variable v.
* @param prefix The prefix of the name of the Skolem
* @param comment Debug information about the Skolem
* @param flags The flags for the Skolem (see NodeManager::mkSkolem)
* @return The skolem whose witness form is registered by this class.
*/
static Node mkSkolem(Node v,
Node pred,
const std::string& prefix,
const std::string& comment = "",
int flags = NodeManager::SKOLEM_DEFAULT);
/**
* Same as above, but where pred is an existential quantified formula
* whose bound variable list contains v. For example, calling this method on:
* x, (exists ((x Int) (y Int)) (P x y))
* will return:
* (witness ((x Int)) (exists ((y Int)) (P x y)))
* If the variable v is not in the bound variable list of q, then null is
* returned and an assertion failure is thrown.
*/
static Node mkSkolemExists(Node v,
Node q,
const std::string& prefix,
const std::string& comment = "",
int flags = NodeManager::SKOLEM_DEFAULT);
/**
* Same as above, but for special case for (witness ((x T)) (= x t))
* where T is the type of t. This skolem is unique for each t.
*/
static Node mkPurifySkolem(Node t,
const std::string& prefix,
const std::string& comment = "",
int flags = NodeManager::SKOLEM_DEFAULT);
/** convert to witness form
*
* @param n The term or formula to convert to witness form described above
* @return n in witness form.
*/
static Node getWitnessForm(Node n);
/** convert to Skolem form
*
* @param n The term or formula to convert to Skolem form described above
* @return n in Skolem form.
*/
static Node getSkolemForm(Node n);
/** convert to witness form vector */
static void convertToWitnessFormVec(std::vector<Node>& vec);
/** convert to Skolem form vector */
static void convertToSkolemFormVec(std::vector<Node>& vec);
private:
/** Convert to witness or skolem form */
static Node convertInternal(Node n, bool toWitness);
};
} // namespace CVC4
#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */
|
