1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
use std::rc::Rc;
use logos::Lexer;
use veripb_formula::prelude::*;
use veripb_parser::{error::ParserError, opb_parser::parse_single_constraint};
use crate::prelude::*;
/// Check that there is a constraint in the database that is equal to the expected constraint.
#[derive(Debug)]
pub struct RUPRule {
constraint: Rc<DBConstraint>,
hint: Option<Vec<isize>>,
}
impl RUPRule {
pub fn new(constraint: PBConstraintEnum, hint: Option<Vec<isize>>) -> Self {
Self {
constraint: Rc::new(DBConstraint::from(constraint)),
hint,
}
}
pub fn parse(lex: Lexer<RuleToken>, context: &mut Context) -> Result<Self, ParserError> {
let mut lex = lex.morph();
let (geq_constraint, leq_constraint) =
parse_single_constraint(&mut lex, &mut context.var_names)?;
if leq_constraint.is_some() {
Err(ParserError::token_error(
0..lex.span().end,
"inequality constraint",
))
} else {
let mut lex = lex.morph();
match RUPHint::parse_optional(&mut lex)? {
Some(integer) => {
let mut hint = vec![0, integer];
while let Some(integer) = RUPHint::parse_optional(&mut lex)? {
hint.push(integer);
}
Ok(RUPRule {
constraint: Rc::new(DBConstraint::from(geq_constraint)),
hint: Some(hint),
})
}
None => Ok(RUPRule {
constraint: Rc::new(DBConstraint::from(geq_constraint)),
hint: None,
}),
}
}
}
}
impl Rule for RUPRule {
#[inline]
fn compute(
&mut self,
context: &mut Context,
database: &mut Database,
) -> Result<Vec<Rc<DBConstraint>>, CheckingError> {
let mut proof_buf = None;
if let Some(elaborator) = context.elaborator.as_mut() {
proof_buf = Some(&mut elaborator.proof_buf);
}
match &self.hint {
None => {
// Do unit propagation check to see if constraint is implied.
database.update_propagation_index(&mut context.propagation_engine)?;
if context
.propagation_engine
.reverse_unit_propagation_check(
&context.var_names,
&[],
Some(&self.constraint),
context.only_core,
&mut proof_buf,
context.args.trace_failed,
)?
.is_conflict()
{
Ok(vec![self.constraint.clone()])
} else {
Err(CheckingError::NotRUP(context.only_core))
}
}
Some(hint) => {
// Do propagation based on the constraint IDs given as hint.
context.annotated_rup_assignment.reset();
context
.annotated_rup_assignment
.resize(context.var_names.len());
let negated = self.constraint.negate();
loop {
let mut unchanged = true;
for id in hint {
let id = database.normalize_id(*id);
if id == 0 {
match negated.propagate(&mut context.annotated_rup_assignment) {
ConstraintPropagationResult::Conflict => {
if let Some(buf) = proof_buf.as_mut() {
buf.push_str(" ~");
}
return Ok(vec![self.constraint.clone()]);
}
ConstraintPropagationResult::NoPropagation => {}
ConstraintPropagationResult::Propagated => {
unchanged = false;
if let Some(buf) = proof_buf.as_mut() {
buf.push_str(" ~");
}
}
}
} else {
let constraint = database.get_entry_usize(id as usize)?;
if context.only_core && !constraint.is_core_constraint_id(id as usize) {
return Err(CheckingError::CoreSubproofUsingNonCoreConstraint(id));
}
match constraint.propagate(&mut context.annotated_rup_assignment) {
ConstraintPropagationResult::Conflict => {
if let Some(buf) = proof_buf.as_mut() {
buf.push(' ');
buf.push_str(
&constraint
.get_out_id(constraint.get_some_id())
.expect("should have output ID")
.to_string(),
);
}
return Ok(vec![self.constraint.clone()]);
}
ConstraintPropagationResult::NoPropagation => {}
ConstraintPropagationResult::Propagated => {
unchanged = false;
if let Some(buf) = proof_buf.as_mut() {
buf.push(' ');
buf.push_str(
&constraint
.get_out_id(constraint.get_some_id())
.expect("should have output ID")
.to_string(),
);
}
}
}
};
}
if unchanged {
return Err(CheckingError::NotRUP(context.only_core));
}
}
}
}
}
#[inline]
fn elaborate(
&self,
context: &mut Context,
_database: &Database,
) -> Result<(), ElaborationError> {
let elaborator = context.elaborator.as_mut().unwrap();
elaborator.write("rup ");
elaborator.write(&self.constraint.to_pretty_string(&context.var_names));
elaborator.write(" :");
elaborator.write_and_clear_buf();
elaborator.writeln(";");
Ok(())
}
#[inline]
fn is_subproof_friendly(&self) -> bool {
true
}
}