CVC3  2.4.1
Modules | Classes
Theories
Validity Checker

Theories. More...

Modules

 Abstract Theory Interface
 Abstract Theory Interface.

Classes

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.