Added initial abstract syntax tree for first-order logic formulas.

This commit is contained in:
Patrick Lühne 2017-03-08 01:21:03 +01:00
parent afe49dce6c
commit f139e375f1
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 248 additions and 0 deletions

151
include/anthem/AST.h Normal file
View File

@ -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

View File

@ -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