CVC3::TheoryRecords Class Reference
[Theories]

This theory handles records. More...

#include <theory_records.h>

Inheritance diagram for CVC3::TheoryRecords:

[legend]Collaboration diagram for CVC3::TheoryRecords:

[legend]List of all members.

Public Member Functions

• TheoryRecords (TheoryCore *core)

  Constructor.
  

• ~TheoryRecords ()
• RecordsProofRules * createProofRules ()

  creates a reference to the proof rules
  

• void assertFact (const Theorem &e)

  assert a fact to the theory of records
  

• void checkSat (bool fullEffort)

  empty implementation to fit theory interface
  

• Theorem rewrite (const Expr &e)

  rewrites an expression e to one of several allowed forms
  

• void checkType (const Expr &e)

  check record or tuple type
  

• void computeType (const Expr &e)

  computes the type of a record or a tuple
  

• Type computeBaseType (const Type &t)

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

• Expr computeTypePred (const Type &t, const Expr &e)

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

• void computeModelTerm (const Expr &e, std::vector< Expr > &v)

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

• void computeModel (const Expr &e, std::vector< Expr > &vars)

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

• Expr computeTCC (const Expr &e)

  Compute and cache the TCC of e.
  

• virtual Expr parseExprOp (const Expr &e)

  Theory-specific parsing implemented by the DP.
  

• void setup (const Expr &e)

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

• void update (const Theorem &e, const Expr &d)

  Notify a theory of a new equality.
  

• ExprStream & print (ExprStream &os, const Expr &e)

  pretty printing
  

• bool isRecord (const Expr &e)

  Test whether expr is a record literal.
  

• bool isRecordType (const Expr &e)

  Test whether expr is a record type.
  

• bool isRecordType (const Type &t)

  Test whether expr is a record type.
  

• bool isRecordAccess (const Expr &e)

  Test whether expr is a record select/update subclass.
  

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

  Create a record literal.
  

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

  Create a record literal.
  

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

  Create a record type.
  

• Type 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).
  

• Type 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).
  

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

  Create a record field select expression.
  

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

  Create a record field update expression.
  

• const std::vector< Expr > & getFields (const Expr &r)

  Get the list of fields from a record literal.
  

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

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

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

  Get the field index in the record literal or type.
  

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

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

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

  Create a tuple literal.
  

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

  Create a tuple type.
  

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

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

• Expr tupleSelect (const Expr &tup, int i)

  Create a tuple index selector expression.
  

• Expr tupleUpdate (const Expr &tup, int i, const Expr &val)

  Create a tuple index update expression.
  

• int getIndex (const Expr &e)

  Get the index from the tuple select and update expressions.
  

• bool isTupleAccess (const Expr &e)

  Test whether expr is a tuple select/update subclass.
  

• bool isTuple (const Expr &e)

  Test if expr is a tuple literal.
  

• bool isTupleType (const Expr &e)

  Test if expr represents a tuple type.
  

• bool isTupleType (const Type &tp)

  Test if 'tp' is a tuple type.
  

Private Member Functions

• Theorem rewriteAux (const Expr &e)

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

• Theorem rewriteAux (const Theorem &thm)

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

Private Attributes

• RecordsProofRules * d_rules

---

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 95 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 124 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 44 of file theory_records.cpp.

References CVC3::AND, CVC3::Expr::arity(), CVC3::EQ, CVC3::Expr::getFind(), CVC3::Expr::getKind(), 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 90 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 128 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 160 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 343 of file theory_records.cpp.

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

void TheoryRecords::computeType

(

const Expr &

e

)

[virtual]

computes the type of a record or a tuple

Reimplemented from CVC3::Theory.

Definition at line 379 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 &

t

)

[virtual]

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

Reimplemented from CVC3::Theory.

Definition at line 475 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 311 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 260 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 280 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::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 227 of file theory_records.cpp.

References CVC3::Theory::computeTCC(), DebugAssert, getField(), getFieldIndex(), getIndex(), 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 870 of file theory_records.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::ID, CVC3::Theory::parseExpr(), CVC3::RAW_LIST, CVC3::RECORD, CVC3::RECORD_SELECT, CVC3::RECORD_TYPE, CVC3::RECORD_UPDATE, recordExpr(), recordSelect(), recordType(), recordUpdate(), 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 499 of file theory_records.cpp.

References d_rules, CVC3::Theory::enqueueFact(), CVC3::RecordsProofRules::expandRecord(), CVC3::RecordsProofRules::expandTuple(), CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Theorem::isNull(), isRecordType(), CVC3::Expr::isTerm(), isTupleType(), CVC3::RECORD, rewrite(), CVC3::Theory::setupCC(), CVC3::Theory::substitutivityRule(), CVC3::Theory::symmetryRule(), 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 552 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 575 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 89 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 93 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 97 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 101 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 951 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 960 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 967 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).

Definition at line 978 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 987 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.

Definition at line 994 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 1000 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 1007 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 1017 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 1027 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 1039 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 1048 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 1054 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).

Definition at line 1064 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 1070 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 1076 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 1082 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 145 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 149 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 151 of file theory_records.h.

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

Referenced by isTupleType(), and setup().

bool CVC3::TheoryRecords::isTupleType

(

const Type &

tp

)

[inline]

Test if 'tp' is a tuple type.

Definition at line 154 of file theory_records.h.

References CVC3::Type::getExpr(), and 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:

• theory_records.h
• records_theorem_producer.cpp
• theory_records.cpp

---