From 63f39e5162e6a9c77e7f9d502910cd8f7dc87664 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Patrick=20L=C3=BChne?= Date: Sun, 29 Apr 2018 21:27:31 +0200 Subject: [PATCH] Provide function for evaluating formulas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This provides a new function that can be used to evaluate formulas under partial knowledge about the individual variables’ assignments. This will be useful for testing whether formulas or subformulas become trivial under specific interpretations. --- include/anthem/ASTUtils.h | 15 +++ include/anthem/Evaluation.h | 244 ++++++++++++++++++++++++++++++++++++ include/anthem/Type.h | 11 +- include/anthem/Utils.h | 10 ++ 4 files changed, 270 insertions(+), 10 deletions(-) create mode 100644 include/anthem/Evaluation.h diff --git a/include/anthem/ASTUtils.h b/include/anthem/ASTUtils.h index 75d6623..3e407ef 100644 --- a/include/anthem/ASTUtils.h +++ b/include/anthem/ASTUtils.h @@ -90,6 +90,21 @@ struct ReplaceVariableInFormulaVisitor : public RecursiveFormulaVisitordomain; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + } #endif diff --git a/include/anthem/Evaluation.h b/include/anthem/Evaluation.h new file mode 100644 index 0000000..bbc24c1 --- /dev/null +++ b/include/anthem/Evaluation.h @@ -0,0 +1,244 @@ +#ifndef __ANTHEM__EVALUATION_H +#define __ANTHEM__EVALUATION_H + +#include +#include +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Evaluation +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +struct EvaluateFormulaVisitor +{ + template + static EvaluationResult visit(const ast::And &and_, Arguments &&... arguments) + { + bool someFalse = false; + bool someUnknown = false; + + for (const auto &argument : and_.arguments) + { + const auto result = evaluate(argument, std::forward(arguments)...); + + switch (result) + { + case EvaluationResult::Error: + return EvaluationResult::Error; + case EvaluationResult::True: + break; + case EvaluationResult::False: + someFalse = true; + break; + case EvaluationResult::Unknown: + someUnknown = true; + break; + } + } + + if (someFalse) + return EvaluationResult::False; + + if (someUnknown) + return EvaluationResult::Unknown; + + return EvaluationResult::True; + } + + template + static EvaluationResult visit(const ast::Biconditional &biconditional, Arguments &&... arguments) + { + const auto leftResult = evaluate(biconditional.left, std::forward(arguments)...); + const auto rightResult = evaluate(biconditional.right, std::forward(arguments)...); + + if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error) + return EvaluationResult::Error; + + if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown) + return EvaluationResult::Unknown; + + return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False); + } + + template + static EvaluationResult visit(const ast::Boolean &boolean, Arguments &&...) + { + return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False); + } + + template + static EvaluationResult visit(const ast::Comparison &comparison, Arguments &&... arguments) + { + const auto leftType = type(comparison.left, std::forward(arguments)...); + const auto rightType = type(comparison.right, std::forward(arguments)...); + + // Comparisons with empty sets always return false + if (leftType.setSize == SetSize::Empty || rightType.setSize == SetSize::Empty) + return EvaluationResult::False; + + // If either side has an unknown domain, the result is unknown + if (leftType.domain == Domain::Unknown || rightType.domain == Domain::Unknown) + return EvaluationResult::Unknown; + + // If both sides have the same domain, the result is unknown + if (leftType.domain == rightType.domain) + return EvaluationResult::Unknown; + + // If one side is integer, but the other one isn’t, they are not equal + switch (comparison.operator_) + { + case ast::Comparison::Operator::Equal: + return EvaluationResult::False; + case ast::Comparison::Operator::NotEqual: + return EvaluationResult::True; + default: + // TODO: implement more cases + return EvaluationResult::Unknown; + } + } + + template + static EvaluationResult visit(const ast::Exists &exists, Arguments &&... arguments) + { + return evaluate(exists.argument, std::forward(arguments)...); + } + + template + static EvaluationResult visit(const ast::ForAll &forAll, Arguments &&... arguments) + { + return evaluate(forAll.argument, std::forward(arguments)...); + } + + template + static EvaluationResult visit(const ast::Implies &implies, Arguments &&... arguments) + { + const auto antecedentResult = evaluate(implies.antecedent, std::forward(arguments)...); + const auto consequentResult = evaluate(implies.consequent, std::forward(arguments)...); + + if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error) + return EvaluationResult::Error; + + if (antecedentResult == EvaluationResult::False) + return EvaluationResult::True; + + if (consequentResult == EvaluationResult::True) + return EvaluationResult::True; + + if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False) + return EvaluationResult::False; + + return EvaluationResult::Unknown; + } + + template + static EvaluationResult visit(const ast::In &in, Arguments &&... arguments) + { + const auto elementType = type(in.element, std::forward(arguments)...); + const auto setType = type(in.set, std::forward(arguments)...); + + // The element to test shouldn’t be empty or a proper set by itself + assert(elementType.setSize != SetSize::Empty && elementType.setSize != SetSize::Multi); + + // If the set is empty, no element can be selected + if (setType.setSize == SetSize::Empty) + return EvaluationResult::False; + + // If one of the sides has an unknown type, the result is unknown + if (elementType.domain == Domain::Unknown || setType.domain == Domain::Unknown) + return EvaluationResult::Unknown; + + // If both sides have the same domain, the result is unknown + if (elementType.domain == setType.domain) + return EvaluationResult::Unknown; + + // If one side is integer, but the other one isn’t, set inclusion is never satisfied + return EvaluationResult::False; + } + + template + static EvaluationResult visit(const ast::Not ¬_, Arguments &&... arguments) + { + const auto result = evaluate(not_.argument, std::forward(arguments)...); + + if (result == EvaluationResult::Error || result == EvaluationResult::Unknown) + return result; + + return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True); + } + + template + static EvaluationResult visit(const ast::Or &or_, Arguments &&... arguments) + { + bool someTrue = false; + bool someUnknown = false; + + for (const auto &argument : or_.arguments) + { + const auto result = evaluate(argument, std::forward(arguments)...); + + switch (result) + { + case EvaluationResult::Error: + return EvaluationResult::Error; + case EvaluationResult::True: + someTrue = true; + break; + case EvaluationResult::False: + break; + case EvaluationResult::Unknown: + someUnknown = true; + break; + } + } + + if (someTrue) + return EvaluationResult::True; + + if (someUnknown) + return EvaluationResult::Unknown; + + return EvaluationResult::False; + } + + template + static EvaluationResult visit(const ast::Predicate &predicate, Arguments &&... arguments) + { + assert(predicate.arguments.size() == predicate.declaration->arity()); + + for (size_t i = 0; i < predicate.arguments.size(); i++) + { + const auto &argument = predicate.arguments[i]; + const auto ¶meter = predicate.declaration->parameters[i]; + + if (parameter.domain != Domain::Integer) + continue; + + const auto argumentType = type(argument, std::forward(arguments)...); + + if (argumentType.domain == Domain::Noninteger || argumentType.setSize == SetSize::Empty) + return EvaluationResult::Error; + } + + return EvaluationResult::Unknown; + } +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +template +EvaluationResult evaluate(const ast::Formula &formula, Arguments &&... arguments) +{ + return formula.accept(EvaluateFormulaVisitor(), std::forward(arguments)...); +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/include/anthem/Type.h b/include/anthem/Type.h index 61442ea..1e48ad7 100644 --- a/include/anthem/Type.h +++ b/include/anthem/Type.h @@ -2,6 +2,7 @@ #define __ANTHEM__TYPE_H #include +#include #include namespace anthem @@ -13,16 +14,6 @@ namespace anthem // //////////////////////////////////////////////////////////////////////////////////////////////////// -struct DefaultVariableDomainAccessor -{ - Domain operator()(const ast::Variable &variable) - { - return variable.declaration->domain; - } -}; - -//////////////////////////////////////////////////////////////////////////////////////////////////// - template Type type(const ast::Term &term, Arguments &&... arguments); diff --git a/include/anthem/Utils.h b/include/anthem/Utils.h index bad2c1a..f10f1f5 100644 --- a/include/anthem/Utils.h +++ b/include/anthem/Utils.h @@ -33,6 +33,16 @@ enum class OperationResult //////////////////////////////////////////////////////////////////////////////////////////////////// +enum class EvaluationResult +{ + True, + False, + Unknown, + Error, +}; + +//////////////////////////////////////////////////////////////////////////////////////////////////// + enum class Domain { Noninteger,