Implemented disjunctive normal form.

This commit is contained in:
2016-09-08 03:42:32 +02:00
parent 34496a7158
commit 4fc9b35c13
12 changed files with 273 additions and 1 deletions

View File

@@ -120,11 +120,14 @@ class Expression
virtual Type expressionType() const = 0;
virtual ExpressionPointer copy();
ExpressionPointer normalized();
virtual ExpressionPointer reduced();
virtual ExpressionPointer negationNormalized();
virtual ExpressionPointer prenex(Expression::Type lastQuantifierType = Expression::Type::Exists);
virtual ExpressionPointer simplified();
virtual ExpressionPointer disjunctionNormalized();
ExpressionPointer negated();
virtual void print(std::ostream &ostream) const = 0;

View File

@@ -22,6 +22,9 @@ class And: public NAry<And>
static const Expression::Type ExpressionType = Expression::Type::And;
static const std::string Identifier;
public:
ExpressionPointer disjunctionNormalized() override;
};
////////////////////////////////////////////////////////////////////////////////////////////////////

View File

@@ -32,6 +32,8 @@ class At: public ExpressionCRTP<At>
public:
At();
ExpressionPointer copy() override;
size_t timePoint() const;
void setArgument(ExpressionPointer argument);
@@ -41,6 +43,7 @@ class At: public ExpressionCRTP<At>
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex(Expression::Type lastExpressionType) override;
ExpressionPointer simplified() override;
ExpressionPointer disjunctionNormalized() override;
void print(std::ostream &ostream) const override;

View File

@@ -29,12 +29,16 @@ class Binary: public ExpressionCRTP<Derived>
ExpressionContext &expressionContext, ExpressionParser parseExpression);
public:
ExpressionPointer copy() override;
void setArgument(size_t i, ExpressionPointer argument);
const std::array<ExpressionPointer, 2> &arguments() const;
ExpressionPointer reduced() override;
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex(Expression::Type lastExpressionType) override;
ExpressionPointer simplified() override;
ExpressionPointer disjunctionNormalized() override;
void print(std::ostream &ostream) const override;
@@ -73,6 +77,19 @@ boost::intrusive_ptr<Derived> Binary<Derived>::parse(Context &context,
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
ExpressionPointer Binary<Derived>::copy()
{
auto result = new Derived;
for (size_t i = 0; i < m_arguments.size(); i++)
result->m_arguments[i] = m_arguments[i]->copy();
return result;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
void Binary<Derived>::setArgument(size_t i, ExpressionPointer expression)
{
@@ -130,6 +147,36 @@ inline ExpressionPointer Binary<Derived>::prenex(Expression::Type)
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer Binary<Derived>::simplified()
{
for (size_t i = 0; i < m_arguments.size(); i++)
{
BOOST_ASSERT(m_arguments[i]);
m_arguments[i] = m_arguments[i]->simplified();
}
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer Binary<Derived>::disjunctionNormalized()
{
for (size_t i = 0; i < m_arguments.size(); i++)
{
BOOST_ASSERT(m_arguments[i]);
m_arguments[i] = m_arguments[i]->disjunctionNormalized();
}
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline void Binary<Derived>::print(std::ostream &ostream) const
{

View File

@@ -29,6 +29,8 @@ class NAry: public ExpressionCRTP<Derived>
ExpressionContext &expressionContext, ExpressionParser parseExpression);
public:
ExpressionPointer copy() override;
void setArgument(size_t i, ExpressionPointer argument);
void addArgument(ExpressionPointer argument);
Expressions &arguments();
@@ -38,6 +40,7 @@ class NAry: public ExpressionCRTP<Derived>
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex(Expression::Type lastExpressionType) override;
ExpressionPointer simplified() override;
ExpressionPointer disjunctionNormalized() override;
void print(std::ostream &ostream) const override;
@@ -85,6 +88,21 @@ boost::intrusive_ptr<Derived> NAry<Derived>::parse(Context &context,
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
ExpressionPointer NAry<Derived>::copy()
{
auto result = new Derived;
result->m_arguments.resize(m_arguments.size());
for (size_t i = 0; i < m_arguments.size(); i++)
result->m_arguments[i] = m_arguments[i]->copy();
return result;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
void NAry<Derived>::setArgument(size_t i, ExpressionPointer expression)
{
@@ -273,6 +291,21 @@ inline ExpressionPointer NAry<Derived>::simplified()
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer NAry<Derived>::disjunctionNormalized()
{
for (size_t i = 0; i < m_arguments.size(); i++)
{
BOOST_ASSERT(m_arguments[i]);
m_arguments[i] = m_arguments[i]->disjunctionNormalized();
}
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline void NAry<Derived>::print(std::ostream &ostream) const
{

View File

@@ -29,6 +29,8 @@ class Not: public ExpressionCRTP<Not>
public:
Not();
ExpressionPointer copy() override;
void setArgument(ExpressionPointer argument);
ExpressionPointer argument() const;
@@ -36,6 +38,7 @@ class Not: public ExpressionCRTP<Not>
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex(Expression::Type lastExpressionType) override;
ExpressionPointer simplified() override;
ExpressionPointer disjunctionNormalized() override;
void print(std::ostream &ostream) const override;

View File

@@ -49,10 +49,13 @@ class QuantifiedCRTP: public Quantified
return Derived::ExpressionType;
}
ExpressionPointer copy() override;
ExpressionPointer reduced() override;
ExpressionPointer negationNormalized() override;
ExpressionPointer prenex(Expression::Type lastExpressionType) override;
ExpressionPointer simplified() override;
ExpressionPointer disjunctionNormalized() override;
void print(std::ostream &ostream) const override;
};
@@ -98,6 +101,18 @@ boost::intrusive_ptr<Derived> QuantifiedCRTP<Derived>::parse(Context &context,
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
ExpressionPointer QuantifiedCRTP<Derived>::copy()
{
auto result = new Derived;
result->m_argument = m_argument->copy();
return result;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
inline void Quantified::setArgument(ExpressionPointer expression)
{
m_argument = expression;
@@ -190,6 +205,18 @@ inline ExpressionPointer QuantifiedCRTP<Derived>::simplified()
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline ExpressionPointer QuantifiedCRTP<Derived>::disjunctionNormalized()
{
BOOST_ASSERT(m_argument);
m_argument = m_argument->disjunctionNormalized();
return this;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
template<class Derived>
inline void QuantifiedCRTP<Derived>::print(std::ostream &ostream) const
{