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.
