How to write a theory in CVC4 (old instructions)

From CVC4
Revision as of 13:23, 30 March 2011 by Lianah (Talk | contribs) (Created page with 'This document is meant as a guide to a theory writer. = CVC4 architecture = A high-level description of the flow of information in CVC4 (TheoryEngine, SMTEngine etc.) = Adding …')

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

This document is meant as a guide to a theory writer.

CVC4 architecture

A high-level description of the flow of information in CVC4 (TheoryEngine, SMTEngine etc.)

Adding a new theory

parser

todo

config and make

todo

types and kinds

todo

Theory API & Invariants

methods implemented in a subclass

methods in the API

Useful tools

context dependent structures

Nodes and TNodes

Attributes

Statistics