Skip to content

Commit

Permalink
Clean up mentions to enums; remove debug code except checks in fw dem…
Browse files Browse the repository at this point in the history 
…odulation; clean up fw demodulation a bit
  • Loading branch information
@mezpusz
mezpusz committed Jan 3, 2025
1 parent 169bb52 commit c816f4e
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 140 deletions.
28 changes: 10 additions & 18 deletions Inferences/ForwardDemodulation.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,33 +162,28 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
}
}

TermList rhs = qr.data->rhs;
bool preordered = qr.data->preordered;

auto subs = qr.unifier;
ASS(subs->isIdentityOnQueryWhenResultBound());

ApplicatorWithEqSort applWithEqSort(subs.ptr(), eqSortSubs);
Applicator applWithoutEqSort(subs.ptr());
auto appl = lhs.isVar() ? (SubstApplicator*)&applWithEqSort : (SubstApplicator*)&applWithoutEqSort;

AppliedTerm rhsApplied(qr.data->rhs,appl,true);
bool preordered = qr.data->preordered;

if (_precompiledComparison) {
#if VDEBUG
auto dcomp = ordering.isGreaterOrEq(trm,rhsApplied);
#endif
qr.data->comparator->init(appl);
if (!preordered && (_preorderedOnly || !qr.data->comparator->next())) {
#if DEBUG_ORDERING
if (ordering.isGreaterOrEq(AppliedTerm(trm),AppliedTerm(rhs,appl,true))==Ordering::GREATER) {
INVALID_OPERATION("greater");
}
#endif
ASS_NEQ(dcomp,Ordering::GREATER);
continue;
}
#if DEBUG_ORDERING
if (ordering.isGreaterOrEq(AppliedTerm(trm),AppliedTerm(rhs,appl,true))!=Ordering::GREATER) {
INVALID_OPERATION("not greater");
}
#endif
ASS_EQ(dcomp,Ordering::GREATER);
} else {
if (!preordered && (_preorderedOnly || ordering.isGreaterOrEq(AppliedTerm(trm),AppliedTerm(rhs,appl,true))!=Ordering::GREATER)) {
if (!preordered && (_preorderedOnly || ordering.isGreaterOrEq(trm,rhsApplied)!=Ordering::GREATER)) {
continue;
}
}
Expand All @@ -205,10 +200,7 @@ bool ForwardDemodulationImpl<combinatorySupSupport>::perform(Clause* cl, Clause*
}
}

TermList rhsS = subs->applyToBoundResult(rhs);
if (lhs.isVar()) {
rhsS = eqSortSubs.apply(rhsS, 0);
}
TermList rhsS = rhsApplied.apply();

