use std::{rc::Rc, str::FromStr};
use logos::{Lexer, Logos};
use malachite_bigint::{BigInt, Sign};
use veripb_formula::prelude::*;
use veripb_parser::error::ParserError;
use crate::prelude::*;
use super::{Rule, RuleToken};
#[derive(Debug, Logos, PartialEq, Eq)]
#[logos(skip r"[ \t\r\n]")]
enum PolToken {
#[regex("[+-]?[0-9]+")]
Integer,
#[regex("[a-zA-Z_][_a-zA-Z0-9\\-\\^\\[\\]\\{\\}]+")]
Var,
#[regex("~[a-zA-Z_][_a-zA-Z0-9\\-\\^\\[\\]\\{\\}]+")]
NegatedVar,
#[token("s")]
Saturate,
#[token("d")]
Divide,
#[token("w")]
Weaken,
#[token("*")]
Multiply,
#[token("+")]
Add,
}
#[derive(Debug, PartialEq, Eq)]
pub enum Instruction {
ConstraintId(isize),
LiteralAxiom(Lit),
Divide(BigInt),
Multiply(BigInt),
Weaken(VarIdx),
Add,
Saturate,
}
#[derive(Debug, PartialEq, Eq)]
pub struct PolRule {
instructions: Vec<Instruction>,
}
impl PolRule {
pub fn new(instructions: Vec<Instruction>) -> Self {
Self { instructions }
}
#[inline]
pub fn parse(lex: Lexer<RuleToken>, context: &mut Context) -> Result<Self, ParserError> {
let mut lex = lex.morph();
let mut instructions = Vec::new();
let mut integer_buf: Option<&str> = None;
let mut var_buffer: Option<VarIdx> = None;
while let Some(token) = lex.next() {
if let Some(slice) = integer_buf {
integer_buf = None;
match token {
Ok(PolToken::Divide) => {
let divisor = BigInt::from_str(slice).unwrap();
if divisor.sign() != Sign::Plus {
return Err(ParserError::token_error(
lex.span(),
"positive integer as divisor",
));
}
instructions.push(Instruction::Divide(divisor));
continue;
}
Ok(PolToken::Multiply) => {
let factor = BigInt::from_str(slice).unwrap();
if factor.sign() == Sign::Minus {
return Err(ParserError::token_error(
lex.span(),
"non-negative integer as factor",
));
}
instructions.push(Instruction::Multiply(factor));
continue;
}
_ => instructions.push(Instruction::ConstraintId(slice.parse().unwrap())),
}
} else if token == Ok(PolToken::Divide) || token == Ok(PolToken::Multiply) {
return Err(ParserError::token_error(
lex.span(),
"integer before division or multiplication in cutting planes step",
));
}
if let Some(var_idx) = var_buffer {
var_buffer = None;
match token {
Ok(PolToken::Weaken) => {
instructions.push(Instruction::Weaken(var_idx));
continue;
}
_ => {
instructions.push(Instruction::LiteralAxiom(Lit::from_var(var_idx, false)));
}
}
} else if token == Ok(PolToken::Weaken) {
return Err(ParserError::token_error(
lex.span(),
"variable name before weakening rule",
));
}
match token {
Ok(PolToken::Integer) => integer_buf = Some(lex.slice()),
Ok(PolToken::Var) => var_buffer = Some(context.var_names.add_by_name(lex.slice())),
Ok(PolToken::NegatedVar) => instructions.push(Instruction::LiteralAxiom(
Lit::from_var(context.var_names.add_by_name(&lex.slice()[1..]), true),
)),
Ok(PolToken::Saturate) => instructions.push(Instruction::Saturate),
Ok(PolToken::Add) => instructions.push(Instruction::Add),
Err(_) => {
return Err(ParserError::token_error(
lex.span(),
"integer, literal, '+', '*', 'd', 's', or 'w'",
))
}
_ => {}
}
}
if let Some(slice) = integer_buf {
instructions.push(Instruction::ConstraintId(slice.parse().unwrap()))
}
if let Some(var_idx) = var_buffer {
instructions.push(Instruction::LiteralAxiom(Lit::from_var(var_idx, false)));
}
Ok(PolRule { instructions })
}
}
impl Rule for PolRule {
fn compute(
&mut self,
context: &mut Context,
database: &mut Database,
) -> Result<Vec<Rc<DBConstraint>>, CheckingError> {
let mut stack: Vec<PBConstraintEnum> = Vec::new();
for instruction in self.instructions.iter_mut() {
match instruction {
Instruction::ConstraintId(index) => {
*index = database.normalize_id(*index);
let constraint = database.get_entry_usize(*index as usize)?;
if context.only_core && !constraint.is_core_constraint_id(*index as usize) {
return Err(CheckingError::CoreSubproofUsingNonCoreConstraint(*index));
}
stack.push(constraint.constraint.clone());
}
Instruction::LiteralAxiom(lit) => {
stack.push(Cardinality::from_lits(vec![*lit], 0).into())
}
Instruction::Saturate => match stack.last_mut() {
Some(constraint) => constraint.saturate(),
None => return Err(CheckingError::NotEnoughConstraintsOnStack),
},
Instruction::Weaken(var_idx) => match stack.last_mut() {
Some(constraint) => {
if let Some(replacement) = constraint.weaken(*var_idx) {
stack.pop();
stack.push(replacement);
}
}
None => return Err(CheckingError::NotEnoughConstraintsOnStack),
},
Instruction::Divide(divisor) => match stack.last_mut() {
Some(constraint) => constraint.cutting_planes_div(divisor),
None => return Err(CheckingError::NotEnoughConstraintsOnStack),
},
Instruction::Multiply(factor) => match stack.last_mut() {
Some(constraint) => {
if let Some(replacement) = constraint.multiply(factor) {
stack.pop();
stack.push(replacement);
}
}
None => return Err(CheckingError::NotEnoughConstraintsOnStack),
},
Instruction::Add => {
if let Some(second) = stack.pop() {
if let Some(first) = stack.last_mut() {
if let Some(replacement) = first.add(&second) {
stack.pop();
stack.push(replacement);
}
continue;
}
return Err(CheckingError::NotEnoughConstraintsOnStack);
}
return Err(CheckingError::NotEnoughConstraintsOnStack);
}
}
}
if stack.len() != 1 {
return Err(CheckingError::StackNotOne(stack.len()));
}
Ok(vec![Rc::new(DBConstraint::from(
stack.pop().unwrap().into_smallest_type(),
))])
}
#[inline]
fn elaborate(
&self,
context: &mut Context,
database: &Database,
) -> Result<(), ElaborationError> {
let elaborator = context.elaborator.as_mut().unwrap();
elaborator.write("pol");
for instruction in self.instructions.iter() {
elaborator.write(" ");
match instruction {
Instruction::ConstraintId(index) => {
let constraint = database
.get_entry_usize(*index as usize)
.expect("constraint at this ID was successfully accessed before");
elaborator.write(
&constraint
.get_out_id(*index as usize)
.expect("constraint should have output ID")
.to_string(),
);
}
Instruction::LiteralAxiom(lit) => {
elaborator.write(&lit.to_pretty_string(&context.var_names))
}
Instruction::Divide(big_int) => {
elaborator.write(&big_int.to_string());
elaborator.write(" d");
}
Instruction::Multiply(big_int) => {
elaborator.write(&big_int.to_string());
elaborator.write(" *");
}
Instruction::Weaken(var) => {
elaborator.write(&var.to_pretty_string(&context.var_names));
elaborator.write(" w");
}
Instruction::Add => elaborator.write("+"),
Instruction::Saturate => elaborator.write("s"),
}
}
elaborator.writeln(";");
Ok(())
}
#[inline]
fn is_subproof_friendly(&self) -> bool {
true
}
}