CVC3::TheoryRecords Class Reference
[Theories]

This theory handles records. More...

#include <theory_records.h>

Inheritance diagram for CVC3::TheoryRecords:

Inheritance graph
[legend]
Collaboration diagram for CVC3::TheoryRecords:

Collaboration graph
[legend]

List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

This theory handles records.

Author: Daniel Wichs

Created: 7/22/03

Definition at line 51 of file theory_records.h.

Constructor & Destructor Documentation

TheoryRecords::TheoryRecords ( TheoryCore *  core  ) 

Constructor.

Definition at line 96 of file theory_records.cpp.

References createProofRules(), d_rules, CVC3::Theory::getEM(), CVC3::ExprManager::newKind(), CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::RECORD_TYPE, CVC3::RECORD_UPDATE, CVC3::Theory::registerTheory(), CVC3::TUPLE, CVC3::TUPLE_SELECT, CVC3::TUPLE_TYPE, and CVC3::TUPLE_UPDATE.

TheoryRecords::~TheoryRecords (  ) 

Destructor

Definition at line 125 of file theory_records.cpp.

References d_rules.

Member Function Documentation

Theorem TheoryRecords::rewriteAux ( const Expr &  e  )  [private]

Auxiliary rewrites: Processing of AND and OR of equations. Returns e=e'.

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.

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.

However, r1.f and/or r2.f may rewrite to something interesting, and the equality may yield new important facts.

Definition at line 45 of file theory_records.cpp.

