Skip to content

Commit 60d234e

Browse files
Daniel1854Daniel1854
committed
refactor: review
1 parent 24298d8 commit 60d234e

3 files changed

Lines changed: 63 additions & 64 deletions

File tree

‎src/clause.rs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -452,6 +452,18 @@ impl Clause {
452452
.filter(|(id, _)| vec.not_any() || *vec.get(id.0).unwrap())
453453
}
454454

455+
// XXX: strategy only gets respected the first time, we could add an assertion that it never
456+
// changes
457+
pub fn non_eligible_iter<'a>(
458+
&'a self,
459+
strategy: SelectionStrategy,
460+
term_bank: &TermBank,
461+
) -> impl Iterator<Item = (LiteralId, &'a Literal)> {
462+
let vec = self.get_selected(strategy, term_bank);
463+
self.iter()
464+
.filter(|(id, _)| vec.not_any() || !*vec.get(id.0).unwrap())
465+
}
466+
455467
pub fn has_selection(&self, strategy: SelectionStrategy, term_bank: &TermBank) -> bool {
456468
self.get_selected(strategy, term_bank).any()
457469
}

‎src/selection.rs‎

Lines changed: 11 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,9 @@ use bitvec::vec::BitVec;
66
use crate::{
77
clause::{Clause, Literal, LiteralId, Polarity},
88
kbo::KboOrd,
9-
term_bank::{Sort, TermBank},
9+
term_bank::TermBank,
1010
};
1111

