diff --git a/include/anthem/AST.h b/include/anthem/AST.h index 3507a2b..1c49ed0 100644 --- a/include/anthem/AST.h +++ b/include/anthem/AST.h @@ -148,7 +148,7 @@ struct FunctionDeclaration std::string name; size_t arity; - Domain domain{Domain::General}; + Domain domain{Domain::Noninteger}; }; //////////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/include/anthem/Arithmetics.h b/include/anthem/Arithmetics.h index ec501d6..0e465b9 100644 --- a/include/anthem/Arithmetics.h +++ b/include/anthem/Arithmetics.h @@ -1,6 +1,7 @@ #ifndef __ANTHEM__ARITHMETICS_H #define __ANTHEM__ARITHMETICS_H +#include #include namespace anthem @@ -59,7 +60,7 @@ struct IsTermArithmeticVisitor { switch (function.declaration->domain) { - case Domain::General: + case Domain::Noninteger: return EvaluationResult::False; case Domain::Integer: return EvaluationResult::True; @@ -127,7 +128,7 @@ struct IsTermArithmeticVisitor switch (domain) { - case Domain::General: + case Domain::Noninteger: return EvaluationResult::False; case Domain::Integer: return EvaluationResult::True; @@ -184,7 +185,7 @@ struct IsTermIntegerVisitor { switch (function.declaration->domain) { - case Domain::General: + case Domain::Noninteger: return EvaluationResult::False; case Domain::Integer: return EvaluationResult::True; @@ -236,7 +237,7 @@ struct IsTermIntegerVisitor { switch (variable.declaration->domain) { - case Domain::General: + case Domain::Noninteger: return EvaluationResult::False; case Domain::Integer: return EvaluationResult::True; diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index 56633ab..0a56c2a 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -45,7 +45,7 @@ enum class OperationResult enum class Domain { - General, + Noninteger, Integer, Unknown, }; diff --git a/include/anthem/output/AST.h b/include/anthem/output/AST.h index 6f6ffd9..15f91c7 100644 --- a/include/anthem/output/AST.h +++ b/include/anthem/output/AST.h @@ -329,8 +329,8 @@ inline output::ColorStream &print(output::ColorStream &stream, const VariableDec { case Domain::Unknown: return ""; - case Domain::General: - return "g"; + case Domain::Noninteger: + return "n"; case Domain::Integer: return "i"; } diff --git a/src/anthem/IntegerVariableDetection.cpp b/src/anthem/IntegerVariableDetection.cpp index 297754e..fcefc33 100644 --- a/src/anthem/IntegerVariableDetection.cpp +++ b/src/anthem/IntegerVariableDetection.cpp @@ -403,7 +403,7 @@ struct CheckIfDefinitionFalseFunctor return OperationResult::Unchanged; // As a hypothesis, make the parameter’s domain noninteger - variableDomainMap[&variableDeclaration] = Domain::General; + variableDomainMap[&variableDeclaration] = Domain::Noninteger; result = evaluate(definition, variableDomainMap); @@ -436,7 +436,7 @@ struct CheckIfQuantifiedFormulaFalseFunctor return OperationResult::Unchanged; // As a hypothesis, make the parameter’s domain noninteger - variableDomainMap[&variableDeclaration] = Domain::General; + variableDomainMap[&variableDeclaration] = Domain::Noninteger; result = evaluate(quantifiedFormula, variableDomainMap); @@ -469,7 +469,7 @@ struct CheckIfCompletedFormulaTrueFunctor return OperationResult::Unchanged; // As a hypothesis, make the parameter’s domain noninteger - variableDomainMap[&variableDeclaration] = Domain::General; + variableDomainMap[&variableDeclaration] = Domain::Noninteger; result = evaluate(completedFormula, variableDomainMap);