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