diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 16:40:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 16:40:19 +0000 |
commit | 0201aa29bea8467e5cc07f2d0af68a4da3e86ec1 (patch) | |
tree | 548f42c4244176fb91956e9571451842fd85e482 /src/include/cvc4.h | |
parent | 7293554b109742697d4d928ed7b58acadc6de947 (diff) |
fixes/redesign of source layout from meeting
Diffstat (limited to 'src/include/cvc4.h')
-rw-r--r-- | src/include/cvc4.h | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/include/cvc4.h b/src/include/cvc4.h new file mode 100644 index 000000000..109496001 --- /dev/null +++ b/src/include/cvc4.h @@ -0,0 +1,42 @@ +/********************* -*- C++ -*- */ +/** vc.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + **/ + +#ifndef __CVC4_VC_H +#define __CVC4_VC_H + +#include "command.h" +#include "cvc4_expr.h" + +/* 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 */ + +#endif /* __CVC4_VC_H */ |