CVC3: Theories

Theories. More...

Collaboration diagram for Theories:

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...

Theories.