CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_array
array_theorem_producer.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file array_theorem_producer.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: TRUSTED implementation of array proof rules. DO
22
* NOT use this file in any DP code, use the exported API in
23
* array_proof_rules.h instead.
24
*
25
*/
26
/*****************************************************************************/
27
#ifndef _cvc3__theory_array__array_theorem_producer_h_
28
#define _cvc3__theory_array__array_theorem_producer_h_
29
30
#include "
array_proof_rules.h
"
31
#include "
theorem_producer.h
"
32
33
namespace
CVC3 {
34
35
class
TheoryArray;
36
37
class
ArrayTheoremProducer
:
public
ArrayProofRules
,
public
TheoremProducer
{
38
private
:
39
TheoryArray
*
d_theoryArray
;
40
41
public
:
42
// Constructor
43
ArrayTheoremProducer
(
TheoryArray
* theoryArray);
44
45
////////////////////////////////////////////////////////////////////
46
// Proof rules
47
////////////////////////////////////////////////////////////////////
48
49
// ==>
50
// write(store, index_0, v_0, index_1, v_1, ..., index_n, v_n) = store IFF
51
//
52
// read(store, index_n) = v_n &
53
// index_{n-1} != index_n -> read(store, index_{n-1}) = v_{n-1} &
54
// (index_{n-2} != index_{n-1} & index_{n-2} != index_n) -> read(store, index_{n-2}) = v_{n-2} &
55
// ...
56
// (index_1 != index_2 & ... & index_1 != index_n) -> read(store, index_1) = v_1
57
// (index_0 != index_1 & index_0 != index_2 & ... & index_0 != index_n) -> read(store, index_0) = v_0
58
Theorem
rewriteSameStore
(
const
Expr
& e,
int
n);
59
60
// ==> write(store, index, value) = write(...) IFF
61
// store = write(write(...), index, read(store, index)) &
62
// value = read(write(...), index)
63
Theorem
rewriteWriteWrite
(
const
Expr
& e);
64
65
// ==> read(write(store, index1, value), index2) =
66
// ite(index1 = index2, value, read(store, index2))
67
Theorem
rewriteReadWrite
(
const
Expr
& e);
68
69
// e = read(write(store, index1, value), index2):
70
// ==> ite(index1 = index2,
71
// read(write(store, index1, value), index2) = value,
72
// read(write(store, index1, value), index2) = read(store, index2))
73
Theorem
rewriteReadWrite2
(
const
Expr
& e);
74
75
// value = read(store, index) ==>
76
// write(store, index, value) = store
77
Theorem
rewriteRedundantWrite1
(
const
Theorem
& v_eq_r,
78
const
Expr
& write);
79
80
// ==>
81
// write(write(store, index, v1), index, v2) = write(store, index, v2)
82
Theorem
rewriteRedundantWrite2
(
const
Expr
& e);
83
84
// ==>
85
// write(write(store, index1, v1), index2, v2) =
86
// write(write(store, index2, v2), index1, ite(index1 = index2, v2, v1))
87
Theorem
interchangeIndices
(
const
Expr
& e);
88
// Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
89
Theorem
readArrayLiteral
(
const
Expr
& e);
90
91
Theorem
liftReadIte
(
const
Expr
& e);
92
93
// a /= b |- exists i. a[i] /= b[i]
94
Theorem
arrayNotEq
(
const
Theorem
& e);
95
96
Theorem
splitOnConstants
(
const
Expr
& a,
const
std::vector<Expr>& consts);
97
98
Theorem
propagateIndexDiseq
(
const
Theorem
& read1eqread2isFalse);
99
100
};
// end of class ArrayTheoremProducer
101
102
}
// end of namespace CVC3
103
104
#endif
Generated on Sat May 18 2013 12:01:23 for CVC3 by
1.8.3.1