Move Domain class to Utils header
This commit is contained in:
parent
529aec15af
commit
2b62c6227d
@ -2,7 +2,7 @@
|
|||||||
#define __ANTHEM__AST_H
|
#define __ANTHEM__AST_H
|
||||||
|
|
||||||
#include <anthem/ASTForward.h>
|
#include <anthem/ASTForward.h>
|
||||||
#include <anthem/Domain.h>
|
#include <anthem/Utils.h>
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
@ -14,7 +14,7 @@ namespace anthem
|
|||||||
|
|
||||||
struct DefaultVariableDomainAccessor
|
struct DefaultVariableDomainAccessor
|
||||||
{
|
{
|
||||||
ast::Domain operator()(const ast::Variable &variable)
|
Domain operator()(const ast::Variable &variable)
|
||||||
{
|
{
|
||||||
return variable.declaration->domain;
|
return variable.declaration->domain;
|
||||||
}
|
}
|
||||||
@ -59,11 +59,11 @@ struct IsTermArithmeticVisitor
|
|||||||
{
|
{
|
||||||
switch (function.declaration->domain)
|
switch (function.declaration->domain)
|
||||||
{
|
{
|
||||||
case ast::Domain::General:
|
case Domain::General:
|
||||||
return EvaluationResult::False;
|
return EvaluationResult::False;
|
||||||
case ast::Domain::Integer:
|
case Domain::Integer:
|
||||||
return EvaluationResult::True;
|
return EvaluationResult::True;
|
||||||
case ast::Domain::Unknown:
|
case Domain::Unknown:
|
||||||
return EvaluationResult::Unknown;
|
return EvaluationResult::Unknown;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -127,11 +127,11 @@ struct IsTermArithmeticVisitor
|
|||||||
|
|
||||||
switch (domain)
|
switch (domain)
|
||||||
{
|
{
|
||||||
case ast::Domain::General:
|
case Domain::General:
|
||||||
return EvaluationResult::False;
|
return EvaluationResult::False;
|
||||||
case ast::Domain::Integer:
|
case Domain::Integer:
|
||||||
return EvaluationResult::True;
|
return EvaluationResult::True;
|
||||||
case ast::Domain::Unknown:
|
case Domain::Unknown:
|
||||||
return EvaluationResult::Unknown;
|
return EvaluationResult::Unknown;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -184,11 +184,11 @@ struct IsTermIntegerVisitor
|
|||||||
{
|
{
|
||||||
switch (function.declaration->domain)
|
switch (function.declaration->domain)
|
||||||
{
|
{
|
||||||
case ast::Domain::General:
|
case Domain::General:
|
||||||
return EvaluationResult::False;
|
return EvaluationResult::False;
|
||||||
case ast::Domain::Integer:
|
case Domain::Integer:
|
||||||
return EvaluationResult::True;
|
return EvaluationResult::True;
|
||||||
case ast::Domain::Unknown:
|
case Domain::Unknown:
|
||||||
return EvaluationResult::Unknown;
|
return EvaluationResult::Unknown;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -236,11 +236,11 @@ struct IsTermIntegerVisitor
|
|||||||
{
|
{
|
||||||
switch (variable.declaration->domain)
|
switch (variable.declaration->domain)
|
||||||
{
|
{
|
||||||
case ast::Domain::General:
|
case Domain::General:
|
||||||
return EvaluationResult::False;
|
return EvaluationResult::False;
|
||||||
case ast::Domain::Integer:
|
case Domain::Integer:
|
||||||
return EvaluationResult::True;
|
return EvaluationResult::True;
|
||||||
case ast::Domain::Unknown:
|
case Domain::Unknown:
|
||||||
return EvaluationResult::Unknown;
|
return EvaluationResult::Unknown;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,27 +0,0 @@
|
|||||||
#ifndef __ANTHEM__DOMAIN_H
|
|
||||||
#define __ANTHEM__DOMAIN_H
|
|
||||||
|
|
||||||
namespace anthem
|
|
||||||
{
|
|
||||||
namespace ast
|
|
||||||
{
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
//
|
|
||||||
// Domain
|
|
||||||
//
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
enum class Domain
|
|
||||||
{
|
|
||||||
General,
|
|
||||||
Integer,
|
|
||||||
Unknown,
|
|
||||||
};
|
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
||||||
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif
|
|
@ -237,7 +237,7 @@ struct StatementVisitor
|
|||||||
const size_t arity = aritySymbol.number();
|
const size_t arity = aritySymbol.number();
|
||||||
|
|
||||||
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
|
auto functionDeclaration = context.findOrCreateFunctionDeclaration(function.name, arity);
|
||||||
functionDeclaration->domain = ast::Domain::Integer;
|
functionDeclaration->domain = Domain::Integer;
|
||||||
|
|
||||||
return true;
|
return true;
|
||||||
};
|
};
|
||||||
|
@ -1,13 +1,6 @@
|
|||||||
#ifndef __ANTHEM__UTILS_H
|
#ifndef __ANTHEM__UTILS_H
|
||||||
#define __ANTHEM__UTILS_H
|
#define __ANTHEM__UTILS_H
|
||||||
|
|
||||||
#include <iostream>
|
|
||||||
|
|
||||||
#include <clingo.hh>
|
|
||||||
|
|
||||||
#include <anthem/Context.h>
|
|
||||||
#include <anthem/Location.h>
|
|
||||||
|
|
||||||
namespace anthem
|
namespace anthem
|
||||||
{
|
{
|
||||||
|
|
||||||
@ -50,6 +43,15 @@ enum class OperationResult
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
enum class Domain
|
||||||
|
{
|
||||||
|
General,
|
||||||
|
Integer,
|
||||||
|
Unknown,
|
||||||
|
};
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
@ -18,19 +18,19 @@ namespace anthem
|
|||||||
//
|
//
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
using VariableDomainMap = std::map<const ast::VariableDeclaration *, ast::Domain>;
|
using VariableDomainMap = std::map<const ast::VariableDeclaration *, Domain>;
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
||||||
{
|
{
|
||||||
if (variable.declaration->domain != ast::Domain::Unknown)
|
if (variable.declaration->domain != Domain::Unknown)
|
||||||
return variable.declaration->domain;
|
return variable.declaration->domain;
|
||||||
|
|
||||||
const auto match = variableDomainMap.find(variable.declaration);
|
const auto match = variableDomainMap.find(variable.declaration);
|
||||||
|
|
||||||
if (match == variableDomainMap.end())
|
if (match == variableDomainMap.end())
|
||||||
return ast::Domain::Unknown;
|
return Domain::Unknown;
|
||||||
|
|
||||||
return match->second;
|
return match->second;
|
||||||
}
|
}
|
||||||
@ -40,14 +40,14 @@ ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDom
|
|||||||
void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
|
void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
|
||||||
{
|
{
|
||||||
for (auto &variableDeclaration : variableDomainMap)
|
for (auto &variableDeclaration : variableDomainMap)
|
||||||
variableDeclaration.second = ast::Domain::Unknown;
|
variableDeclaration.second = Domain::Unknown;
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
struct VariableDomainMapAccessor
|
struct VariableDomainMapAccessor
|
||||||
{
|
{
|
||||||
ast::Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
|
||||||
{
|
{
|
||||||
return domain(variable, variableDomainMap);
|
return domain(variable, variableDomainMap);
|
||||||
}
|
}
|
||||||
@ -247,7 +247,7 @@ struct EvaluateFormulaVisitor
|
|||||||
const auto &argument = predicate.arguments[i];
|
const auto &argument = predicate.arguments[i];
|
||||||
const auto ¶meter = predicate.declaration->parameters[i];
|
const auto ¶meter = predicate.declaration->parameters[i];
|
||||||
|
|
||||||
if (parameter.domain != ast::Domain::Integer)
|
if (parameter.domain != Domain::Integer)
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
|
const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
|
||||||
@ -392,7 +392,7 @@ struct CheckIfDefinitionFalseFunctor
|
|||||||
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
|
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
|
||||||
ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
|
||||||
{
|
{
|
||||||
if (variableDeclaration.domain != ast::Domain::Unknown)
|
if (variableDeclaration.domain != Domain::Unknown)
|
||||||
return OperationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
clearVariableDomainMap(variableDomainMap);
|
clearVariableDomainMap(variableDomainMap);
|
||||||
@ -403,14 +403,14 @@ struct CheckIfDefinitionFalseFunctor
|
|||||||
return OperationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
// As a hypothesis, make the parameter’s domain noninteger
|
// As a hypothesis, make the parameter’s domain noninteger
|
||||||
variableDomainMap[&variableDeclaration] = ast::Domain::General;
|
variableDomainMap[&variableDeclaration] = Domain::General;
|
||||||
|
|
||||||
result = evaluate(definition, variableDomainMap);
|
result = evaluate(definition, variableDomainMap);
|
||||||
|
|
||||||
if (result == EvaluationResult::Error || result == EvaluationResult::False)
|
if (result == EvaluationResult::Error || result == EvaluationResult::False)
|
||||||
{
|
{
|
||||||
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
||||||
variableDeclaration.domain = ast::Domain::Integer;
|
variableDeclaration.domain = Domain::Integer;
|
||||||
return OperationResult::Changed;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -425,7 +425,7 @@ struct CheckIfQuantifiedFormulaFalseFunctor
|
|||||||
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
|
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
|
||||||
ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
|
ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
|
||||||
{
|
{
|
||||||
if (variableDeclaration.domain != ast::Domain::Unknown)
|
if (variableDeclaration.domain != Domain::Unknown)
|
||||||
return OperationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
clearVariableDomainMap(variableDomainMap);
|
clearVariableDomainMap(variableDomainMap);
|
||||||
@ -436,14 +436,14 @@ struct CheckIfQuantifiedFormulaFalseFunctor
|
|||||||
return OperationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
// As a hypothesis, make the parameter’s domain noninteger
|
// As a hypothesis, make the parameter’s domain noninteger
|
||||||
variableDomainMap[&variableDeclaration] = ast::Domain::General;
|
variableDomainMap[&variableDeclaration] = Domain::General;
|
||||||
|
|
||||||
result = evaluate(quantifiedFormula, variableDomainMap);
|
result = evaluate(quantifiedFormula, variableDomainMap);
|
||||||
|
|
||||||
if (result == EvaluationResult::Error || result == EvaluationResult::False)
|
if (result == EvaluationResult::Error || result == EvaluationResult::False)
|
||||||
{
|
{
|
||||||
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
||||||
variableDeclaration.domain = ast::Domain::Integer;
|
variableDeclaration.domain = Domain::Integer;
|
||||||
return OperationResult::Changed;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -458,7 +458,7 @@ struct CheckIfCompletedFormulaTrueFunctor
|
|||||||
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
|
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
|
||||||
ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
|
ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
|
||||||
{
|
{
|
||||||
if (variableDeclaration.domain != ast::Domain::Unknown)
|
if (variableDeclaration.domain != Domain::Unknown)
|
||||||
return OperationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
clearVariableDomainMap(variableDomainMap);
|
clearVariableDomainMap(variableDomainMap);
|
||||||
@ -469,14 +469,14 @@ struct CheckIfCompletedFormulaTrueFunctor
|
|||||||
return OperationResult::Unchanged;
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
// As a hypothesis, make the parameter’s domain noninteger
|
// As a hypothesis, make the parameter’s domain noninteger
|
||||||
variableDomainMap[&variableDeclaration] = ast::Domain::General;
|
variableDomainMap[&variableDeclaration] = Domain::General;
|
||||||
|
|
||||||
result = evaluate(completedFormula, variableDomainMap);
|
result = evaluate(completedFormula, variableDomainMap);
|
||||||
|
|
||||||
if (result == EvaluationResult::Error || result == EvaluationResult::True)
|
if (result == EvaluationResult::Error || result == EvaluationResult::True)
|
||||||
{
|
{
|
||||||
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
|
||||||
variableDeclaration.domain = ast::Domain::Integer;
|
variableDeclaration.domain = Domain::Integer;
|
||||||
return OperationResult::Changed;
|
return OperationResult::Changed;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -147,7 +147,7 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
|||||||
{
|
{
|
||||||
auto ¶meter = predicateDeclaration->parameters[i];
|
auto ¶meter = predicateDeclaration->parameters[i];
|
||||||
|
|
||||||
if (parameter.domain != ast::Domain::Integer)
|
if (parameter.domain != Domain::Integer)
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
context.logger.outputStream()
|
context.logger.outputStream()
|
||||||
|
Loading…
x
Reference in New Issue
Block a user