CVC3
2.4.1
|
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... | |
Theories.