12-
const FILTER_PROPS: bool = false;
13-
1412
#[derive(Debug, Clone, Copy, clap::ValueEnum)]
1513
pub enum SelectionStrategy {
1614
/// Never select a literal
@@ -22,22 +20,12 @@ pub enum SelectionStrategy {
2220
ZipperSel,
2321
}
2422

25-
fn is_propositional(lit: &Literal, term_bank: &TermBank) -> bool {
26-
if let Some(id) = lit.get_rhs().function_id() {
27-
if term_bank.get_function_info(id).sort == Sort::Individual {
28-
return true;
29-
}
30-
} else {
31-
return true;
32-
}
33-
false
34-
}
35-
36-
fn select_first_neg_lit(clause: &Clause, term_bank: &TermBank) -> BitVec {
23+
fn select_first_neg_lit(clause: &Clause) -> BitVec {
3724
let mut result = bitvec![0; clause.len()];
3825
for (lit_id, lit) in clause.iter() {
39-
if lit.get_pol() == Polarity::Ne && (!FILTER_PROPS || is_propositional(lit, term_bank)) {
26+
if lit.get_pol() == Polarity::Ne {
4027
result.set(lit_id.0, true);
28+
return result;
4129
}
4230
}
4331
result
@@ -47,18 +35,14 @@ fn select_first_max_neg_lit_and_all_pos_lits(clause: &Clause, term_bank: &TermBa
4735
let mut result = bitvec![0; clause.len()];
4836
let mut max_neg_lit: Option<(LiteralId, &Literal)> = None;
4937
for (lit_id, lit) in clause.iter() {
50-
if !FILTER_PROPS || is_propositional(lit, term_bank) {
51-
if lit.get_pol() == Polarity::Eq {
52-
if !FILTER_PROPS {
53-
result.set(lit_id.0, true);
54-
}
55-
} else if let Some((_, max_lit)) = max_neg_lit {
56-
if lit.kbo(max_lit, term_bank) == Some(Ordering::Greater) {
57-
max_neg_lit = Some((lit_id, lit));
58-
}
59-
} else {
38+
if lit.get_pol() == Polarity::Eq {
39+
result.set(lit_id.0, true);
40+
} else if let Some((_, max_lit)) = max_neg_lit {
41+
if lit.kbo(max_lit, term_bank) == Some(Ordering::Greater) {
6042
max_neg_lit = Some((lit_id, lit));
6143
}
44+
} else {
45+
max_neg_lit = Some((lit_id, lit));
6246
}
6347
}
6448
if let Some((neg_lit_id, _)) = max_neg_lit {
@@ -76,7 +60,7 @@ pub fn select_literals(
7660
) -> BitVec {
7761
match strategy {
7862
SelectionStrategy::NoSel => bitvec![0; clause.len()],
79-
SelectionStrategy::FirstNeg => select_first_neg_lit(clause, term_bank),
63+
SelectionStrategy::FirstNeg => select_first_neg_lit(clause),
8064
SelectionStrategy::ZipperSel => {
8165
select_first_max_neg_lit_and_all_pos_lits(clause, term_bank)
8266
}

‎src/superposition.rs‎

Lines changed: 40 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -146,39 +146,54 @@ fn maximality_check(
146146
)
147147
}
148148

149-
// Eligiblity for Resolution: maximality check for selected literal
150-
// Returns true if the literal is maximal in the intersection of the selection
149+
// Eligiblity for Resolution Check given a non-empty selection:
150+
// Returns the substituted and filtered literals,
151+
// if the given literal is maximal in the intersection of the selection
151152
// with either the positive or negative literalset of the clause with the mgu applied
152-
fn maximal_in_selection(
153+
fn eligible_resolution_with_selection(
153154
clause: &Clause,
154155
check_lit_id: LiteralId,
155156
subst: &Substitution,
156157
selection_strategy: SelectionStrategy,
157158
term_bank: &TermBank,
158-
) -> bool {
159+
) -> Option<Vec<Literal>> {
160+
let mut new_literals = Vec::with_capacity(clause.len());
159161
let check_lit = clause
160162
.get_literal(check_lit_id)
161163
.clone()
162164
.subst_with(subst, term_bank);
163165
let mut is_pos_max = true;
164166
let mut is_neg_max = true;
165-
// Iterate through sel(C) and keep track if there is a positive or negative
166-
// literal which is greater than check_lit
167+
// Iterate through the selection and keep track if there is a positive
168+
// or negative literal which is greater than check_lit
167169
for (_, other_lit) in clause
168170
.eligible_iter(selection_strategy, term_bank)
169171
.filter(|(other_lit_id, _)| check_lit_id != *other_lit_id)
170172
{
171173
let other_lit = other_lit.clone().subst_with(subst, term_bank);
172-
if let Some(Ordering::Greater) = check_lit.kbo(&other_lit, term_bank) {
173-
// Abort: we are not maximal for the intersection of that polarity
174-
// TODO: maybe implement through streams with some early cutoff
175-
match other_lit.get_pol() {
176-
Polarity::Eq => is_pos_max = false,
177-
Polarity::Ne => is_neg_max = false,
174+
// Only compute the KBO if the polarity can make the maximality check fail
175+
if (is_pos_max && other_lit.get_pol() == Polarity::Eq)
176+
|| (is_neg_max && other_lit.get_pol() == Polarity::Ne)
177+
{
178+
if let Some(Ordering::Greater) = check_lit.kbo(&other_lit, term_bank) {
179+
// Abort: we are not maximal for the intersection of that polarity
180+
match other_lit.get_pol() {
181+
Polarity::Eq => is_pos_max = false,
182+
Polarity::Ne => is_neg_max = false,
183+
}
184+
if !is_pos_max && !is_neg_max {
185+
return None;
186+
}
178187
}
179188
}
189+
new_literals.push(other_lit);
180190
}
181-
is_pos_max || is_neg_max
191+
// On success add the remaining literals, which were not part of the selection
192+
for (_, other_lit) in clause.non_eligible_iter(selection_strategy, term_bank) {
193+
let other_lit = other_lit.clone().subst_with(subst, term_bank);
194+
new_literals.push(other_lit);
195+
}
196+
Some(new_literals)
182197
}
183198

184199
impl SuperpositionState<'_> {
@@ -379,20 +394,14 @@ impl SuperpositionState<'_> {
379394
if clause.has_selection(self.selection_strategy, self.term_bank) {
380395
// Condition 2: non-empty selection: has to be maximal in the
381396
// mgu applied intersection of the selection with either C- or C+
382-
if maximal_in_selection(
397+
if let Some(new_literals) = eligible_resolution_with_selection(
383398
clause,
384399
literal_id,
385400
&subst,
386401
self.selection_strategy,
387402
self.term_bank,
388403
) {
389-
let filtered_literals = clause
390-
.iter()
391-
.filter(|(id, _)| *id != literal_id)
392-
.map(|(_, l)| l.clone())
393-
.collect();
394-
let new_clause =
395-
Clause::new(filtered_literals).subst_with(&subst, self.term_bank);
404+
let new_clause = Clause::new(new_literals);
396405
info!(
397406
"ERes derived clause: {}",
398407
pretty_print(&new_clause, self.term_bank)
@@ -429,6 +438,13 @@ impl SuperpositionState<'_> {
429438
}
430439

431440
fn equality_factoring(&mut self, clause: &Clause, acc: &mut Vec<Clause>) {
441+
if clause.has_selection(self.selection_strategy, self.term_bank) {
442+
info!(
443+
"EFact working clause skipped due to selection: {}",
444+
pretty_print(clause, self.term_bank)
445+
);
446+
return;
447+
}
432448
info!(
433449
"EFact working clause: {}",
434450
pretty_print(clause, self.term_bank)
@@ -539,19 +555,13 @@ impl SuperpositionState<'_> {
539555
if clause2.has_selection(self.selection_strategy, self.term_bank) {
540556
// Non-empty selection: has to be maximal in the mgu applied intersection of the
541557
// selection with either C- or C+
542-
if maximal_in_selection(
558+
if let Some(mut new_literals2) = eligible_resolution_with_selection(
543559
clause2,
544560
lit2_id,
545561
subst,
546562
self.selection_strategy,
547563
self.term_bank,
548564
) {
549-
let mut new_literals2 = clause2
550-
.iter()
551-
.filter(|(id, _)| *id != lit2_id)
552-
.map(|(_, l)| l.clone())
553-
.map(|l| l.subst_with(subst, self.term_bank))
554-
.collect();
555565
new_literals1.append(&mut new_literals2);
556566
let new_rhs = l2_rhs_subst;
557567
let new_lhs = subterm_pos
@@ -613,13 +623,8 @@ impl SuperpositionState<'_> {
613623
if lit1.is_ne() {
614624
continue;
615625
}
626+
// Try to orient the equation using stability under substitution
616627
for (lit1_lhs, lit1_rhs) in lit1.oriented_symm_term_iter(self.term_bank) {
617-
// Try to orient the equation using stability under substitution
618-
let l1_ord = lit1_lhs.kbo(&lit1_rhs, self.term_bank);
619-
if l1_ord == Some(Ordering::Less) {
620-
continue;
621-
}
622-
623628
// Iterate over all possible unifying subpositions in the active set
624629
for candidate_pos in self.subterm_index.get_unification_candidates(&lit1_lhs) {
625630
let lit2_lhs_p = candidate_pos.term_at(&self.active);
@@ -714,9 +719,7 @@ impl SuperpositionState<'_> {
714719
fn generate(&mut self, clause: Clause) -> Vec<Clause> {
715720
let mut acc = Vec::new();
716721
self.equality_resolution(&clause, &mut acc);
717-
if !clause.has_selection(self.selection_strategy, self.term_bank) {
718-
self.equality_factoring(&clause, &mut acc);
719-
}
722+
self.equality_factoring(&clause, &mut acc);
720723
self.superposition(&clause, &mut acc);
721724
acc
722725
}

0 commit comments

Comments
 (0)