if (redundancyCheck && !_helper.isPremiseRedundant(cl, lit, trm, rhsS, lhs, appl)) {
continue;
Expand Down
2 changes: 0 additions & 2 deletions Kernel/Ordering.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,6 @@
#include "Lib/Portability.hpp"
#include "Kernel/SubstHelper.hpp"

#define DEBUG_ORDERING 0

namespace Kernel {


Expand Down
22 changes: 13 additions & 9 deletions Kernel/OrderingComparator.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ void* OrderingComparator::next()
AppliedTerm(node->rhs, _appl, true));

} else {
ASS(node->tag == Node::T_POLY);
ASS_EQ(node->tag, Node::T_POLY);

const auto& kbo = static_cast<const KBO&>(_ord);
auto weight = node->poly->constant;
Expand Down Expand Up @@ -451,20 +451,24 @@ const OrderingComparator::Polynomial* OrderingComparator::Polynomial::get(int co

std::ostream& operator<<(std::ostream& out, const OrderingComparator::Node::Tag& t)
{
using Tag = OrderingComparator::Node::Tag;
switch (t) {
case OrderingComparator::Node::T_DATA: return out << "d";
case OrderingComparator::Node::T_TERM: return out << "t";
case OrderingComparator::Node::T_POLY: return out << "p";
case Tag::T_DATA: return out << "d";
case Tag::T_TERM: return out << "t";
case Tag::T_POLY: return out << "p";
default: ASSERTION_VIOLATION;
}
}

std::ostream& operator<<(std::ostream& out, const OrderingComparator::Node& node)
{
out << (OrderingComparator::Node::Tag)node.tag << (node.ready?" ":"? ");
using Tag = OrderingComparator::Node::Tag;
out << (Tag)node.tag << (node.ready?" ":"? ");
switch (node.tag) {
case OrderingComparator::Node::Tag::T_DATA: return out << node.data;
case OrderingComparator::Node::Tag::T_POLY: return out << *node.poly;
case OrderingComparator::Node::Tag::T_TERM: return out << node.lhs << " " << node.rhs;
case Tag::T_DATA: return out << node.data;
case Tag::T_POLY: return out << *node.poly;
case Tag::T_TERM: return out << node.lhs << " " << node.rhs;
default: ASSERTION_VIOLATION;
}
}

Expand Down Expand Up @@ -505,7 +509,7 @@ std::ostream& operator<<(std::ostream& str, const OrderingComparator& comp)
}
str << *kv.first->node() << std::endl;
if (seen.insert(kv.first->node())) {
if (kv.first->node()->tag==OrderingComparator::Node::Tag::T_DATA) {
if (kv.first->node()->tag==OrderingComparator::Node::T_DATA) {
if (kv.first->node()->data) {
todo.push(std::make_pair(&kv.first->node()->alternative,kv.second+1));
}
Expand Down
110 changes: 3 additions & 107 deletions Kernel/TermPartialOrdering.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,9 +36,8 @@ Result poCompToResult(PoComp c) {
case PoComp::INCOMPARABLE:
return Result::INCOMPARABLE;
default:
break;
ASSERTION_VIOLATION;
}
ASSERTION_VIOLATION;
}

PoComp resultToPoComp(Result r, bool reversed) {
Expand All @@ -51,6 +50,8 @@ PoComp resultToPoComp(Result r, bool reversed) {
return reversed ? PoComp::GREATER : PoComp::LESS;
case Result::INCOMPARABLE:
return reversed ? PoComp::NLEQ : PoComp::NGEQ;
default:
ASSERTION_VIOLATION;
}
}

Expand Down Expand Up @@ -306,9 +307,6 @@ bool TermPartialOrdering::set(TermOrderingConstraint con)
if (!_po) {
return false;
}
#if DEBUG_ORDERING
// debug_check();
#endif
return true;
}

Expand Down Expand Up @@ -365,106 +363,4 @@ ostream& operator<<(ostream& str, const TermPartialOrdering& tpo)
return str;
}

#if DEBUG_ORDERING
void TermPartialOrdering::debug_check() const
{
// auto output_args = [this](size_t x, size_t y, size_t z) {
// return _po->all_to_string() + " at " + Int::toString(x) + ", " + Int::toString(y) + ", " + Int::toString(z);
// };

auto check_val = [/* &output_args */](auto actual_val, auto expected_val, size_t x, size_t y, size_t z) {
if (actual_val == PoComp::UNKNOWN) {
// INVALID_OPERATION(output_args(x,y,z));
}
if (expected_val == PoComp::NLEQ) {
if (actual_val != PoComp::NLEQ && actual_val != PoComp::INCOMPARABLE && actual_val != PoComp::GREATER) {
// INVALID_OPERATION(output_args(x,y,z));
}
} else if (expected_val == PoComp::NGEQ) {
if (actual_val != PoComp::NGEQ && actual_val != PoComp::INCOMPARABLE && actual_val != PoComp::LESS) {
// INVALID_OPERATION(output_args(x,y,z));
}
} else {
if (actual_val != expected_val) {
// INVALID_OPERATION(output_args(x,y,z));
}
}
};

decltype(_nodes)::Iterator it1(_nodes);
while (it1.hasNext()) {
auto& e1 = it1.next();

decltype(_nodes)::Iterator it2(_nodes);
while (it2.hasNext()) {
auto& e2 = it2.next();
if (e1.value() == e2.value()) {
continue;
}
auto v12 = _po->get(e1.value(),e2.value());
if (v12 == PoComp::UNKNOWN) {
continue;
}
auto comp = _ord.compare(e1.key(),e2.key());
if (comp != Ordering::INCOMPARABLE) {
check_val(v12, resultToPoComp(comp, false), e1.value(), e2.value(), e2.value());
}

decltype(_nodes)::Iterator it3(_nodes);
while (it3.hasNext()) {
auto& e3 = it3.next();
if (e1.value() == e3.value() || e2.value() == e3.value()) {
continue;
}

auto v13 = _po->get(e1.value(),e3.value());
if (v13 == PoComp::UNKNOWN) {
continue;
}

auto v23 = _po->get(e2.value(),e3.value());

switch (v12) {
case PoComp::UNKNOWN:
break;
case PoComp::EQUAL:
// x = y rel z -> x rel z
check_val(v13, v23, e1.value(), e2.value(), e3.value());
break;
case PoComp::GREATER:
case PoComp::NLEQ: {
if (v23 == PoComp::EQUAL || v23 == PoComp::GREATER) {
// x > y ≥ z -> x > z
// x ≰ y ≥ z -> x ≰ z
check_val(v13, v12, e1.value(), e2.value(), e3.value());
}
break;
}
case PoComp::LESS:
case PoComp::NGEQ: {
if (v23 == PoComp::EQUAL || v23 == PoComp::LESS) {
// x < y ≤ z -> x < z
// x ≱ y ≤ z -> x ≱ z
check_val(v13, v12, e1.value(), e2.value(), e3.value());
}
break;
}
case PoComp::INCOMPARABLE: {
if (v23 == PoComp::EQUAL || v23 == PoComp::GREATER) {
// x ≰ y ≥ z -> x ≰ z
check_val(v13, PoComp::NLEQ, e1.value(), e2.value(), e3.value());
}
if (v23 == PoComp::EQUAL || v23 == PoComp::LESS) {
// x ≱ y ≤ z -> x ≱ z
check_val(v13, PoComp::NGEQ, e1.value(), e2.value(), e3.value());
}
break;
}
}
}
}
}
}
#endif

}
4 changes: 0 additions & 4 deletions Kernel/TermPartialOrdering.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -76,10 +76,6 @@ class TermPartialOrdering
size_t getId(TermList t) const;
size_t getIdExt(TermList t);

#if DEBUG_ORDERING
void debug_check() const;
#endif

const Ordering& _ord;
Map<TermList,size_t> _nodes;
const PartialOrdering* _po;
Expand Down

0 comments on commit c816f4e

Please sign in to comment.