CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
theory_uf.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file theory_uf.h
4
*
5
* Author: Clark Barrett
6
*
7
* Created: Fri Jan 17 18:25:40 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
21
#ifndef _cvc3__include__theory_uf_h_
22
#define _cvc3__include__theory_uf_h_
23
24
#include "
theory.h
"
25
#include "
cdmap.h
"
26
27
namespace
CVC3 {
28
29
class
UFProofRules;
30
31
//! Local kinds for transitive closure of binary relations
32
typedef
enum
{
33
TRANS_CLOSURE
= 500,
34
OLD_ARROW
// for backward compatibility with old function declarations
35
}
UFKinds
;
36
37
/*****************************************************************************/
38
/*!
39
*\class TheoryUF
40
*\ingroup Theories
41
*\brief This theory handles uninterpreted functions.
42
*
43
* Author: Clark Barrett
44
*
45
* Created: Sat Feb 8 14:51:19 2003
46
*/
47
/*****************************************************************************/
48
class
TheoryUF
:
public
Theory
{
49
UFProofRules
*
d_rules
;
50
//! Flag to include function applications to the concrete model
51
const
bool
&
d_applicationsInModel
;
52
53
// For computing transitive closure of binary relations
54
typedef
struct
TCMapPair
{
55
ExprMap<CDList<Theorem>
*>
appearsFirstMap
;
56
ExprMap<CDList<Theorem>
*>
appearsSecondMap
;
57
}
TCMapPair
;
58
59
ExprMap<TCMapPair*>
d_transClosureMap
;
60
61
//! Backtracking list of function applications
62
/*! Used for building concrete models and beta-reducing
63
* lambda-expressions. */
64
CDList<Expr>
d_funApplications
;
65
//! Pointer to the last unprocessed element (for lambda expansions)
66
CDO<size_t>
d_funApplicationsIdx
;
67
//! The pointers to the last unprocessed shared pair
68
CDO<size_t>
d_sharedIdx1
,
d_sharedIdx2
;
69
//! The set of all shared terms
70
CDMap<Expr, bool>
d_sharedTermsMap
;
71
72
public
:
73
TheoryUF
(
TheoryCore
* core);
74
~TheoryUF
();
75
76
// Trusted method that creates the proof rules class (used in constructor).
77
// Implemented in uf_theorem_producer.cpp
78
UFProofRules
*
createProofRules
();
79
80
// Theory interface
81
void
addSharedTerm
(
const
Expr
& e);
82
void
assertFact
(
const
Theorem
& e);
83
void
checkSat
(
bool
fullEffort);
84
Theorem
rewrite
(
const
Expr
& e);
85
void
setup
(
const
Expr
& e);
86
void
update
(
const
Theorem
& e,
const
Expr
& d);
87
void
checkType
(
const
Expr
& e);
88
Cardinality
finiteTypeInfo
(
Expr
& e,
Unsigned
& n,
89
bool
enumerate,
bool
computeSize);
90
void
computeType
(
const
Expr
& e);
91
Type
computeBaseType
(
const
Type
& t);
92
void
computeModelTerm
(
const
Expr
& e, std::vector<Expr>& v);
93
void
computeModel
(
const
Expr
& e, std::vector<Expr>& vars);
94
Expr
computeTCC
(
const
Expr
& e);
95
virtual
Expr
parseExprOp
(
const
Expr
& e);
96
ExprStream
&
print
(
ExprStream
& os,
const
Expr
& e);
97
98
//! Create a new LAMBDA-abstraction
99
Expr
lambdaExpr
(
const
std::vector<Expr>& vars,
const
Expr
& body);
100
//! Create a transitive closure expression
101
Expr
transClosureExpr
(
const
std::string& name,
102
const
Expr
& e1,
const
Expr
& e2);
103
private
:
104
void
printSmtLibShared
(
ExprStream
& os,
const
Expr
& e);
105
};
106
107
}
108
109
#endif
Generated on Mon Aug 19 2013 14:42:45 for CVC3 by
1.8.4