diff options
Diffstat (limited to 'src/include/vc.h')
-rw-r--r-- | src/include/vc.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/include/vc.h b/src/include/vc.h index d4b293a28..a75aa0548 100644 --- a/src/include/vc.h +++ b/src/include/vc.h @@ -13,11 +13,23 @@ /* TODO provide way of querying whether you fall into a fragment / * returning what fragment you're in */ +// In terms of abstraction, this is below (and provides services to) +// users using the library interface, and also the parser for the main +// CVC4 binary. It is above (and requires the services of) the Prover +// class. + namespace CVC4 { +/** + * User-visible (library) interface to CVC4. + */ class ValidityChecker { + // on entry to the validity checker interface, need to set up + // current state (ExprManager::d_current etc.) public: void doCommand(Command); + + void query(Expr); }; } /* CVC4 namespace */ |