Skip to content
Commit a884a5b2 authored by Christoph Schwering's avatar Christoph Schwering
Browse files

Added Clause::ResolveWrt(), which supersedes Clause::ResolveWithUnit().

* Added Clause::ResolveWrt(). The public version takes two clauses and
  an atom. It looks for all for all literals with the same predicate
  symbol in the two given clauses and tries to resolve them.
  The private version takes the two clauses and these two literals, it
  generalizes the old and now removed Clause::ResolveWithUnit().
  SimpleClause::ResolveWrt() is another simple helper.
* Removed SimpleClause::Unify because its task is highly specialized
  and not captured by its name and it's used only in one place.
  (Clause::Unify() will probably removed as well.)
  same speed in non-debug mode) Clause::ResolveWrt().
parent 981ed30a
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment