summaryrefslogtreecommitdiff
path: root/src/theory/fp/theory_fp.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/fp/theory_fp.h')
-rw-r--r--src/theory/fp/theory_fp.h36
1 files changed, 36 insertions, 0 deletions
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
new file mode 100644
index 000000000..6fb41685f
--- /dev/null
+++ b/src/theory/fp/theory_fp.h
@@ -0,0 +1,36 @@
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__FP__THEORY_FP_H
+#define __CVC4__THEORY__FP__THEORY_FP_H
+
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace fp {
+
+class TheoryFp : public Theory {
+public:
+
+ /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
+ TheoryFp(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo);
+
+ Node expandDefinition(LogicRequest &, Node node);
+
+ void check(Effort);
+
+ std::string identify() const {
+ return "THEORY_FP";
+ }
+
+};/* class TheoryFp */
+
+}/* CVC4::theory::fp namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__FP__THEORY_FP_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback