<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<title>CVC3: CVC3::TheoryRecords Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="hierarchy.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a> </li>
<li class="navelem"><a class="el" href="classCVC3_1_1TheoryRecords.html">TheoryRecords</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::TheoryRecords Class Reference<div class="ingroups"><a class="el" href="group__Theories.html">Theories</a></div></div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::TheoryRecords" --><!-- doxytag: inherits="CVC3::Theory" -->
<p>This theory handles records.
<a href="classCVC3_1_1TheoryRecords.html#details">More...</a></p>
<p><code>#include <<a class="el" href="theory__records_8h_source.html">theory_records.h</a>></code></p>
<div class="dynheader">
Inheritance diagram for CVC3::TheoryRecords:</div>
<div class="dyncontent">
<div class="center">
<img src="classCVC3_1_1TheoryRecords.png" usemap="#CVC3::TheoryRecords_map" alt=""/>
<map id="CVC3::TheoryRecords_map" name="CVC3::TheoryRecords_map">
<area href="classCVC3_1_1Theory.html" title="Base class for theories." alt="CVC3::Theory" shape="rect" coords="0,0,139,24"/>
</map>
</div></div>
<p><a href="classCVC3_1_1TheoryRecords-members.html">List of all members.</a></p>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1TheoryRecords.html#a7f3fc16c1167afe2d6ff3da0a59c06fd">TheoryRecords</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)
<dl class="el"><dd class="mdescRight">Constructor. <a href="#a7f3fc16c1167afe2d6ff3da0a59c06fd"></a><br/></dl><li><a class="el" href="classCVC3_1_1TheoryRecords.html#a7e0ac2c2be6942fc04ce9c21951fe7a7">~TheoryRecords</a> ()
<li><a class="el" href="classCVC3_1_1RecordsProofRules.html">RecordsProofRules</a> * <a class="el" href="classCVC3_1_1TheoryRecords.html#acefe38731a5693d2c2b7d630088ee708">createProofRules</a> ()
<dl class="el"><dd class="mdescRight">creates a reference to the proof rules <a href="#acefe38731a5693d2c2b7d630088ee708"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#ad7fd739c906e86c0b5a135374cc10dc0">assertFact</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e)
<dl class="el"><dd class="mdescRight">assert a fact to the theory of records <a href="#ad7fd739c906e86c0b5a135374cc10dc0"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#a4780c4692ecdb6fc82f181b86cebeb68">checkSat</a> (bool fullEffort)
<dl class="el"><dd class="mdescRight">empty implementation to fit theory interface <a href="#a4780c4692ecdb6fc82f181b86cebeb68"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a56d1048536807a3bb9d746c833b75c47">rewrite</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">rewrites an expression e to one of several allowed forms <a href="#a56d1048536807a3bb9d746c833b75c47"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#a0fd20bc4ca8c7701c189ce465cd3641c">checkType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">check record or tuple type <a href="#a0fd20bc4ca8c7701c189ce465cd3641c"></a><br/></dl><li><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#ac58f7129ed3e62d2d183922cb70428ac">finiteTypeInfo</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> &n, bool enumerate, bool computeSize)
<dl class="el"><dd class="mdescRight">Compute information related to finiteness of types. <a href="#ac58f7129ed3e62d2d183922cb70428ac"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#a59dd99a5c7c1540d6517dc69dc157cfb">computeType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">computes the type of a record or a tuple <a href="#a59dd99a5c7c1540d6517dc69dc157cfb"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a0cdc07a00c674c1190f721908a77c0ca">computeBaseType</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t)
<dl class="el"><dd class="mdescRight">Compute the base type of the top-level operator of an arbitrary type. <a href="#a0cdc07a00c674c1190f721908a77c0ca"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a62ea35463c9093da92601e33698f905b">computeTypePred</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight"><a class="el" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a> specific computation of the subtyping predicate for type t applied to the expression e. <a href="#a62ea35463c9093da92601e33698f905b"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#a77c8993b2ad9daca3803c78991589351">computeModelTerm</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &v)
<dl class="el"><dd class="mdescRight">Add variables from 'e' to 'v' for constructing a concrete model. <a href="#a77c8993b2ad9daca3803c78991589351"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#a43f8bb4aeae98801e974b7f3fa0ed068">computeModel</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &vars)
<dl class="el"><dd class="mdescRight">Compute the value of a compound variable from the more primitive ones. <a href="#a43f8bb4aeae98801e974b7f3fa0ed068"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a2ae67fcdda4a2c2f55238adea0b8eabc">computeTCC</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Compute and cache the TCC of e. <a href="#a2ae67fcdda4a2c2f55238adea0b8eabc"></a><br/></dl><li>virtual <a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a72f4af007baf95a36b21246433266319">parseExprOp</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Theory-specific parsing implemented by the DP. <a href="#a72f4af007baf95a36b21246433266319"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#a707f98454898e685084f75a006cdd100">setup</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Set up the term e for call-backs when e or its children change. <a href="#a707f98454898e685084f75a006cdd100"></a><br/></dl><li>void <a class="el" href="classCVC3_1_1TheoryRecords.html#a070b5644bc6e362999305ee8bb3774ff">update</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &d)
<dl class="el"><dd class="mdescRight">Notify a theory of a new equality. <a href="#a070b5644bc6e362999305ee8bb3774ff"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & <a class="el" href="classCVC3_1_1TheoryRecords.html#aad0935f7bc94c98934c0e1690b2ec850">print</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &os, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">pretty printing <a href="#aad0935f7bc94c98934c0e1690b2ec850"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#a5aee76070091906e4b5a710d2c1e2d5b">isRecord</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Test whether expr is a record literal. <a href="#a5aee76070091906e4b5a710d2c1e2d5b"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#a71dfd95cef55ec88b9c2a29297542ab0">isRecordType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Test whether expr is a record type. <a href="#a71dfd95cef55ec88b9c2a29297542ab0"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#a9944c0e052d60784eaffb8329db47a5f">isRecordType</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &t)
<dl class="el"><dd class="mdescRight">Test whether expr is a record type. <a href="#a9944c0e052d60784eaffb8329db47a5f"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#a09dac099c2d70610b91e30cd21e00fe1">isRecordAccess</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Test whether expr is a record select/update subclass. <a href="#a09dac099c2d70610b91e30cd21e00fe1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#aa5a9cbcd30ed23792c030d70181483d3">recordExpr</a> (const std::vector< std::string > &fields, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &kids)
<dl class="el"><dd class="mdescRight">Create a record literal. <a href="#aa5a9cbcd30ed23792c030d70181483d3"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a179c7224344f4316c25ceb4626a6f2f0">recordExpr</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &fields, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &kids)
<dl class="el"><dd class="mdescRight">Create a record literal. <a href="#a179c7224344f4316c25ceb4626a6f2f0"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a4b298f0e7a25449c945480544996d105">recordType</a> (const std::vector< std::string > &fields, const std::vector< <a class="el" href="classCVC3_1_1Type.html">Type</a> > &types)
<dl class="el"><dd class="mdescRight">Create a record type. <a href="#a4b298f0e7a25449c945480544996d105"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a9a918c3cb8e49f04b4a8331eaf696c7c">recordType</a> (const std::vector< std::string > &fields, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &types)
<dl class="el"><dd class="mdescRight">Create a record type (field types are given as a vector of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>) <a href="#a9a918c3cb8e49f04b4a8331eaf696c7c"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a4c7522da56902a7f3bd8a7b530a77dc5">recordType</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &fields, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &types)
<dl class="el"><dd class="mdescRight">Create a record type (fields and types are given as a vector of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>) <a href="#a4c7522da56902a7f3bd8a7b530a77dc5"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a6123e229d2eac24364f4cf1b30927f0c">recordSelect</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &r, const std::string &field)
<dl class="el"><dd class="mdescRight">Create a record field select expression. <a href="#a6123e229d2eac24364f4cf1b30927f0c"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#ad6d5734bb5b21cada7e7958c6840e2c4">recordUpdate</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &r, const std::string &field, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &val)
<dl class="el"><dd class="mdescRight">Create a record field update expression. <a href="#ad6d5734bb5b21cada7e7958c6840e2c4"></a><br/></dl><li>const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & <a class="el" href="classCVC3_1_1TheoryRecords.html#aaf09fd297eafe6e114863581c558f163">getFields</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &r)
<dl class="el"><dd class="mdescRight">Get the list of fields from a record literal. <a href="#aaf09fd297eafe6e114863581c558f163"></a><br/></dl><li>const std::string & <a class="el" href="classCVC3_1_1TheoryRecords.html#ac45307e001d2f373bdf4116416c84b77">getField</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int i)
<dl class="el"><dd class="mdescRight">Get the i-th field name from the record literal or type. <a href="#ac45307e001d2f373bdf4116416c84b77"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1TheoryRecords.html#a8b8cf0a921555538ec1b91c08600e721">getFieldIndex</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const std::string &field)
<dl class="el"><dd class="mdescRight">Get the field index in the record literal or type. <a href="#a8b8cf0a921555538ec1b91c08600e721"></a><br/></dl><li>const std::string & <a class="el" href="classCVC3_1_1TheoryRecords.html#ac64247bde64f8819221125be780f3a1d">getField</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Get the field name from the record select and update expressions. <a href="#ac64247bde64f8819221125be780f3a1d"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a6633d0d5b34ebfaf5d6a42f72c8d4818">tupleExpr</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &kids)
<dl class="el"><dd class="mdescRight">Create a tuple literal. <a href="#a6633d0d5b34ebfaf5d6a42f72c8d4818"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a4ab484efb75ef41b5a29d5e598ab91a1">tupleType</a> (const std::vector< <a class="el" href="classCVC3_1_1Type.html">Type</a> > &types)
<dl class="el"><dd class="mdescRight">Create a tuple type. <a href="#a4ab484efb75ef41b5a29d5e598ab91a1"></a><br/></dl><li><a class="el" href="classCVC3_1_1Type.html">Type</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#aaf96b1c14ffa1741f3dfadcca8bfa212">tupleType</a> (const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &types)
<dl class="el"><dd class="mdescRight">Create a tuple type (types of components are given as Exprs) <a href="#aaf96b1c14ffa1741f3dfadcca8bfa212"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#ada5d6a109788e70405af2adee937c379">tupleSelect</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &tup, int i)
<dl class="el"><dd class="mdescRight">Create a tuple index selector expression. <a href="#ada5d6a109788e70405af2adee937c379"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a7ca579aacef4b87f4b2235da4ef1ec47">tupleUpdate</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &tup, int i, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &val)
<dl class="el"><dd class="mdescRight">Create a tuple index update expression. <a href="#a7ca579aacef4b87f4b2235da4ef1ec47"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1TheoryRecords.html#ab228944f5113535c5859cbaa2de0d811">getIndex</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Get the index from the tuple select and update expressions. <a href="#ab228944f5113535c5859cbaa2de0d811"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#a8524c2c102a95e757b3c990b44e9576d">isTupleAccess</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Test whether expr is a tuple select/update subclass. <a href="#a8524c2c102a95e757b3c990b44e9576d"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#a30d3306dd140e2ff2dbf3b145bb476cf">isTuple</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Test if expr is a tuple literal. <a href="#a30d3306dd140e2ff2dbf3b145bb476cf"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#a6c178cfcd9fd7e13a0c28ff28ce60f4d">isTupleType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Test if expr represents a tuple type. <a href="#a6c178cfcd9fd7e13a0c28ff28ce60f4d"></a><br/></dl><li>bool <a class="el" href="classCVC3_1_1TheoryRecords.html#af039aad415a0cc2be21c354d40c8f9aa">isTupleType</a> (const <a class="el" href="classCVC3_1_1Type.html">Type</a> &tp)
<dl class="el"><dd class="mdescRight">Test if 'tp' is a tuple type. <a href="#af039aad415a0cc2be21c354d40c8f9aa"></a><br/></dl></ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a243eef0e23027e100aede3646eca3617">rewriteAux</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'. <a href="#a243eef0e23027e100aede3646eca3617"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1TheoryRecords.html#a89f926d66c9b7b414160bb12f42f4485">rewriteAux</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<dl class="el"><dd class="mdescRight">Takes Thm(e), returns Thm(e'), where e rewrites to e' by rewriteAux. <a href="#a89f926d66c9b7b414160bb12f42f4485"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1RecordsProofRules.html">RecordsProofRules</a> * <a class="el" href="classCVC3_1_1TheoryRecords.html#a6bb9f23a660b77ee034a407bc46774dd">d_rules</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock"><p>This theory handles records. </p>
<p>Author: Daniel Wichs</p>
<p>Created: 7/22/03 </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00051">51</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a7f3fc16c1167afe2d6ff3da0a59c06fd"></a><!-- doxytag: member="CVC3::TheoryRecords::TheoryRecords" ref="a7f3fc16c1167afe2d6ff3da0a59c06fd" args="(TheoryCore *core)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoryRecords::TheoryRecords </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Constructor. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00096">96</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="records__theorem__producer_8cpp_source.html#l00032">createProofRules()</a>, <a class="el" href="theory__records_8h_source.html#l00052">d_rules</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00367">CVC3::ExprManager::newKind()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>, <a class="el" href="theory_8cpp_source.html#l00203">CVC3::Theory::registerTheory()</a>, <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
</div>
</div>
<a class="anchor" id="a7e0ac2c2be6942fc04ce9c21951fe7a7"></a><!-- doxytag: member="CVC3::TheoryRecords::~TheoryRecords" ref="a7e0ac2c2be6942fc04ce9c21951fe7a7" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">TheoryRecords::~TheoryRecords </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Destructor </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00125">125</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory__records_8h_source.html#l00052">d_rules</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="a243eef0e23027e100aede3646eca3617"></a><!-- doxytag: member="CVC3::TheoryRecords::rewriteAux" ref="a243eef0e23027e100aede3646eca3617" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> TheoryRecords::rewriteAux </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'. </p>
<p>When a record/tuple (dis)equality is expanded into the (dis)equalities of fields, we have to perform rewrites on the resulting record terms before the simplifier kicks in.</p>
<p>Otherwise, if we have r1.f = r2.f, but r1=r2 was asserted before, for some complex record expressions r1 and r2, then the simplifier will substitute r2 for r1, and we get r2.f=r2.f at the end, which is not a useful fact to have.</p>
<p>However, r1.f and/or r2.f may rewrite to something interesting, and the equality may yield new important facts. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00045">45</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="kinds_8h_source.html#l00061">EQ</a>, <a class="el" href="expr_8h_source.html#l01237">CVC3::Expr::getFind()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, and <a class="el" href="kinds_8h_source.html#l00068">OR</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00129">assertFact()</a>.</p>
</div>
</div>
<a class="anchor" id="a89f926d66c9b7b414160bb12f42f4485"></a><!-- doxytag: member="CVC3::TheoryRecords::rewriteAux" ref="a89f926d66c9b7b414160bb12f42f4485" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> TheoryRecords::rewriteAux </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Takes Thm(e), returns Thm(e'), where e rewrites to e' by rewriteAux. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00091">91</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="acefe38731a5693d2c2b7d630088ee708"></a><!-- doxytag: member="CVC3::TheoryRecords::createProofRules" ref="acefe38731a5693d2c2b7d630088ee708" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1RecordsProofRules.html">RecordsProofRules</a> * TheoryRecords::createProofRules </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>creates a reference to the proof rules </p>
<p>Definition at line <a class="el" href="records__theorem__producer_8cpp_source.html#l00032">32</a> of file <a class="el" href="records__theorem__producer_8cpp_source.html">records_theorem_producer.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00096">TheoryRecords()</a>.</p>
</div>
</div>
<a class="anchor" id="ad7fd739c906e86c0b5a135374cc10dc0"></a><!-- doxytag: member="CVC3::TheoryRecords::assertFact" ref="ad7fd739c906e86c0b5a135374cc10dc0" args="(const Theorem &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryRecords::assertFact </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>assert a fact to the theory of records </p>
<p>Implements <a class="el" href="group__Theory__API.html#ga58de37714dd855f4d50de15108b8dbc7">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00129">129</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory__records_8h_source.html#l00052">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory_8cpp_source.html#l00128">CVC3::Theory::enqueueFact()</a>, <a class="el" href="kinds_8h_source.html#l00061">EQ</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#a70d657a0ff820b3276c88d4208b2c6d7">CVC3::RecordsProofRules::expandEq()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory__records_8cpp_source.html#l00045">rewriteAux()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>.</p>
</div>
</div>
<a class="anchor" id="a4780c4692ecdb6fc82f181b86cebeb68"></a><!-- doxytag: member="CVC3::TheoryRecords::checkSat" ref="a4780c4692ecdb6fc82f181b86cebeb68" args="(bool fullEffort)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::TheoryRecords::checkSat </td>
<td>(</td>
<td class="paramtype">bool </td>
<td class="paramname"><em>fullEffort</em></td><td>)</td>
<td><code> [inline, virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>empty implementation to fit theory interface </p>
<p>Implements <a class="el" href="group__Theory__API.html#gae0bb3d506dad8d69da546777cae27228">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00069">69</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
</div>
</div>
<a class="anchor" id="a56d1048536807a3bb9d746c833b75c47"></a><!-- doxytag: member="CVC3::TheoryRecords::rewrite" ref="a56d1048536807a3bb9d746c833b75c47" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> TheoryRecords::rewrite </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>rewrites an expression e to one of several allowed forms </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gaa6475baeb444915fa3b2f5c58dc5148a">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00161">161</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__records_8h_source.html#l00052">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>, <a class="el" href="theory_8h_source.html#l00673">CVC3::Theory::reflexivityRule()</a>, <a class="el" href="theory_8cpp_source.html#l00512">CVC3::Theory::rewriteCC()</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#a3e3add607e89398f2cc6cc38ea99d1ff">CVC3::RecordsProofRules::rewriteLitSelect()</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#a123d754579587119040963036a57b20c">CVC3::RecordsProofRules::rewriteLitUpdate()</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#aa89519b074a161d4709cc57c72be9877">CVC3::RecordsProofRules::rewriteUpdateSelect()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="theory_8h_source.html#l00681">CVC3::Theory::transitivityRule()</a>, <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00261">computeModelTerm()</a>, <a class="el" href="theory__records_8cpp_source.html#l00508">setup()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00561">update()</a>.</p>
</div>
</div>
<a class="anchor" id="a0fd20bc4ca8c7701c189ce465cd3641c"></a><!-- doxytag: member="CVC3::TheoryRecords::checkType" ref="a0fd20bc4ca8c7701c189ce465cd3641c" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryRecords::checkType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>check record or tuple type </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gac22e5fff02a4681c3972e3637bd15748">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00344">344</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="type_8h_source.html#l00062">CVC3::Type::isFunction()</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, and <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>.</p>
</div>
</div>
<a class="anchor" id="ac58f7129ed3e62d2d183922cb70428ac"></a><!-- doxytag: member="CVC3::TheoryRecords::finiteTypeInfo" ref="ac58f7129ed3e62d2d183922cb70428ac" args="(Expr &e, Unsigned &n, bool enumerate, bool computeSize)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#af969e724f8b7016909f5804e8cea3e54">Cardinality</a> TheoryRecords::finiteTypeInfo </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Unsigned.html">Unsigned</a> & </td>
<td class="paramname"><em>n</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>enumerate</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>computeSize</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compute information related to finiteness of types. </p>
<p>Used by the TypeComputer defined in <a class="el" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a> (theories should not call this funtion directly -- they should use the methods in <a class="el" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> instead). Each theory should implement this if it contains any types that could be non-infinite.</p>
<p>1. Returns Cardinality of the type (finite, infinite, or unknown) 2. If cardinality = finite and enumerate is true, sets e to the nth element of the type if it can sets e to NULL if n is out of bounds or if unable to compute nth element 3. If cardinality = finite and computeSize is true, sets n to the size of the type if it can sets n to 0 otherwise </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga166b2a0c7ec3b09e079c2f84bb6087bc">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00381">381</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00083">CVC3::CARD_UNKNOWN</a>.</p>
</div>
</div>
<a class="anchor" id="a59dd99a5c7c1540d6517dc69dc157cfb"></a><!-- doxytag: member="CVC3::TheoryRecords::computeType" ref="a59dd99a5c7c1540d6517dc69dc157cfb" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryRecords::computeType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>computes the type of a record or a tuple </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gabaed6b47e6fdea3ae1e53ff75f1882db">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00388">388</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theory__records_8cpp_source.html#l01027">getField()</a>, <a class="el" href="theory__records_8cpp_source.html#l01037">getFieldIndex()</a>, <a class="el" href="theory__records_8cpp_source.html#l01017">getFields()</a>, <a class="el" href="theory__records_8cpp_source.html#l01092">getIndex()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>, <a class="el" href="theory__records_8cpp_source.html#l00977">recordType()</a>, <a class="el" href="expr_8h_source.html#l01427">CVC3::Expr::setType()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
</div>
</div>
<a class="anchor" id="a0cdc07a00c674c1190f721908a77c0ca"></a><!-- doxytag: member="CVC3::TheoryRecords::computeBaseType" ref="a0cdc07a00c674c1190f721908a77c0ca" args="(const Type &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> TheoryRecords::computeBaseType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>tp</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compute the base type of the top-level operator of an arbitrary type. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gaa29925192ee19a6d1f0644174cfd07af">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00484">484</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="type_8h_source.html#l00080">CVC3::Type::toString()</a>, and <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>.</p>
</div>
</div>
<a class="anchor" id="a62ea35463c9093da92601e33698f905b"></a><!-- doxytag: member="CVC3::TheoryRecords::computeTypePred" ref="a62ea35463c9093da92601e33698f905b" args="(const Type &t, const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::computeTypePred </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>t</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p><a class="el" href="classCVC3_1_1Theory.html" title="Base class for theories.">Theory</a> specific computation of the subtyping predicate for type t applied to the expression e. </p>
<p>By default returns true. Each theory needs to compute subtype predicates for the types associated with it. So, for example, the theory of records will take a record type [# f1: T1, f2: T2 #] and an expression e and will return the subtyping predicate for e, namely: computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2) </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga19d53b411ccc48276f6666183b3c5887">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00312">312</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00945">CVC3::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theory__records_8cpp_source.html#l01017">getFields()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theory_8cpp_source.html#l00406">CVC3::Theory::getTypePred()</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory__records_8cpp_source.html#l01004">recordSelect()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>, and <a class="el" href="theory__records_8cpp_source.html#l01080">tupleSelect()</a>.</p>
</div>
</div>
<a class="anchor" id="a77c8993b2ad9daca3803c78991589351"></a><!-- doxytag: member="CVC3::TheoryRecords::computeModelTerm" ref="a77c8993b2ad9daca3803c78991589351" args="(const Expr &e, std::vector< Expr > &v)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryRecords::computeModelTerm </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>v</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Add variables from 'e' to 'v' for constructing a concrete model. </p>
<p>If e is already of primitive type, do NOT add it to v. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga37309ea20a161f2529cbb0ab79f9ed3f">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00261">261</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theory__records_8cpp_source.html#l01017">getFields()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory__records_8cpp_source.html#l01004">recordSelect()</a>, <a class="el" href="theory__records_8cpp_source.html#l00161">rewrite()</a>, <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>, and <a class="el" href="theory__records_8cpp_source.html#l01080">tupleSelect()</a>.</p>
</div>
</div>
<a class="anchor" id="a43f8bb4aeae98801e974b7f3fa0ed068"></a><!-- doxytag: member="CVC3::TheoryRecords::computeModel" ref="a43f8bb4aeae98801e974b7f3fa0ed068" args="(const Expr &e, std::vector< Expr > &vars)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryRecords::computeModel </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>vars</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compute the value of a compound variable from the more primitive ones. </p>
<p>The more primitive variables for e are already assigned concrete values, and are available through <a class="el" href="classCVC3_1_1Theory.html#a4867f332c809f6efe8f01ffa45c32db3" title="Fetch the concrete assignment to the variable during model generation.">getModelValue()</a>.</p>
<p>The new value for e must be assigned using <a class="el" href="classCVC3_1_1Theory.html#a917b117d28514f486b296568fcd1cfd1" title="Assigns t a concrete value val. Used in model generation.">assignValue()</a> method.</p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is the compound type expression to assign a value;</td></tr>
<tr><td class="paramname">vars</td><td>are the variables actually assigned. Normally, 'e' is the only element of vars. However, e.g. in the case of uninterpreted functions, assigning 'f' means assigning all relevant applications of 'f' to constant values (f(0), f(5), etc.). Such applications might not be known before the model is constructed (they may be of the form f(x), f(y+z), etc., where x,y,z are still unassigned).</td></tr>
</table>
</dd>
</dl>
<p>Populating 'vars' is an opportunity for a DP to change the set of top-level "variables" to assign, if needed. In particular, it may drop 'e' from the model entirely, if it is already a concrete value by itself. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga4a5b9fff88df80582fc76fd3def55002">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00281">281</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory_8cpp_source.html#l00162">CVC3::Theory::assignValue()</a>, <a class="el" href="theory__records_8h_source.html#l00052">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#ab813be2b9919eae3952a0f0a73ed5e3a">CVC3::RecordsProofRules::expandRecord()</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#a249e1cab39dd671e11f775b8f9658629">CVC3::RecordsProofRules::expandTuple()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00240">CVC3::Theorem::getLHS()</a>, <a class="el" href="theory_8cpp_source.html#l00541">CVC3::Theory::getModelValue()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory_8h_source.html#l00686">CVC3::Theory::substitutivityRule()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="theory_8h_source.html#l00681">CVC3::Theory::transitivityRule()</a>, and <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>.</p>
</div>
</div>
<a class="anchor" id="a2ae67fcdda4a2c2f55238adea0b8eabc"></a><!-- doxytag: member="CVC3::TheoryRecords::computeTCC" ref="a2ae67fcdda4a2c2f55238adea0b8eabc" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::computeTCC </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Compute and cache the TCC of e. </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">e</td><td>is an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined.</td></tr>
</table>
</dd>
</dl>
<p>This function computes the TCC or predicate of the top-level operator of e, and recurses into children using <a class="el" href="classCVC3_1_1Theory.html#af38bdeb162a9ab9bd81ce40f598f608f" title="Compute the TCC of e, or the subtyping predicate, if e is a type.">getTCC()</a>, if necessary.</p>
<p>The default implementation is to compute TCCs recursively for all children, and return their conjunction. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga9278ad3a6eb8351865a71acd7bb7f968">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00228">228</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8cpp_source.html#l00081">CVC3::Theory::computeTCC()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theory__records_8cpp_source.html#l01027">getField()</a>, <a class="el" href="theory__records_8cpp_source.html#l01037">getFieldIndex()</a>, <a class="el" href="theory__records_8cpp_source.html#l01092">getIndex()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="theory_8cpp_source.html#l00406">CVC3::Theory::getTypePred()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>, <a class="el" href="theory_8h_source.html#l00719">CVC3::Theory::rewriteAnd()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
</div>
</div>
<a class="anchor" id="a72f4af007baf95a36b21246433266319"></a><!-- doxytag: member="CVC3::TheoryRecords::parseExprOp" ref="a72f4af007baf95a36b21246433266319" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::parseExprOp </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Theory-specific parsing implemented by the DP. </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga378bef078620e67fc80f36fa79320d91">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00880">880</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01156">CVC3::Expr::getEM()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00412">CVC3::ExprManager::getKind()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01135">CVC3::Expr::getRational()</a>, <a class="el" href="expr_8h_source.html#l01055">CVC3::Expr::getString()</a>, <a class="el" href="kinds_8h_source.html#l00046">ID</a>, <a class="el" href="classCVC3_1_1Rational.html#a1366320f4de558bb964c67f8aecedb36">CVC3::Rational::isInteger()</a>, <a class="el" href="expr_8h_source.html#l00431">CVC3::Expr::isRational()</a>, <a class="el" href="theory_8cpp_source.html#l00519">CVC3::Theory::parseExpr()</a>, <a class="el" href="kinds_8h_source.html#l00044">RAW_LIST</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>, <a class="el" href="theory__records_8cpp_source.html#l00961">recordExpr()</a>, <a class="el" href="theory__records_8cpp_source.html#l01004">recordSelect()</a>, <a class="el" href="theory__records_8cpp_source.html#l00977">recordType()</a>, <a class="el" href="theory__records_8cpp_source.html#l01010">recordUpdate()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>, <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>, <a class="el" href="theory__records_8cpp_source.html#l01058">tupleExpr()</a>, <a class="el" href="theory__records_8cpp_source.html#l01080">tupleSelect()</a>, <a class="el" href="theory__records_8cpp_source.html#l01064">tupleType()</a>, and <a class="el" href="theory__records_8cpp_source.html#l01086">tupleUpdate()</a>.</p>
</div>
</div>
<a class="anchor" id="a707f98454898e685084f75a006cdd100"></a><!-- doxytag: member="CVC3::TheoryRecords::setup" ref="a707f98454898e685084f75a006cdd100" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryRecords::setup </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Set up the term e for call-backs when e or its children change. </p>
<p>setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update. </p>
<dl class="see"><dt><b>See also:</b></dt><dd><a class="el" href="classCVC3_1_1TheoryRecords.html#a070b5644bc6e362999305ee8bb3774ff" title="Notify a theory of a new equality.">update</a> </dd></dl>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga6896845c1e25b3452238059d779fc4c8">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00508">508</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8cpp_source.html#l00142">CVC3::Theory::assertEqualities()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="theory__records_8h_source.html#l00052">d_rules</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="theory_8cpp_source.html#l00128">CVC3::Theory::enqueueFact()</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#ab813be2b9919eae3952a0f0a73ed5e3a">CVC3::RecordsProofRules::expandRecord()</a>, <a class="el" href="classCVC3_1_1RecordsProofRules.html#a249e1cab39dd671e11f775b8f9658629">CVC3::RecordsProofRules::expandTuple()</a>, <a class="el" href="theory_8cpp_source.html#l00310">CVC3::Theory::find()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, <a class="el" href="theory__records_8h_source.html#l00095">isRecordType()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="theory__records_8h_source.html#l00153">isTupleType()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8cpp_source.html#l00161">rewrite()</a>, <a class="el" href="theory_8cpp_source.html#l00459">CVC3::Theory::setupCC()</a>, <a class="el" href="theory__core_8cpp_source.html#l04260">CVC3::TheoryCore::setupTerm()</a>, <a class="el" href="theory_8h_source.html#l00686">CVC3::Theory::substitutivityRule()</a>, <a class="el" href="theory_8h_source.html#l00677">CVC3::Theory::symmetryRule()</a>, <a class="el" href="theory_8h_source.html#l00093">CVC3::Theory::theoryCore()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="theory_8h_source.html#l00681">CVC3::Theory::transitivityRule()</a>, and <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>.</p>
</div>
</div>
<a class="anchor" id="a070b5644bc6e362999305ee8bb3774ff"></a><!-- doxytag: member="CVC3::TheoryRecords::update" ref="a070b5644bc6e362999305ee8bb3774ff" args="(const Theorem &e, const Expr &d)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void TheoryRecords::update </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>d</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Notify a theory of a new equality. </p>
<p>update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.</p>
<p>To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.</p>
<dl class="see"><dt><b>See also:</b></dt><dd><a class="el" href="classCVC3_1_1TheoryRecords.html#a707f98454898e685084f75a006cdd100" title="Set up the term e for call-backs when e or its children change.">setup</a> </dd></dl>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#gac41af6a90290fe83b2ee6c53cbfc4a62">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00561">561</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8cpp_source.html#l00142">CVC3::Theory::assertEqualities()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory_8cpp_source.html#l00310">CVC3::Theory::find()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="theory_8cpp_source.html#l00097">CVC3::Theory::inconsistent()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8cpp_source.html#l00161">rewrite()</a>, <a class="el" href="theory_8h_source.html#l00681">CVC3::Theory::transitivityRule()</a>, <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>, <a class="el" href="theory_8cpp_source.html#l00473">CVC3::Theory::updateCC()</a>, and <a class="el" href="theory_8cpp_source.html#l00417">CVC3::Theory::updateHelper()</a>.</p>
</div>
</div>
<a class="anchor" id="aad0935f7bc94c98934c0e1690b2ec850"></a><!-- doxytag: member="CVC3::TheoryRecords::print" ref="aad0935f7bc94c98934c0e1690b2ec850" args="(ExprStream &os, const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & TheoryRecords::print </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [virtual]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>pretty printing </p>
<p>Reimplemented from <a class="el" href="group__Theory__API.html#ga49009744d64bbc47785f3fc5fa6884ca">CVC3::Theory</a>.</p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00584">584</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory_8h_source.html#l00079">CVC3::Theory::d_theoryUsed</a>, <a class="el" href="theory__records_8cpp_source.html#l01027">getField()</a>, <a class="el" href="theory__records_8cpp_source.html#l01017">getFields()</a>, <a class="el" href="theory__records_8cpp_source.html#l01092">getIndex()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="theory__records_8h_source.html#l00091">isRecord()</a>, <a class="el" href="theory__records_8h_source.html#l00103">isRecordAccess()</a>, <a class="el" href="theory__records_8h_source.html#l00095">isRecordType()</a>, <a class="el" href="theory__records_8h_source.html#l00147">isTupleAccess()</a>, <a class="el" href="expr__stream_8h_source.html#l00165">CVC3::ExprStream::lang()</a>, <a class="el" href="lang_8h_source.html#l00036">CVC3::LISP_LANG</a>, <a class="el" href="expr__stream_8cpp_source.html#l00301">CVC3::pop()</a>, <a class="el" href="lang_8h_source.html#l00032">CVC3::PRESENTATION_LANG</a>, <a class="el" href="expr_8cpp_source.html#l00400">CVC3::Expr::printAST()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00298">CVC3::push()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>, <a class="el" href="lang_8h_source.html#l00034">CVC3::SMTLIB_LANG</a>, <a class="el" href="lang_8h_source.html#l00052">CVC3::SMTLIB_V2_LANG</a>, <a class="el" href="expr__stream_8cpp_source.html#l00326">CVC3::space()</a>, <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
</div>
</div>
<a class="anchor" id="a5aee76070091906e4b5a710d2c1e2d5b"></a><!-- doxytag: member="CVC3::TheoryRecords::isRecord" ref="a5aee76070091906e4b5a710d2c1e2d5b" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isRecord </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test whether expr is a record literal. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00091">91</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, and <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00584">print()</a>.</p>
</div>
</div>
<a class="anchor" id="a71dfd95cef55ec88b9c2a29297542ab0"></a><!-- doxytag: member="CVC3::TheoryRecords::isRecordType" ref="a71dfd95cef55ec88b9c2a29297542ab0" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isRecordType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test whether expr is a record type. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00095">95</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, and <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8h_source.html#l00099">isRecordType()</a>, <a class="el" href="records__theorem__producer_8h_source.html#l00047">CVC3::RecordsTheoremProducer::isRecordType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00584">print()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00508">setup()</a>.</p>
</div>
</div>
<a class="anchor" id="a9944c0e052d60784eaffb8329db47a5f"></a><!-- doxytag: member="CVC3::TheoryRecords::isRecordType" ref="a9944c0e052d60784eaffb8329db47a5f" args="(const Type &t)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isRecordType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test whether expr is a record type. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00099">99</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, and <a class="el" href="theory__records_8h_source.html#l00095">isRecordType()</a>.</p>
</div>
</div>
<a class="anchor" id="a09dac099c2d70610b91e30cd21e00fe1"></a><!-- doxytag: member="CVC3::TheoryRecords::isRecordAccess" ref="a09dac099c2d70610b91e30cd21e00fe1" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isRecordAccess </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test whether expr is a record select/update subclass. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00103">103</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, and <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>.</p>
<p>Referenced by <a class="el" href="records__theorem__producer_8h_source.html#l00053">CVC3::RecordsTheoremProducer::isRecordAccess()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00584">print()</a>.</p>
</div>
</div>
<a class="anchor" id="aa5a9cbcd30ed23792c030d70181483d3"></a><!-- doxytag: member="CVC3::TheoryRecords::recordExpr" ref="aa5a9cbcd30ed23792c030d70181483d3" args="(const std::vector< std::string > &fields, const std::vector< Expr > &kids)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::recordExpr </td>
<td>(</td>
<td class="paramtype">const std::vector< std::string > & </td>
<td class="paramname"><em>fields</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>kids</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a record literal. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00961">961</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, and <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00056">CVC3::RecordsTheoremProducer::recordExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a179c7224344f4316c25ceb4626a6f2f0"></a><!-- doxytag: member="CVC3::TheoryRecords::recordExpr" ref="a179c7224344f4316c25ceb4626a6f2f0" args="(const std::vector< Expr > &fields, const std::vector< Expr > &kids)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::recordExpr </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>fields</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>kids</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a record literal. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00970">970</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>.</p>
</div>
</div>
<a class="anchor" id="a4b298f0e7a25449c945480544996d105"></a><!-- doxytag: member="CVC3::TheoryRecords::recordType" ref="a4b298f0e7a25449c945480544996d105" args="(const std::vector< std::string > &fields, const std::vector< Type > &types)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> TheoryRecords::recordType </td>
<td>(</td>
<td class="paramtype">const std::vector< std::string > & </td>
<td class="paramname"><em>fields</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Type.html">Type</a> > & </td>
<td class="paramname"><em>types</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a record type. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00977">977</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00388">computeType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, <a class="el" href="theory__records_8cpp_source.html#l00988">recordType()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00064">CVC3::RecordsTheoremProducer::recordType()</a>.</p>
</div>
</div>
<a class="anchor" id="a9a918c3cb8e49f04b4a8331eaf696c7c"></a><!-- doxytag: member="CVC3::TheoryRecords::recordType" ref="a9a918c3cb8e49f04b4a8331eaf696c7c" args="(const std::vector< std::string > &fields, const std::vector< Expr > &types)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> TheoryRecords::recordType </td>
<td>(</td>
<td class="paramtype">const std::vector< std::string > & </td>
<td class="paramname"><em>fields</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>types</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a record type (field types are given as a vector of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>) </p>
<p>Create a record type. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00988">988</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00977">recordType()</a>.</p>
</div>
</div>
<a class="anchor" id="a4c7522da56902a7f3bd8a7b530a77dc5"></a><!-- doxytag: member="CVC3::TheoryRecords::recordType" ref="a4c7522da56902a7f3bd8a7b530a77dc5" args="(const std::vector< Expr > &fields, const std::vector< Expr > &types)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> TheoryRecords::recordType </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>fields</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>types</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a record type (fields and types are given as a vector of <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>) </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l00997">997</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>.</p>
</div>
</div>
<a class="anchor" id="a6123e229d2eac24364f4cf1b30927f0c"></a><!-- doxytag: member="CVC3::TheoryRecords::recordSelect" ref="a6123e229d2eac24364f4cf1b30927f0c" args="(const Expr &r, const std::string &field)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::recordSelect </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>r</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>field</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a record field select expression. </p>
<p>Create a record field selector expression. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01004">1004</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00261">computeModelTerm()</a>, <a class="el" href="theory__records_8cpp_source.html#l00312">computeTypePred()</a>, <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00072">CVC3::RecordsTheoremProducer::recordSelect()</a>.</p>
</div>
</div>
<a class="anchor" id="ad6d5734bb5b21cada7e7958c6840e2c4"></a><!-- doxytag: member="CVC3::TheoryRecords::recordUpdate" ref="ad6d5734bb5b21cada7e7958c6840e2c4" args="(const Expr &r, const std::string &field, const Expr &val)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::recordUpdate </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>r</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>field</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>val</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a record field update expression. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01010">1010</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00075">CVC3::RecordsTheoremProducer::recordUpdate()</a>.</p>
</div>
</div>
<a class="anchor" id="aaf09fd297eafe6e114863581c558f163"></a><!-- doxytag: member="CVC3::TheoryRecords::getFields" ref="aaf09fd297eafe6e114863581c558f163" args="(const Expr &r)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & TheoryRecords::getFields </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>r</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get the list of fields from a record literal. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01017">1017</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="lang_8h_source.html#l00038">CVC3::AST_LANG</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01162">CVC3::Expr::getKids()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00261">computeModelTerm()</a>, <a class="el" href="theory__records_8cpp_source.html#l00388">computeType()</a>, <a class="el" href="theory__records_8cpp_source.html#l00312">computeTypePred()</a>, <a class="el" href="theory__records_8cpp_source.html#l01037">getFieldIndex()</a>, <a class="el" href="records__theorem__producer_8h_source.html#l00079">CVC3::RecordsTheoremProducer::getFields()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00584">print()</a>.</p>
</div>
</div>
<a class="anchor" id="ac45307e001d2f373bdf4116416c84b77"></a><!-- doxytag: member="CVC3::TheoryRecords::getField" ref="ac45307e001d2f373bdf4116416c84b77" args="(const Expr &e, int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const string & TheoryRecords::getField </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get the i-th field name from the record literal or type. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01027">1027</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01055">CVC3::Expr::getString()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__records_8h_source.html#l00030">CVC3::RECORD</a>, <a class="el" href="theory__records_8h_source.html#l00033">CVC3::RECORD_TYPE</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00228">computeTCC()</a>, <a class="el" href="theory__records_8cpp_source.html#l00388">computeType()</a>, <a class="el" href="records__theorem__producer_8h_source.html#l00082">CVC3::RecordsTheoremProducer::getField()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00584">print()</a>.</p>
</div>
</div>
<a class="anchor" id="a8b8cf0a921555538ec1b91c08600e721"></a><!-- doxytag: member="CVC3::TheoryRecords::getFieldIndex" ref="a8b8cf0a921555538ec1b91c08600e721" args="(const Expr &e, const std::string &field)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int TheoryRecords::getFieldIndex </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>field</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get the field index in the record literal or type. </p>
<p>The field must be present in the record; otherwise it's an error. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01037">1037</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory__records_8cpp_source.html#l01017">getFields()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00228">computeTCC()</a>, <a class="el" href="theory__records_8cpp_source.html#l00388">computeType()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00086">CVC3::RecordsTheoremProducer::getFieldIndex()</a>.</p>
</div>
</div>
<a class="anchor" id="ac64247bde64f8819221125be780f3a1d"></a><!-- doxytag: member="CVC3::TheoryRecords::getField" ref="ac64247bde64f8819221125be780f3a1d" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string & TheoryRecords::getField </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get the field name from the record select and update expressions. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01049">1049</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr_8h_source.html#l01050">CVC3::Expr::getName()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__records_8h_source.html#l00031">CVC3::RECORD_SELECT</a>, and <a class="el" href="theory__records_8h_source.html#l00032">CVC3::RECORD_UPDATE</a>.</p>
</div>
</div>
<a class="anchor" id="a6633d0d5b34ebfaf5d6a42f72c8d4818"></a><!-- doxytag: member="CVC3::TheoryRecords::tupleExpr" ref="a6633d0d5b34ebfaf5d6a42f72c8d4818" args="(const std::vector< Expr > &kids)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::tupleExpr </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>kids</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a tuple literal. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01058">1058</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00092">CVC3::RecordsTheoremProducer::tupleExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a4ab484efb75ef41b5a29d5e598ab91a1"></a><!-- doxytag: member="CVC3::TheoryRecords::tupleType" ref="a4ab484efb75ef41b5a29d5e598ab91a1" args="(const std::vector< Type > &types)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> TheoryRecords::tupleType </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Type.html">Type</a> > & </td>
<td class="paramname"><em>types</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a tuple type. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01064">1064</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00095">CVC3::RecordsTheoremProducer::tupleType()</a>.</p>
</div>
</div>
<a class="anchor" id="aaf96b1c14ffa1741f3dfadcca8bfa212"></a><!-- doxytag: member="CVC3::TheoryRecords::tupleType" ref="aaf96b1c14ffa1741f3dfadcca8bfa212" args="(const std::vector< Expr > &types)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a> TheoryRecords::tupleType </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>types</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a tuple type (types of components are given as Exprs) </p>
<p>Create a tuple type. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01074">1074</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>.</p>
</div>
</div>
<a class="anchor" id="ada5d6a109788e70405af2adee937c379"></a><!-- doxytag: member="CVC3::TheoryRecords::tupleSelect" ref="ada5d6a109788e70405af2adee937c379" args="(const Expr &tup, int i)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::tupleSelect </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>tup</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a tuple index selector expression. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01080">1080</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00261">computeModelTerm()</a>, <a class="el" href="theory__records_8cpp_source.html#l00312">computeTypePred()</a>, <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00101">CVC3::RecordsTheoremProducer::tupleSelect()</a>.</p>
</div>
</div>
<a class="anchor" id="a7ca579aacef4b87f4b2235da4ef1ec47"></a><!-- doxytag: member="CVC3::TheoryRecords::tupleUpdate" ref="a7ca579aacef4b87f4b2235da4ef1ec47" args="(const Expr &tup, int i, const Expr &val)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> TheoryRecords::tupleUpdate </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>tup</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>i</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>val</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Create a tuple index update expression. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01086">1086</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00880">parseExprOp()</a>, and <a class="el" href="records__theorem__producer_8h_source.html#l00104">CVC3::RecordsTheoremProducer::tupleUpdate()</a>.</p>
</div>
</div>
<a class="anchor" id="ab228944f5113535c5859cbaa2de0d811"></a><!-- doxytag: member="CVC3::TheoryRecords::getIndex" ref="ab228944f5113535c5859cbaa2de0d811" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int TheoryRecords::getIndex </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Get the index from the tuple select and update expressions. </p>
<p>Definition at line <a class="el" href="theory__records_8cpp_source.html#l01092">1092</a> of file <a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a>.</p>
<p>References <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1Rational.html#a094636dfa3a740640ca1b0c7406f7e8f">CVC3::Rational::getInt()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01135">CVC3::Expr::getRational()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00228">computeTCC()</a>, <a class="el" href="theory__records_8cpp_source.html#l00388">computeType()</a>, <a class="el" href="records__theorem__producer_8h_source.html#l00107">CVC3::RecordsTheoremProducer::getIndex()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00584">print()</a>.</p>
</div>
</div>
<a class="anchor" id="a8524c2c102a95e757b3c990b44e9576d"></a><!-- doxytag: member="CVC3::TheoryRecords::isTupleAccess" ref="a8524c2c102a95e757b3c990b44e9576d" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isTupleAccess </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test whether expr is a tuple select/update subclass. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00147">147</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="theory__records_8h_source.html#l00035">CVC3::TUPLE_SELECT</a>, and <a class="el" href="theory__records_8h_source.html#l00036">CVC3::TUPLE_UPDATE</a>.</p>
<p>Referenced by <a class="el" href="records__theorem__producer_8h_source.html#l00110">CVC3::RecordsTheoremProducer::isTupleAccess()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00584">print()</a>.</p>
</div>
</div>
<a class="anchor" id="a30d3306dd140e2ff2dbf3b145bb476cf"></a><!-- doxytag: member="CVC3::TheoryRecords::isTuple" ref="a30d3306dd140e2ff2dbf3b145bb476cf" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isTuple </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test if expr is a tuple literal. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00151">151</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, and <a class="el" href="theory__records_8h_source.html#l00034">CVC3::TUPLE</a>.</p>
</div>
</div>
<a class="anchor" id="a6c178cfcd9fd7e13a0c28ff28ce60f4d"></a><!-- doxytag: member="CVC3::TheoryRecords::isTupleType" ref="a6c178cfcd9fd7e13a0c28ff28ce60f4d" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isTupleType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test if expr represents a tuple type. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00153">153</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, and <a class="el" href="theory__records_8h_source.html#l00037">CVC3::TUPLE_TYPE</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00508">setup()</a>.</p>
</div>
</div>
<a class="anchor" id="af039aad415a0cc2be21c354d40c8f9aa"></a><!-- doxytag: member="CVC3::TheoryRecords::isTupleType" ref="af039aad415a0cc2be21c354d40c8f9aa" args="(const Type &tp)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool CVC3::TheoryRecords::isTupleType </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Type.html">Type</a> & </td>
<td class="paramname"><em>tp</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Test if 'tp' is a tuple type. </p>
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00156">156</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>References <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, and <a class="el" href="theory__records_8h_source.html#l00156">isTupleType()</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8h_source.html#l00156">isTupleType()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a6bb9f23a660b77ee034a407bc46774dd"></a><!-- doxytag: member="CVC3::TheoryRecords::d_rules" ref="a6bb9f23a660b77ee034a407bc46774dd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1RecordsProofRules.html">RecordsProofRules</a>* <a class="el" href="classCVC3_1_1TheoryRecords.html#a6bb9f23a660b77ee034a407bc46774dd">CVC3::TheoryRecords::d_rules</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="theory__records_8h_source.html#l00052">52</a> of file <a class="el" href="theory__records_8h_source.html">theory_records.h</a>.</p>
<p>Referenced by <a class="el" href="theory__records_8cpp_source.html#l00129">assertFact()</a>, <a class="el" href="theory__records_8cpp_source.html#l00281">computeModel()</a>, <a class="el" href="theory__records_8cpp_source.html#l00161">rewrite()</a>, <a class="el" href="theory__records_8cpp_source.html#l00508">setup()</a>, <a class="el" href="theory__records_8cpp_source.html#l00096">TheoryRecords()</a>, and <a class="el" href="theory__records_8cpp_source.html#l00125">~TheoryRecords()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="theory__records_8h_source.html">theory_records.h</a></li>
<li><a class="el" href="records__theorem__producer_8cpp_source.html">records_theorem_producer.cpp</a></li>
<li><a class="el" href="theory__records_8cpp_source.html">theory_records.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
