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

656 lines
21 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>
#include <anthem/ASTCopy.h>
#include <anthem/ASTUtils.h>
#include <anthem/ASTVisitors.h>
#include <anthem/Exception.h>
#include <anthem/Simplification.h>
#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
////////////////////////////////////////////////////////////////////////////////////////////////////
enum class OperationResult
{
Unchanged,
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
enum class EvaluationResult
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
True,
False,
Unknown,
Error,
};
////////////////////////////////////////////////////////////////////////////////////////////////////
EvaluationResult isArithmetic(const ast::Term &term, VariableDomainMap &variableDomainMap);
////////////////////////////////////////////////////////////////////////////////////////////////////
struct IsTermArithmeticVisitor
{
static EvaluationResult visit(const ast::BinaryOperation &binaryOperation, 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 isLeftArithemtic = isArithmetic(binaryOperation.left, variableDomainMap);
const auto isRightArithmetic = isArithmetic(binaryOperation.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 (isLeftArithemtic == 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 (isLeftArithemtic == EvaluationResult::False || isRightArithmetic == EvaluationResult::False)
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 (isLeftArithemtic == EvaluationResult::Unknown || isRightArithmetic == EvaluationResult::Unknown)
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::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 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::Function &function, 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 (function.declaration->domain)
{
case ast::Domain::General:
return EvaluationResult::False;
case ast::Domain::Integer:
return EvaluationResult::True;
case ast::Domain::Unknown:
return 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
static EvaluationResult visit(const ast::Integer &, 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 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::Interval &interval, 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 isFromArithmetic = isArithmetic(interval.from, variableDomainMap);
const auto isToArithmetic = isArithmetic(interval.to, 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 (isFromArithmetic == EvaluationResult::Error || isToArithmetic == 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 (isFromArithmetic == EvaluationResult::False || isToArithmetic == EvaluationResult::False)
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 (isFromArithmetic == EvaluationResult::Unknown || isToArithmetic == EvaluationResult::Unknown)
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::SpecialInteger &, 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 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::String &, 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 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::UnaryOperation &unaryOperation, 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 isArgumentArithmetic = isArithmetic(unaryOperation.argument, variableDomainMap);
switch (unaryOperation.operator_)
{
case ast::UnaryOperation::Operator::Absolute:
return (isArgumentArithmetic == EvaluationResult::False ? EvaluationResult::Error : isArgumentArithmetic);
}
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::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
{
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 (domain(variable, variableDomainMap))
{
case ast::Domain::General:
return EvaluationResult::False;
case ast::Domain::Integer:
return EvaluationResult::True;
case ast::Domain::Unknown:
return 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
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
{
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 term.accept(IsTermArithmeticVisitor(), 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);
}
////////////////////////////////////////////////////////////////////////////////////////////////////
OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, 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
struct DetectIntegerVariablesVisitor
{
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 OperationResult visit(ast::And &and_, ast::Formula &definition, 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
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : and_.arguments)
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 (detectIntegerVariables(argument, definition, variableDomainMap) == 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;
}
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 OperationResult visit(ast::Biconditional &biconditional, ast::Formula &definition, 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
{
auto operationResult = 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
if (detectIntegerVariables(biconditional.left, definition, variableDomainMap) == 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;
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 (detectIntegerVariables(biconditional.right, definition, variableDomainMap) == 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;
}
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 OperationResult visit(ast::Boolean &, ast::Formula &, 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
{
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
static OperationResult visit(ast::Comparison &, ast::Formula &, 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
{
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
static OperationResult visit(ast::Exists &exists, ast::Formula &definition, 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
{
auto operationResult = 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
if (detectIntegerVariables(exists.argument, definition, variableDomainMap) == 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)
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 (variableDeclaration->domain != ast::Domain::Unknown)
continue;
clearVariableDomainMap(variableDomainMap);
auto argumentResult = evaluate(exists.argument, variableDomainMap);
auto definitionResult = evaluate(definition, variableDomainMap);
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == 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
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
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
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
argumentResult = evaluate(exists.argument, variableDomainMap);
definitionResult = evaluate(definition, 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 (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
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;
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
variableDeclaration->domain = ast::Domain::Integer;
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
}
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;
}
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 OperationResult visit(ast::ForAll &forAll, ast::Formula &definition, 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
{
auto operationResult = 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
if (detectIntegerVariables(forAll.argument, definition, variableDomainMap) == 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)
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 (variableDeclaration->domain != ast::Domain::Unknown)
continue;
clearVariableDomainMap(variableDomainMap);
auto argumentResult = evaluate(forAll.argument, variableDomainMap);
auto definitionResult = evaluate(definition, variableDomainMap);
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == 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
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
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
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
argumentResult = evaluate(forAll.argument, variableDomainMap);
definitionResult = evaluate(definition, 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 (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
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;
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
variableDeclaration->domain = ast::Domain::Integer;
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
}
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;
}
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 OperationResult visit(ast::Implies &implies, ast::Formula &definition, 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
{
auto operationResult = 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
if (detectIntegerVariables(implies.antecedent, definition, variableDomainMap) == 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;
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 (detectIntegerVariables(implies.consequent, definition, variableDomainMap) == 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;
}
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 OperationResult visit(ast::In &, ast::Formula &, 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
{
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
static OperationResult visit(ast::Not &not_, ast::Formula &definition, 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 detectIntegerVariables(not_.argument, definition, 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 OperationResult visit(ast::Or &or_, ast::Formula &definition, 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
{
auto operationResult = OperationResult::Unchanged;
for (auto &argument : or_.arguments)
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 (detectIntegerVariables(argument, definition, variableDomainMap) == 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;
}
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 OperationResult visit(ast::Predicate &predicate, ast::Formula &, 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
auto operationResult = OperationResult::Unchanged;
assert(predicate.arguments.size() == predicate.declaration->arity());
// Propagate integer domains from predicates to variables
for (size_t i = 0; i < predicate.arguments.size(); i++)
{
auto &variableArgument = predicate.arguments[i];
auto &parameter = predicate.declaration->parameters[i];
if (parameter.domain != ast::Domain::Integer)
continue;
if (!variableArgument.is<ast::Variable>())
continue;
auto &variable = variableArgument.get<ast::Variable>();
if (variable.declaration->domain == ast::Domain::Integer)
continue;
operationResult = OperationResult::Changed;
variable.declaration->domain = ast::Domain::Integer;
}
return operationResult;
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
OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap)
{
return formula.accept(DetectIntegerVariablesVisitor(), definition, 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
// 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)
{
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 (detectIntegerVariables(completedFormula, 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;
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(predicate.arguments.size() == predicate.declaration->arity());
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 (detectIntegerVariables(definition, definition, variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed;
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>();
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::Unknown)
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
clearVariableDomainMap(variableDomainMap);
auto result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
continue;
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[variable.declaration] = 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
operationResult = OperationResult::Changed;
variable.declaration->domain = ast::Domain::Integer;
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
}
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
}
}
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}