References CVC3::AND, CVC3::Expr::arity(), CVC3::EQ, CVC3::Expr::getFind(), CVC3::Expr::getKind(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::IFF, CVC3::NOT, CVC3::OR, CVC3::Theory::reflexivityRule(), rewrite(), CVC3::Theory::substitutivityRule(), and CVC3::Theory::transitivityRule().

Referenced by assertFact(), and rewriteAux().

Theorem TheoryRecords::rewriteAux ( const Theorem &  thm  )  [private]

Takes Thm(e), returns Thm(e'), where e rewrites to e' by rewriteAux.

Definition at line 91 of file theory_records.cpp.

References CVC3::Theorem::getExpr(), CVC3::Theory::iffMP(), and rewriteAux().

RecordsProofRules * TheoryRecords::createProofRules (  ) 

creates a reference to the proof rules

Definition at line 32 of file records_theorem_producer.cpp.

References CVC3::Theory::theoryCore().

Referenced by TheoryRecords().

void TheoryRecords::assertFact ( const Theorem &  e  )  [virtual]

assert a fact to the theory of records

Implements CVC3::Theory.

Definition at line 129 of file theory_records.cpp.

References d_rules, DebugAssert, CVC3::Theory::enqueueFact(), CVC3::EQ, CVC3::RecordsProofRules::expandEq(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::IFF, CVC3::NOT, CVC3::RECORD_TYPE, rewriteAux(), CVC3::Expr::toString(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::TUPLE_TYPE.

void CVC3::TheoryRecords::checkSat ( bool  fullEffort  )  [inline, virtual]

empty implementation to fit theory interface

Implements CVC3::Theory.

Definition at line 69 of file theory_records.h.

Theorem TheoryRecords::rewrite ( const Expr &  e  )  [virtual]

rewrites an expression e to one of several allowed forms

Reimplemented from CVC3::Theory.

Definition at line 161 of file theory_records.cpp.

References CVC3::Expr::arity(), d_rules, DebugAssert, CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::RECORD_UPDATE, CVC3::Theory::reflexivityRule(), CVC3::Theory::rewriteCC(), CVC3::RecordsProofRules::rewriteLitSelect(), CVC3::RecordsProofRules::rewriteLitUpdate(), CVC3::RecordsProofRules::rewriteUpdateSelect(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::Theory::transitivityRule(), CVC3::TUPLE, CVC3::TUPLE_SELECT, and CVC3::TUPLE_UPDATE.

Referenced by computeModelTerm(), rewriteAux(), setup(), and update().

void TheoryRecords::checkType ( const Expr &  e  )  [virtual]

check record or tuple type

Reimplemented from CVC3::Theory.

Definition at line 344 of file theory_records.cpp.

References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Theory::getEM(), CVC3::Expr::getOpKind(), CVC3::Type::isBool(), CVC3::Type::isFunction(), CVC3::RECORD_TYPE, CVC3::Expr::toString(), and CVC3::TUPLE_TYPE.

Cardinality TheoryRecords::finiteTypeInfo ( Expr &  e,
Unsigned &  n,
bool  enumerate,
bool  computeSize 
) [virtual]

Compute information related to finiteness of types.

Used by the TypeComputer defined in TheoryCore (theories should not call this funtion directly -- they should use the methods in Type instead). Each theory should implement this if it contains any types that could be non-infinite.

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

Reimplemented from CVC3::Theory.

Definition at line 381 of file theory_records.cpp.

References CVC3::CARD_UNKNOWN.

void TheoryRecords::computeType ( const Expr &  e  )  [virtual]

computes the type of a record or a tuple

Reimplemented from CVC3::Theory.

Definition at line 388 of file theory_records.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), getField(), getFieldIndex(), getFields(), getIndex(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::RECORD_TYPE, CVC3::RECORD_UPDATE, recordType(), CVC3::Expr::setType(), CVC3::Expr::toString(), CVC3::TUPLE, CVC3::TUPLE_SELECT, CVC3::TUPLE_TYPE, and CVC3::TUPLE_UPDATE.

Type TheoryRecords::computeBaseType ( const Type &  tp  )  [virtual]

Compute the base type of the top-level operator of an arbitrary type.

Reimplemented from CVC3::Theory.

Definition at line 484 of file theory_records.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), CVC3::RECORD_TYPE, CVC3::Type::toString(), and CVC3::TUPLE_TYPE.

Expr TheoryRecords::computeTypePred ( const Type &  t,
const Expr &  e 
) [virtual]

Theory specific computation of the subtyping predicate for type t applied to the expression e.

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)

Reimplemented from CVC3::Theory.

Definition at line 312 of file theory_records.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), DebugAssert, CVC3::Type::getExpr(), getFields(), CVC3::Expr::getOpKind(), CVC3::Theory::getTypePred(), CVC3::RECORD_TYPE, recordSelect(), CVC3::TRACE, CVC3::TUPLE_TYPE, and tupleSelect().

void TheoryRecords::computeModelTerm ( const Expr &  e,
std::vector< Expr > &  v 
) [virtual]

Add variables from 'e' to 'v' for constructing a concrete model.

If e is already of primitive type, do NOT add it to v.

Reimplemented from CVC3::Theory.

Definition at line 261 of file theory_records.cpp.

References CVC3::Expr::arity(), CVC3::Type::getExpr(), getFields(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::RECORD_TYPE, recordSelect(), rewrite(), CVC3::TUPLE_TYPE, and tupleSelect().

void TheoryRecords::computeModel ( const Expr &  e,
std::vector< Expr > &  vars 
) [virtual]

Compute the value of a compound variable from the more primitive ones.

The more primitive variables for e are already assigned concrete values, and are available through getModelValue().

The new value for e must be assigned using assignValue() method.

Parameters:
e is the compound type expression to assign a value;
vars 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).
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.

Reimplemented from CVC3::Theory.

Definition at line 281 of file theory_records.cpp.

References CVC3::Expr::arity(), CVC3::Theory::assignValue(), d_rules, DebugAssert, CVC3::RecordsProofRules::expandRecord(), CVC3::RecordsProofRules::expandTuple(), CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theory::getModelValue(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::RECORD_TYPE, CVC3::Theory::substitutivityRule(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), and CVC3::TUPLE_TYPE.

Expr TheoryRecords::computeTCC ( const Expr &  e  )  [virtual]

Compute and cache the TCC of e.

Parameters:
e is an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined.
This function computes the TCC or predicate of the top-level operator of e, and recurses into children using getTCC(), if necessary.

The default implementation is to compute TCCs recursively for all children, and return their conjunction.

Reimplemented from CVC3::Theory.

Definition at line 228 of file theory_records.cpp.

References CVC3::Theory::computeTCC(), DebugAssert, CVC3::Type::getExpr(), getField(), getFieldIndex(), getIndex(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Theory::getTypePred(), CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::RECORD_UPDATE, CVC3::Theory::rewriteAnd(), CVC3::TRACE, CVC3::TUPLE, CVC3::TUPLE_SELECT, and CVC3::TUPLE_UPDATE.

Expr TheoryRecords::parseExprOp ( const Expr &  e  )  [virtual]

Theory-specific parsing implemented by the DP.

Reimplemented from CVC3::Theory.

Definition at line 879 of file theory_records.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getEM(), CVC3::Type::getExpr(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::Expr::getString(), CVC3::ID, CVC3::Rational::isInteger(), CVC3::Expr::isRational(), CVC3::Theory::parseExpr(), CVC3::RAW_LIST, CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::RECORD_TYPE, CVC3::RECORD_UPDATE, recordExpr(), recordSelect(), recordType(), recordUpdate(), CVC3::Expr::toString(), CVC3::TRACE, CVC3::TUPLE, CVC3::TUPLE_SELECT, CVC3::TUPLE_TYPE, CVC3::TUPLE_UPDATE, tupleExpr(), tupleSelect(), tupleType(), and tupleUpdate().

void TheoryRecords::setup ( const Expr &  e  )  [virtual]

Set up the term e for call-backs when e or its children change.

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.

See also:
update

Reimplemented from CVC3::Theory.

Definition at line 508 of file theory_records.cpp.

References CVC3::Theory::assertEqualities(), CVC3::Expr::begin(), d_rules, CVC3::Expr::end(), CVC3::Theory::enqueueFact(), CVC3::RecordsProofRules::expandRecord(), CVC3::RecordsProofRules::expandTuple(), CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::int2string(), CVC3::Theorem::isNull(), isRecordType(), CVC3::Expr::isTerm(), isTupleType(), CVC3::RECORD, rewrite(), CVC3::Theory::setupCC(), CVC3::TheoryCore::setupTerm(), CVC3::Theory::substitutivityRule(), CVC3::Theory::symmetryRule(), CVC3::Theory::theoryCore(), CVC3::TRACE, CVC3::Theory::transitivityRule(), and CVC3::TUPLE.

void TheoryRecords::update ( const Theorem &  e,
const Expr &  d 
) [virtual]

Notify a theory of a new equality.

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.

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.

See also:
setup

Reimplemented from CVC3::Theory.

Definition at line 561 of file theory_records.cpp.

References CVC3::Theory::assertEqualities(), DebugAssert, CVC3::Theory::find(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::Theory::inconsistent(), CVC3::RECORD, rewrite(), CVC3::Theory::transitivityRule(), CVC3::TUPLE, CVC3::Theory::updateCC(), and CVC3::Theory::updateHelper().

ExprStream & TheoryRecords::print ( ExprStream &  os,
const Expr &  e 
) [virtual]

pretty printing

Reimplemented from CVC3::Theory.

Definition at line 584 of file theory_records.cpp.

References CVC3::Expr::arity(), CVC3::Theory::d_theoryUsed, getField(), getFields(), getIndex(), CVC3::Expr::getOpKind(), isRecord(), isRecordAccess(), isRecordType(), isTupleAccess(), CVC3::ExprStream::lang(), CVC3::LISP_LANG, CVC3::pop(), CVC3::PRESENTATION_LANG, CVC3::Expr::printAST(), CVC3::push(), CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::RECORD_TYPE, CVC3::RECORD_UPDATE, CVC3::SMTLIB_LANG, CVC3::space(), CVC3::TUPLE, CVC3::TUPLE_SELECT, CVC3::TUPLE_TYPE, and CVC3::TUPLE_UPDATE.

bool CVC3::TheoryRecords::isRecord ( const Expr &  e  )  [inline]

Test whether expr is a record literal.

Definition at line 91 of file theory_records.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and CVC3::RECORD.

Referenced by print().

bool CVC3::TheoryRecords::isRecordType ( const Expr &  e  )  [inline]

Test whether expr is a record type.

Definition at line 95 of file theory_records.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and CVC3::RECORD_TYPE.

Referenced by isRecordType(), CVC3::RecordsTheoremProducer::isRecordType(), print(), and setup().

bool CVC3::TheoryRecords::isRecordType ( const Type &  t  )  [inline]

Test whether expr is a record type.

Definition at line 99 of file theory_records.h.

References CVC3::Type::getExpr(), and isRecordType().

bool CVC3::TheoryRecords::isRecordAccess ( const Expr &  e  )  [inline]

Test whether expr is a record select/update subclass.

Definition at line 103 of file theory_records.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::RECORD_SELECT, and CVC3::RECORD_UPDATE.

Referenced by CVC3::RecordsTheoremProducer::isRecordAccess(), and print().

Expr TheoryRecords::recordExpr ( const std::vector< std::string > &  fields,
const std::vector< Expr > &  kids 
)

Create a record literal.

Definition at line 960 of file theory_records.cpp.

References CVC3::Expr::begin(), and CVC3::Theory::getEM().

Referenced by parseExprOp(), CVC3::VCL::recordExpr(), and CVC3::RecordsTheoremProducer::recordExpr().

Expr TheoryRecords::recordExpr ( const std::vector< Expr > &  fields,
const std::vector< Expr > &  kids 
)

Create a record literal.

Definition at line 969 of file theory_records.cpp.

References CVC3::RECORD.

Type TheoryRecords::recordType ( const std::vector< std::string > &  fields,
const std::vector< Type > &  types 
)

Create a record type.

Definition at line 976 of file theory_records.cpp.

Referenced by computeType(), parseExprOp(), CVC3::VCL::recordType(), recordType(), and CVC3::RecordsTheoremProducer::recordType().

Type TheoryRecords::recordType ( const std::vector< std::string > &  fields,
const std::vector< Expr > &  types 
)

Create a record type (field types are given as a vector of Expr).

Create a record type.

Definition at line 987 of file theory_records.cpp.

References CVC3::Theory::getEM(), and recordType().

Type TheoryRecords::recordType ( const std::vector< Expr > &  fields,
const std::vector< Expr > &  types 
)

Create a record type (fields and types are given as a vector of Expr).

Definition at line 996 of file theory_records.cpp.

References CVC3::RECORD_TYPE.

Expr TheoryRecords::recordSelect ( const Expr &  r,
const std::string &  field 
)

Create a record field select expression.

Create a record field selector expression.

Definition at line 1003 of file theory_records.cpp.

References CVC3::Theory::getEM(), and CVC3::RECORD_SELECT.

Referenced by computeModelTerm(), computeTypePred(), parseExprOp(), CVC3::RecordsTheoremProducer::recordSelect(), and CVC3::VCL::recSelectExpr().

Expr TheoryRecords::recordUpdate ( const Expr &  r,
const std::string &  field,
const Expr &  val 
)

Create a record field update expression.

Definition at line 1009 of file theory_records.cpp.

References CVC3::Theory::getEM(), and CVC3::RECORD_UPDATE.

Referenced by parseExprOp(), CVC3::RecordsTheoremProducer::recordUpdate(), and CVC3::VCL::recUpdateExpr().

const vector< Expr > & TheoryRecords::getFields ( const Expr &  r  ) 

Get the list of fields from a record literal.

Definition at line 1016 of file theory_records.cpp.

References CVC3::AST_LANG, DebugAssert, CVC3::Expr::getKids(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::RECORD, CVC3::RECORD_TYPE, and CVC3::Expr::toString().

Referenced by computeModelTerm(), computeType(), computeTypePred(), getFieldIndex(), CVC3::RecordsTheoremProducer::getFields(), and print().

const string & TheoryRecords::getField ( const Expr &  e,
int  i 
)

Get the i-th field name from the record literal or type.

Definition at line 1026 of file theory_records.cpp.

References DebugAssert, CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getString(), CVC3::Expr::isApply(), CVC3::RECORD, CVC3::RECORD_TYPE, and CVC3::Expr::toString().

Referenced by computeTCC(), computeType(), CVC3::RecordsTheoremProducer::getField(), and print().

int TheoryRecords::getFieldIndex ( const Expr &  e,
const std::string &  field 
)

Get the field index in the record literal or type.

The field must be present in the record; otherwise it's an error.

Definition at line 1036 of file theory_records.cpp.

References DebugAssert, getFields(), and CVC3::Expr::toString().

Referenced by computeTCC(), computeType(), and CVC3::RecordsTheoremProducer::getFieldIndex().

const std::string & TheoryRecords::getField ( const Expr &  e  ) 

Get the field name from the record select and update expressions.

Definition at line 1048 of file theory_records.cpp.

References DebugAssert, CVC3::Expr::getName(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::RECORD_SELECT, and CVC3::RECORD_UPDATE.

Expr TheoryRecords::tupleExpr ( const std::vector< Expr > &  kids  ) 

Create a tuple literal.

Definition at line 1057 of file theory_records.cpp.

References CVC3::Theory::getEM(), and CVC3::TUPLE.

Referenced by parseExprOp(), CVC3::VCL::tupleExpr(), and CVC3::RecordsTheoremProducer::tupleExpr().

Type TheoryRecords::tupleType ( const std::vector< Type > &  types  ) 

Create a tuple type.

Definition at line 1063 of file theory_records.cpp.

References CVC3::Theory::getEM(), and CVC3::TUPLE_TYPE.

Referenced by parseExprOp(), CVC3::VCL::tupleType(), and CVC3::RecordsTheoremProducer::tupleType().

Type TheoryRecords::tupleType ( const std::vector< Expr > &  types  ) 

Create a tuple type (types of components are given as Exprs).

Create a tuple type.

Definition at line 1073 of file theory_records.cpp.

References CVC3::Theory::getEM(), and CVC3::TUPLE_TYPE.

Expr TheoryRecords::tupleSelect ( const Expr &  tup,
int  i 
)

Create a tuple index selector expression.

Definition at line 1079 of file theory_records.cpp.

References CVC3::Theory::getEM(), and CVC3::TUPLE_SELECT.

Referenced by computeModelTerm(), computeTypePred(), parseExprOp(), CVC3::RecordsTheoremProducer::tupleSelect(), and CVC3::VCL::tupleSelectExpr().

Expr TheoryRecords::tupleUpdate ( const Expr &  tup,
int  i,
const Expr &  val 
)

Create a tuple index update expression.

Definition at line 1085 of file theory_records.cpp.

References CVC3::Theory::getEM(), and CVC3::TUPLE_UPDATE.

Referenced by parseExprOp(), CVC3::RecordsTheoremProducer::tupleUpdate(), and CVC3::VCL::tupleUpdateExpr().

int TheoryRecords::getIndex ( const Expr &  e  ) 

Get the index from the tuple select and update expressions.

Definition at line 1091 of file theory_records.cpp.

References DebugAssert, CVC3::Rational::getInt(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::Expr::getRational(), CVC3::Expr::isApply(), CVC3::TUPLE_SELECT, and CVC3::TUPLE_UPDATE.

Referenced by computeTCC(), computeType(), CVC3::RecordsTheoremProducer::getIndex(), and print().

bool CVC3::TheoryRecords::isTupleAccess ( const Expr &  e  )  [inline]

Test whether expr is a tuple select/update subclass.

Definition at line 147 of file theory_records.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::TUPLE_SELECT, and CVC3::TUPLE_UPDATE.

Referenced by CVC3::RecordsTheoremProducer::isTupleAccess(), and print().

bool CVC3::TheoryRecords::isTuple ( const Expr &  e  )  [inline]

Test if expr is a tuple literal.

Definition at line 151 of file theory_records.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and CVC3::TUPLE.

bool CVC3::TheoryRecords::isTupleType ( const Expr &  e  )  [inline]

Test if expr represents a tuple type.

Definition at line 153 of file theory_records.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and CVC3::TUPLE_TYPE.

Referenced by setup().

bool CVC3::TheoryRecords::isTupleType ( const Type &  tp  )  [inline]

Test if 'tp' is a tuple type.

Definition at line 156 of file theory_records.h.

References CVC3::Type::getExpr(), and isTupleType().

Referenced by isTupleType().

Member Data Documentation

RecordsProofRules* CVC3::TheoryRecords::d_rules [private]

Definition at line 52 of file theory_records.h.

Referenced by assertFact(), computeModel(), rewrite(), setup(), TheoryRecords(), and ~TheoryRecords().

The documentation for this class was generated from the following files:
Generated on Thu Oct 15 22:23:11 2009 for CVC3 by  doxygen 1.5.8