patrick
/
anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity
anthem/src/anthem/IntegerVariableDetection.cpp

547 lines
18 KiB
C++
Raw Normal View History

Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
#include <anthem/IntegerVariableDetection.h>
Move arithmetic check to separate header Checking whether terms are arithmetic will be used not just in integer variable detection but also in simplifying formulas with integer variables. For this purpose, the arithmetic check is moved to a commonly accessible header file.
2018-04-21 17:47:27 +02:00
#include <anthem/Arithmetics.h>
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
#include <anthem/ASTCopy.h>
#include <anthem/ASTUtils.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Exception.h>
#include <anthem/Simplification.h>
Consolidate commonly used enum classes This moves the commonly enum classes EvaluationResult, OperationResult, and Tristate to the Utils header file to avoid code duplication. Additionally, the SimplificationResult class is replaced by the semantically similar OperationResult.
2018-04-21 17:34:52 +02:00
#include <anthem/Utils.h>
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
#include <anthem/output/AST.h>
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// IntegerVariableDetection
//
////////////////////////////////////////////////////////////////////////////////////////////////////
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
using VariableDomainMap = std::map<const ast::VariableDeclaration *, ast::Domain>;
////////////////////////////////////////////////////////////////////////////////////////////////////
ast::Domain domain(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
{
if (variable.declaration->domain != ast::Domain::Unknown)
return variable.declaration->domain;
const auto match = variableDomainMap.find(variable.declaration);
if (match == variableDomainMap.end())
return ast::Domain::Unknown;
return match->second;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
void clearVariableDomainMap(VariableDomainMap &variableDomainMap)
{
for (auto &variableDeclaration : variableDomainMap)
variableDeclaration.second = ast::Domain::Unknown;
}
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
////////////////////////////////////////////////////////////////////////////////////////////////////
Move arithmetic check to separate header Checking whether terms are arithmetic will be used not just in integer variable detection but also in simplifying formulas with integer variables. For this purpose, the arithmetic check is moved to a commonly accessible header file.
2018-04-21 17:47:27 +02:00
struct VariableDomainMapAccessor
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
{
Move arithmetic check to separate header Checking whether terms are arithmetic will be used not just in integer variable detection but also in simplifying formulas with integer variables. For this purpose, the arithmetic check is moved to a commonly accessible header file.
2018-04-21 17:47:27 +02:00
ast::Domain operator()(const ast::Variable &variable, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Move arithmetic check to separate header Checking whether terms are arithmetic will be used not just in integer variable detection but also in simplifying formulas with integer variables. For this purpose, the arithmetic check is moved to a commonly accessible header file.
2018-04-21 17:47:27 +02:00
return domain(variable, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Move arithmetic check to separate header Checking whether terms are arithmetic will be used not just in integer variable detection but also in simplifying formulas with integer variables. For this purpose, the arithmetic check is moved to a commonly accessible header file.
2018-04-21 17:47:27 +02:00
return isArithmetic<VariableDomainMapAccessor>(term, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
////////////////////////////////////////////////////////////////////////////////////////////////////
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
////////////////////////////////////////////////////////////////////////////////////////////////////
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
struct EvaluateFormulaVisitor
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::And &and_, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
bool someFalse = false;
bool someUnknown = false;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
for (const auto &argument : and_.arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto result = evaluate(argument, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
switch (result)
{
case EvaluationResult::Error:
return EvaluationResult::Error;
case EvaluationResult::True:
break;
case EvaluationResult::False:
someFalse = true;
break;
case EvaluationResult::Unknown:
someUnknown = true;
break;
}
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (someFalse)
return EvaluationResult::False;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (someUnknown)
return EvaluationResult::Unknown;
return EvaluationResult::True;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Biconditional &biconditional, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto leftResult = evaluate(biconditional.left, variableDomainMap);
const auto rightResult = evaluate(biconditional.right, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (leftResult == EvaluationResult::Error || rightResult == EvaluationResult::Error)
return EvaluationResult::Error;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (leftResult == EvaluationResult::Unknown || rightResult == EvaluationResult::Unknown)
return EvaluationResult::Unknown;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
return (leftResult == rightResult ? EvaluationResult::True : EvaluationResult::False);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Boolean &boolean, VariableDomainMap &)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
return (boolean.value == true ? EvaluationResult::True : EvaluationResult::False);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Comparison &comparison, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto isLeftArithmetic = isArithmetic(comparison.left, variableDomainMap);
const auto isRightArithmetic = isArithmetic(comparison.right, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (isLeftArithmetic == EvaluationResult::Error || isRightArithmetic == EvaluationResult::Error)
return EvaluationResult::Error;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (isLeftArithmetic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
return EvaluationResult::Unknown;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (isLeftArithmetic == isRightArithmetic)
return EvaluationResult::Unknown;
// Handle the case where one side is arithmetic but the other one isn’t
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;
}
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Exists &exists, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
return evaluate(exists.argument, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::ForAll &forAll, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
return evaluate(forAll.argument, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Implies &implies, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto antecedentResult = evaluate(implies.antecedent, variableDomainMap);
const auto consequentResult = evaluate(implies.consequent, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (antecedentResult == EvaluationResult::Error || consequentResult == EvaluationResult::Error)
return EvaluationResult::Error;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (antecedentResult == EvaluationResult::False)
return EvaluationResult::True;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (consequentResult == EvaluationResult::True)
return EvaluationResult::True;
if (antecedentResult == EvaluationResult::True && consequentResult == EvaluationResult::False)
return EvaluationResult::False;
return EvaluationResult::Unknown;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::In &in, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto isElementArithmetic = isArithmetic(in.element, variableDomainMap);
const auto isSetArithmetic = isArithmetic(in.set, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (isElementArithmetic == EvaluationResult::Error || isSetArithmetic == EvaluationResult::Error)
return EvaluationResult::Error;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (isElementArithmetic == EvaluationResult::Unknown || isSetArithmetic == EvaluationResult::Unknown)
return EvaluationResult::Unknown;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (isElementArithmetic == isSetArithmetic)
return EvaluationResult::Unknown;
// If one side is arithmetic, but the other one isn’t, set inclusion is never satisfied
return EvaluationResult::False;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Not &not_, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto result = evaluate(not_.argument, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::Unknown)
return result;
return (result == EvaluationResult::True ? EvaluationResult::False : EvaluationResult::True);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Or &or_, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
bool someTrue = false;
bool someUnknown = false;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
for (const auto &argument : or_.arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto result = evaluate(argument, variableDomainMap);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
switch (result)
{
case EvaluationResult::Error:
return EvaluationResult::Error;
case EvaluationResult::True:
someTrue = true;
break;
case EvaluationResult::False:
break;
case EvaluationResult::Unknown:
someUnknown = true;
break;
}
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (someTrue)
return EvaluationResult::True;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (someUnknown)
return EvaluationResult::Unknown;
return EvaluationResult::False;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
static EvaluationResult visit(const ast::Predicate &predicate, VariableDomainMap &variableDomainMap)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
assert(predicate.arguments.size() == predicate.declaration->arity());
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto &argument = predicate.arguments[i];
const auto &parameter = predicate.declaration->parameters[i];
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (parameter.domain != ast::Domain::Integer)
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
continue;
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
const auto isArgumentArithmetic = isArithmetic(argument, variableDomainMap);
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
if (isArgumentArithmetic == EvaluationResult::Error || isArgumentArithmetic == EvaluationResult::False)
return isArgumentArithmetic;
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
}
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
return EvaluationResult::Unknown;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variableDomainMap)
{
return formula.accept(EvaluateFormulaVisitor(), variableDomainMap);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class Functor>
struct ForEachVariableDeclarationVisitor
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::And &and_, Arguments &&... arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : and_.arguments)
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
return operationResult;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
auto operationResult = OperationResult::Unchanged;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
return operationResult;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Boolean &, Arguments &&...)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
return OperationResult::Unchanged;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Comparison &, Arguments &&...)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
return OperationResult::Unchanged;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
auto operationResult = OperationResult::Unchanged;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
for (auto &variableDeclaration : exists.variables)
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
return operationResult;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
auto operationResult = OperationResult::Unchanged;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
for (auto &variableDeclaration : forAll.variables)
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
return operationResult;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
auto operationResult = OperationResult::Unchanged;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
return operationResult;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::In &, Arguments &&...)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
return OperationResult::Unchanged;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Not &not_, Arguments &&... arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : or_.arguments)
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
operationResult = OperationResult::Changed;
return operationResult;
}
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
template <class... Arguments>
static OperationResult visit(ast::Predicate &, Arguments &&...)
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
{
Remove unwanted detection rule This piece of code was responsible for propagating the domain of predicate parameters to argument variables. However, this approach doesn’t seem to be correct, which is why this commit removes it.
2018-04-21 15:47:49 +02:00
return OperationResult::Unchanged;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
struct CheckIfDefinitionFalseFunctor
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
{
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != ast::Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
auto result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
return OperationResult::Unchanged;
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[&variableDeclaration] = ast::Domain::General;
result = evaluate(definition, variableDomainMap);
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
variableDeclaration.domain = ast::Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfQuantifiedFormulaFalseFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != ast::Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
auto result = evaluate(quantifiedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
return OperationResult::Unchanged;
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[&variableDeclaration] = ast::Domain::General;
result = evaluate(quantifiedFormula, variableDomainMap);
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
variableDeclaration.domain = ast::Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
////////////////////////////////////////////////////////////////////////////////////////////////////
Extend integer variable detection If making a variable noninteger turns the entire formula obtained from completion true, we can drop that statement and conclude that the variable is integer.
2018-04-21 17:10:24 +02:00
struct CheckIfCompletedFormulaTrueFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != ast::Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
auto result = evaluate(completedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::True)
return OperationResult::Unchanged;
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[&variableDeclaration] = ast::Domain::General;
result = evaluate(completedFormula, variableDomainMap);
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
variableDeclaration.domain = ast::Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
// Assumes the completed formulas to be in translated but not simplified form.
// That is, completed formulas are either variable-free or universally quantified
void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
{
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
VariableDomainMap variableDomainMap;
auto operationResult = OperationResult::Changed;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
while (operationResult == OperationResult::Changed)
{
operationResult = OperationResult::Unchanged;
for (auto &completedFormula : completedFormulas)
{
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
operationResult = OperationResult::Changed;
Extend integer variable detection If making a variable noninteger turns the entire formula obtained from completion true, we can drop that statement and conclude that the variable is integer.
2018-04-21 17:10:24 +02:00
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), completedFormula, variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
if (!completedFormula.is<ast::ForAll>())
continue;
auto &forAll = completedFormula.get<ast::ForAll>();
if (!forAll.argument.is<ast::Biconditional>())
continue;
auto &biconditional = forAll.argument.get<ast::Biconditional>();
if (!biconditional.left.is<ast::Predicate>())
continue;
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
auto &predicate = biconditional.left.get<ast::Predicate>();
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
auto &definition = biconditional.right;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfDefinitionFalseFunctor>(), definition, variableDomainMap) == OperationResult::Changed)
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
operationResult = OperationResult::Changed;
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
assert(predicate.arguments.size() == predicate.declaration->arity());
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
auto &variableArgument = predicate.arguments[i];
Reimplement integer variable detection This is a reimplementation of the integer variable detection procedure. The idea is to iteratively assume variables to be noninteger, and to prove that this would lead to a false or erroneous result. If the proof is successful, the variable is integer as a consequence.
2018-04-20 16:12:54 +02:00
auto &parameter = predicate.declaration->parameters[i];
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
assert(variableArgument.is<ast::Variable>());
auto &variable = variableArgument.get<ast::Variable>();
Refactor integer variable detection This reimplements integer variable detection as two parts. The first one is a visitor class that recursively searches for all declared variables in a formula and applies the second part, a custom functor. Two such functors are implemented. The first one checks whether a predicate definition is falsified by making a variable noninteger, in which case it can be concluded that the variable in question is integer. The second functor checks whether bound variables in a quantified formula turn the quantified part false, again to conclude that variables are integer.
2018-04-21 16:54:08 +02:00
parameter.domain = variable.declaration->domain;
Propagate predicate parameter domains With this change, domains detected for predicate parameters are properly propagated to all occurences of the respective variables, enabling more integer simplifications.
2018-04-19 16:57:27 +02:00
}
Implement basic integer variable detection This adds initial support for detecting integer variables in formulas. The scope is somewhat limited in that variables matching predicate parameters with known integer type aren’t propagated to be integer as well yet. Also, the use of constants and functions prevents variables from being detected as integer, because they have to be assumed to be externally defined in such a way that they evaluate to general values and not necessarily integers.
2018-04-19 15:08:50 +02:00
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}