summaryrefslogtreecommitdiff
path: root/src/include/prover.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2009-11-03 03:37:08 +0000
committerMorgan Deters <mdeters@gmail.com>2009-11-03 03:37:08 +0000
commit842e581321bcd9f30c60b9dacc671843ca776fed (patch)
tree202ddf8dae7e090e06d5aed869337ef9162309cd /src/include/prover.h
parent541379b3d361e255cd664207f8b2e278a5b5e3eb (diff)
additional headers and modifications; now passes syntax check
Diffstat (limited to 'src/include/prover.h')
-rw-r--r--src/include/prover.h5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/include/prover.h b/src/include/prover.h
index 7abfafe63..e48d6336c 100644
--- a/src/include/prover.h
+++ b/src/include/prover.h
@@ -10,6 +10,11 @@
#ifndef __CVC4_PROVER_H
#define __CVC4_PROVER_H
+#include <vector>
+#include "expr.h"
+#include "result.h"
+#include "model.h"
+
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
// PropEngine.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback