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

Setup::AddClause() takes over the task of Setup::AddSensingResult().

With regression, adding a sensing result boils down to adding several
clauses which are the result of first regressing the SF literal and
converting the result to CNF.
That's obviously a task for Setup::AddClause(), not for
Setup::AddSensingResult().

To fulfill this task, Setup::AddClause() needs to perform the
consistency checks similar to the one performed by
Setup::AddSensingResult(). In fact, the newly added clause made things
inconsistent at level k if at for all literals from their clause, the
flipped literal is entailed at level k.

Like in Setup::AddSensingResult(), the consistency check is performed
only for those k for which there are entries in incons_. Since incons_
is empty initially when the setup is filled with clauses, the new
Setup::AddClause() has no overhead over the old version for the
traditional use case of filling the setup.

Setups::AddClause() forwards to Setup::AddClause() as before.

Removed Setup[s]::AddSensingResult() because it's subsumed by
Setup[s]::AddClause() now.
parent 27eb6b16
Loading
Loading
Loading
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment