CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_array
array_proof_rules.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file array_proof_rules.h
4
*
5
* Author: Clark Barrett 5/29/2003
6
*
7
* Created: May 29 19:16:33 GMT 2003
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
* CLASS: ArrayProofRules
19
*
20
*
21
* Description: Array proof rules.
22
*/
23
/*****************************************************************************/
24
25
#ifndef _cvc3__theory_array__array_proof_rules_h_
26
#define _cvc3__theory_array__array_proof_rules_h_
27
28
#include <vector>
29
30
namespace
CVC3 {
31
32
class
Theorem;
33
class
Expr;
34
35
class
ArrayProofRules
{
36
public
:
37
// Destructor
38
virtual
~ArrayProofRules
() { }
39
40
////////////////////////////////////////////////////////////////////
41
// Proof rules
42
////////////////////////////////////////////////////////////////////
43
44
// ==>
45
// write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
46
//
47
// read(store, index_n) = v_n &
48
// index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
49
// (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
50
// ...
51
// (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
52
// (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
53
virtual
Theorem
rewriteSameStore
(
const
Expr
& e,
int
n) = 0;
54
55
// ==> write(store, index, value) = write(...) IFF
56
// store = write(write(...), index, read(store, index)) &
57
// value = read(write(...), index)
58
virtual
Theorem
rewriteWriteWrite
(
const
Expr
& e) = 0;
59
60
// ==> read(write(store, index1, value), index2) =
61
// ite(index1 = index2, value, read(store, index2))
62
virtual
Theorem
rewriteReadWrite
(
const
Expr
& e) = 0;
63
64
// e = read(write(store, index1, value), index2):
65
// ==> ite(index1 = index2,
66
// read(write(store, index1, value), index2) = value,
67
// read(write(store, index1, value), index2) = read(store, index2))
68
virtual
Theorem
rewriteReadWrite2
(
const
Expr
& e) = 0;
69
70
// value = read(store, index) ==>
71
// write(store, index, value) = store
72
virtual
Theorem
rewriteRedundantWrite1
(
const
Theorem
& v_eq_r,
73
const
Expr
& write) = 0;
74
75
// ==>
76
// write(write(store, index, v1), index, v2) = write(store, index, v2)
77
virtual
Theorem
rewriteRedundantWrite2
(
const
Expr
& e) = 0;
78
79
// ==>
80
// write(write(store, index1, v1), index2, v2) =
81
// write(write(store, index2, v2), index1, ite(index1 = index2, v2, v1))
82
virtual
Theorem
interchangeIndices
(
const
Expr
& e) = 0;
83
//! Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
84
virtual
Theorem
readArrayLiteral
(
const
Expr
& e) = 0;
85
86
//! Lift ite over read
87
virtual
Theorem
liftReadIte
(
const
Expr
& e) = 0;
88
89
//! a /= b |- exists i. a[i] /= b[i]
90
virtual
Theorem
arrayNotEq
(
const
Theorem
& e) = 0;
91
92
virtual
Theorem
splitOnConstants
(
const
Expr
& a,
const
std::vector<Expr>& consts) = 0;
93
94
virtual
Theorem
propagateIndexDiseq
(
const
Theorem
& read1eqread2isFalse) = 0;
95
96
};
// end of class ArrayProofRules
97
98
}
// end of namespace CVC3
99
100
#endif
Generated on Tue May 14 2013 15:43:22 for CVC3 by
1.8.3.1