Theories
[Validity Checker]

Collaboration diagram for Theories:

Theories. More...

Modules

• Abstract Theory Interface

  Abstract Theory Interface.
  

Classes

• class CVC3::Theory

  Base class for theories. More...
  

• class CVC3::Theory

  Base class for theories. More...
  

• class CVC3::TheoryArith

  This theory handles basic linear arithmetic. More...
  

• class CVC3::TheoryArray

  This theory handles arrays. More...
  

• class CVC3::TheoryBitvector

  Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG). More...
  

• class CVC3::TheoryCore

  This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories. More...
  

• class CVC3::TheoryDatatype

  This theory handles datatypes. More...
  

• class CVC3::TheoryDatatypeLazy

  This theory handles datatypes. More...
  

• class CVC3::TheoryQuant

  This theory handles quantifiers. More...
  

• class CVC3::TheoryRecords

  This theory handles records. More...
  

• class CVC3::TheorySimulate

  "Theory" of symbolic simulation. More...
  

• class CVC3::TheoryUF

  This theory handles uninterpreted functions. More...
  

---

Detailed Description

Theories.

---