Implemented simplification of nested quantified expressions.
This commit is contained in:
@@ -178,7 +178,7 @@ inline ExpressionPointer NAry<Derived>::simplified()
|
||||
}
|
||||
|
||||
// TODO: recognize tautologies
|
||||
// TODO: introduce handle boolean values
|
||||
// TODO: introduce/handle boolean values
|
||||
|
||||
return this;
|
||||
}
|
||||
|
@@ -31,8 +31,12 @@ class Quantified: public ExpressionCRTP<Derived>
|
||||
void setArgument(ExpressionPointer argument);
|
||||
ExpressionPointer argument() const;
|
||||
|
||||
Variables &variables();
|
||||
const Variables &variables() const;
|
||||
|
||||
ExpressionPointer reduced() override;
|
||||
ExpressionPointer negationNormalized() override;
|
||||
ExpressionPointer simplified() override;
|
||||
|
||||
void print(std::ostream &ostream) const override;
|
||||
|
||||
@@ -98,6 +102,22 @@ ExpressionPointer Quantified<Derived>::argument() const
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
Variables &Quantified<Derived>::variables()
|
||||
{
|
||||
return m_variables;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
const Variables &Quantified<Derived>::variables() const
|
||||
{
|
||||
return m_variables;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline ExpressionPointer Quantified<Derived>::reduced()
|
||||
{
|
||||
@@ -118,17 +138,43 @@ inline ExpressionPointer Quantified<Derived>::negationNormalized()
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline ExpressionPointer Quantified<Derived>::simplified()
|
||||
{
|
||||
m_argument = m_argument->simplified();
|
||||
|
||||
// Associate same-type children, such as (forall (?x) (forall (?y) (...)))
|
||||
if (m_argument->expressionType() != Derived::ExpressionType)
|
||||
return this;
|
||||
|
||||
auto &quantifiedExpression = dynamic_cast<Derived &>(*m_argument);
|
||||
|
||||
BOOST_ASSERT(!quantifiedExpression.arguments().empty());
|
||||
|
||||
// Unify variables
|
||||
m_variables.insert(m_variables.end(), quantifiedExpression.variables().begin(), quantifiedExpression.variables().end());
|
||||
|
||||
// Move child expression up
|
||||
m_argument = quantifiedExpression.argument();
|
||||
|
||||
// TODO: introduce/handle boolean values
|
||||
|
||||
return this;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||
|
||||
template<class Derived>
|
||||
inline void Quantified<Derived>::print(std::ostream &ostream) const
|
||||
{
|
||||
ostream << "(" << Derived::Identifier << "(";
|
||||
ostream << "(" << Derived::Identifier << " (";
|
||||
|
||||
for (size_t i = 0; i < m_variables.size(); i++)
|
||||
{
|
||||
if (i > 0)
|
||||
ostream << " ";
|
||||
|
||||
ostream << m_variables[i]->name();
|
||||
m_variables[i]->print(ostream);
|
||||
}
|
||||
|
||||
ostream << ") ";
|
||||
|
@@ -27,6 +27,9 @@ class Variable: public ExpressionCRTP<Variable>
|
||||
Variables &variables);
|
||||
|
||||
public:
|
||||
Variable();
|
||||
Variable(std::string name);
|
||||
|
||||
void setName(std::string name);
|
||||
const std::string &name() const;
|
||||
|
||||
@@ -42,8 +45,6 @@ class Variable: public ExpressionCRTP<Variable>
|
||||
static void parseDeclaration(Context &context, Variables ¶meters);
|
||||
|
||||
private:
|
||||
Variable();
|
||||
|
||||
bool m_isDirty;
|
||||
|
||||
std::string m_name;
|
||||
|
Reference in New Issue
Block a user