From f139e375f191a8f87d5418e29039c25048aa76cb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Wed, 8 Mar 2017 01:21:03 +0100
Subject: [PATCH] Added initial abstract syntax tree for first-order logic
 formulas.

---
 include/anthem/AST.h        | 151 ++++++++++++++++++++++++++++++++++++
 include/anthem/ASTForward.h |  97 +++++++++++++++++++++++
 2 files changed, 248 insertions(+)
 create mode 100644 include/anthem/AST.h
 create mode 100644 include/anthem/ASTForward.h

diff --git a/include/anthem/AST.h b/include/anthem/AST.h
new file mode 100644
index 0000000..5463bb4
--- /dev/null
+++ b/include/anthem/AST.h
@@ -0,0 +1,151 @@
+#ifndef __ANTHEM__AST_H
+#define __ANTHEM__AST_H
+
+#include <anthem/ASTForward.h>
+
+namespace anthem
+{
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// AST
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Primitives
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct BinaryOperation
+{
+	enum class Operator
+	{
+		Add,
+		Subtract
+	};
+
+	Operator operator_;
+	Term left;
+	Term right;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Boolean
+{
+	bool value = false;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Equals
+{
+	Term left;
+	Term right;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Function
+{
+	const char *name = nullptr;
+	std::vector<Term> arguments;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Integer
+{
+	int value;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct IntegerRange
+{
+	Integer from;
+	Integer to;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Predicate
+{
+	const char *name = nullptr;
+	std::vector<Term> arguments;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Variable
+{
+	const char *name = nullptr;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Expressions
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct And
+{
+	std::vector<Formula> arguments;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Biconditional
+{
+	Formula left;
+	Formula right;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Exists
+{
+	std::vector<VariablePointer> variables;
+	Formula formula;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct ForAll
+{
+	std::vector<VariablePointer> variables;
+	Formula formula;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Implies
+{
+	Formula antecedent;
+	Formula consequent;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Not
+{
+	Formula argument;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct Or
+{
+	std::vector<Formula> arguments;
+};
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
+
+#endif
diff --git a/include/anthem/ASTForward.h b/include/anthem/ASTForward.h
new file mode 100644
index 0000000..4c9f3c2
--- /dev/null
+++ b/include/anthem/ASTForward.h
@@ -0,0 +1,97 @@
+#ifndef __ANTHEM__AST_FORWARD_H
+#define __ANTHEM__AST_FORWARD_H
+
+#include <memory>
+#include <experimental/optional>
+#include <mapbox/variant.hpp>
+#include <vector>
+
+namespace anthem
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+//
+// AST Forward Declarations
+//
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+namespace ast
+{
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+struct And;
+struct BinaryOperation;
+struct Biconditional;
+struct Boolean;
+struct Constant;
+struct Equals;
+struct Exists;
+struct ForAll;
+struct Function;
+struct Implies;
+struct Integer;
+struct IntegerRange;
+struct Not;
+struct Or;
+struct Predicate;
+struct Variable;
+
+using AndPointer = std::unique_ptr<And>;
+using BinaryOperationPointer = std::unique_ptr<BinaryOperation>;
+using BiconditionalPointer = std::unique_ptr<Biconditional>;
+using BooleanPointer = std::unique_ptr<Boolean>;
+using ConstantPointer = std::unique_ptr<Constant>;
+using EqualsPointer = std::unique_ptr<Equals>;
+using ExistsPointer = std::unique_ptr<Exists>;
+using ForAllPointer = std::unique_ptr<ForAll>;
+using FunctionPointer = std::unique_ptr<Function>;
+using ImpliesPointer = std::unique_ptr<Implies>;
+using IntegerPointer = std::unique_ptr<Integer>;
+using IntegerRangePointer = std::unique_ptr<IntegerRange>;
+using NotPointer = std::unique_ptr<Not>;
+using OrPointer = std::unique_ptr<Or>;
+using PredicatePointer = std::unique_ptr<Predicate>;
+using VariablePointer = std::unique_ptr<Variable>;
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+// Variants
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+using TermT = mapbox::util::variant<
+	BinaryOperationPointer,
+	ConstantPointer,
+	IntegerPointer,
+	FunctionPointer,
+	VariablePointer>;
+
+class Term : public TermT
+{
+	using TermT::TermT;
+};
+
+using FormulaT = mapbox::util::variant<
+	AndPointer,
+	BiconditionalPointer,
+	BooleanPointer,
+	EqualsPointer,
+	ExistsPointer,
+	ForAllPointer,
+	ImpliesPointer,
+	NotPointer,
+	OrPointer,
+	PredicatePointer>;
+
+class Formula : public FormulaT
+{
+	using FormulaT::FormulaT;
+};
+
+using Formulas = std::vector<Formula>;
+
+////////////////////////////////////////////////////////////////////////////////////////////////////
+
+}
+}
+
+#endif