From e007d7fc975e18ca7c29b8b53ec1c27f4ffdc581 Mon Sep 17 00:00:00 2001 From: Abdul Zreika Date: Thu, 3 Dec 2020 14:45:11 +1100 Subject: [PATCH] Moved out eqcheck functionality. --- src/ast2ram/ClauseTranslator.cpp | 25 ++++++++++++------------- src/ast2ram/ClauseTranslator.h | 3 +++ 2 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/ast2ram/ClauseTranslator.cpp b/src/ast2ram/ClauseTranslator.cpp index b7af152c6d5..d218975e315 100644 --- a/src/ast2ram/ClauseTranslator.cpp +++ b/src/ast2ram/ClauseTranslator.cpp @@ -121,10 +121,9 @@ Own ClauseTranslator::addVariableBindingConstraints(OwnisGenerator(reference.identifier)) { - // FIXME: equiv' for float types (`FEQ`) - op = mk(mk(BinaryConstraintOp::EQ, makeRamTupleElement(first), - makeRamTupleElement(reference)), - std::move(op)); + // TODO: float type equivalence check + op = addEqualityCheck( + std::move(op), makeRamTupleElement(first), makeRamTupleElement(reference), false); } } } @@ -224,7 +223,7 @@ Own ClauseTranslator::instantiateAggregator( auto addAggEqCondition = [&](Own aggr, Own value, size_t pos) { if (isUndefValue(value.get())) return aggr; - // FIXME: equiv' for float types (`FEQ`) + // TODO: float type equivalence check return addConjunctiveTerm( std::move(aggr), mk(BinaryConstraintOp::EQ, mk(curLevel, pos), std::move(value))); @@ -368,15 +367,15 @@ Own ClauseTranslator::translateConstant( return mk(rawConstant); } -Own ClauseTranslator::addConstantConstraints( - size_t const curLevel, const std::vector& arguments, Own op) const { - // Helper function to add a constraint check - auto addEqualityCheck = [&](Own op, Own lhs, Own rhs, - bool isFloat) { - auto eqOp = isFloat ? BinaryConstraintOp::FEQ : BinaryConstraintOp::EQ; - return mk(mk(eqOp, std::move(lhs), std::move(rhs)), std::move(op)); - }; +Own ClauseTranslator::addEqualityCheck( + Own op, Own lhs, Own rhs, bool isFloat) const { + auto eqOp = isFloat ? BinaryConstraintOp::FEQ : BinaryConstraintOp::EQ; + auto eqConstraint = mk(eqOp, std::move(lhs), std::move(rhs)); + return mk(std::move(eqConstraint), std::move(op)); +} +Own ClauseTranslator::addConstantConstraints( + size_t curLevel, const std::vector& arguments, Own op) const { for (size_t i = 0; i < arguments.size(); i++) { const auto* argument = arguments.at(i); if (const auto* numericConstant = dynamic_cast(argument)) { diff --git a/src/ast2ram/ClauseTranslator.h b/src/ast2ram/ClauseTranslator.h index 7a9ebcd7152..82d386b25e7 100644 --- a/src/ast2ram/ClauseTranslator.h +++ b/src/ast2ram/ClauseTranslator.h @@ -88,6 +88,9 @@ class ClauseTranslator { void indexNodeArguments(int nodeLevel, const std::vector& nodeArgs); void indexAggregatorBody(const ast::Aggregator& agg); + Own addEqualityCheck( + Own op, Own lhs, Own rhs, bool isFloat) const; + Own createRamFactQuery(const ast::Clause& clause) const; Own createRamRuleQuery( const ast::Clause& clause, const ast::Clause& originalClause, int version);