CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_records
records_proof_rules.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file records_proof_rules.h
4
*
5
* Author: Daniel Wichs
6
*
7
* Created: Jul 22 22:59:07 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
*/
19
/*****************************************************************************/
20
#ifndef _cvc3__records_proof_rules_h_
21
#define _cvc3__records_proof_rules_h_
22
23
namespace
CVC3 {
24
25
class
Expr;
26
class
Theorem;
27
28
class
RecordsProofRules
{
29
public
:
30
//!< Destructor
31
virtual
~RecordsProofRules
() { }
32
33
//! ==> (REC_LITERAL (f1 v1) ... (fi vi) ...).fi = vi
34
virtual
Theorem
rewriteLitSelect
(
const
Expr
&e) = 0;
35
36
//! ==> (REC_SELECT (REC_UPDATE e fi vi) fi) = vi
37
virtual
Theorem
rewriteUpdateSelect
(
const
Expr
& e) = 0;
38
39
40
//! ==> (REC_UPDATE (REC_LITERAL (f1 v1) ... (fi vi) ...) fi v') =(REC_LITERAL (f1 v1) ... (fi v') ...)
41
virtual
Theorem
rewriteLitUpdate
(
const
Expr
& e) = 0;
42
//! From T|- e = e' return T|- AND (e.i = e'.i) for all i
43
virtual
Theorem
expandEq
(
const
Theorem
& eqThrm) = 0;
44
//! From T|- NOT e=e' return T|- NOT AND (e.i = e'.i) for all i
45
virtual
Theorem
expandNeq
(
const
Theorem
& neqThrm) = 0;
46
//! Expand a record into a literal: |- e = (# f1:=e.f1, ..., fn:=e.fn #)
47
virtual
Theorem
expandRecord
(
const
Expr
& e) = 0;
48
//! Expand a tuple into a literal: |- e = (e.0, ..., e.n-1)
49
virtual
Theorem
expandTuple
(
const
Expr
& e) = 0;
50
};
51
}
52
#endif
Generated on Tue May 14 2013 14:44:52 for CVC3 by
1.8.3.1