CVC3
Modules | Classes
Theories
Validity Checker

Theories. More...

Collaboration diagram for Theories:

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...
 
class  CVC3::TheoryCore::CoreNotifyObj
 
class  CVC3::TheoryCore::CoreSatAPI
 Interface class for callbacks to SAT from Core. More...
 
struct  CVC3::TheoryQuant::multTrigsInfo
 
class  CVC3::TheoryQuant::TypeComp
 
struct  CVC3::TheoryUF::TCMapPair
 

Detailed Description

Theories.