Skip to content

Commit

Permalink
cargo fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
@twizmwazin
twizmwazin committed Oct 28, 2024
1 parent 4c7f027 commit 9cab6d8
Show file tree
Hide file tree
Showing 4 changed files with 103 additions and 109 deletions.
190 changes: 91 additions & 99 deletions crates/clarirs_core/src/algorithms/simplify.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,41 +17,39 @@ impl<'c> Simplify<'c> for BoolAst<'c> {
Ok(self
.context()
.simplification_cache
.get_or_insert_with_bool(self.hash(), || {
match &self.op() {
BooleanOp::BoolS(_) => self.clone(),
BooleanOp::BoolV(_) => self.clone(),
BooleanOp::Not(arc) => todo!(),
BooleanOp::And(arc, arc1) => todo!(),
BooleanOp::Or(arc, arc1) => todo!(),
BooleanOp::Xor(arc, arc1) => todo!(),
BooleanOp::Eq(arc, arc1) => todo!(),
BooleanOp::Neq(arc, arc1) => todo!(),
BooleanOp::ULT(arc, arc1) => todo!(),
BooleanOp::ULE(arc, arc1) => todo!(),
BooleanOp::UGT(arc, arc1) => todo!(),
BooleanOp::UGE(arc, arc1) => todo!(),
BooleanOp::SLT(arc, arc1) => todo!(),
BooleanOp::SLE(arc, arc1) => todo!(),
BooleanOp::SGT(arc, arc1) => todo!(),
BooleanOp::SGE(arc, arc1) => todo!(),
BooleanOp::FpEq(arc, arc1) => todo!(),
BooleanOp::FpNeq(arc, arc1) => todo!(),
BooleanOp::FpLt(arc, arc1) => todo!(),
BooleanOp::FpLeq(arc, arc1) => todo!(),
BooleanOp::FpGt(arc, arc1) => todo!(),
BooleanOp::FpGeq(arc, arc1) => todo!(),
BooleanOp::FpIsNan(arc) => todo!(),
BooleanOp::FpIsInf(arc) => todo!(),
BooleanOp::StrContains(arc, arc1) => todo!(),
BooleanOp::StrPrefixOf(arc, arc1) => todo!(),
BooleanOp::StrSuffixOf(arc, arc1) => todo!(),
BooleanOp::StrIsDigit(arc) => todo!(),
BooleanOp::StrEq(arc, arc1) => todo!(),
BooleanOp::StrNeq(arc, arc1) => todo!(),
BooleanOp::If(arc, arc1, arc2) => todo!(),
BooleanOp::Annotated(arc, annotation) => todo!(),
}
.get_or_insert_with_bool(self.hash(), || match &self.op() {
BooleanOp::BoolS(_) => self.clone(),
BooleanOp::BoolV(_) => self.clone(),
BooleanOp::Not(arc) => todo!(),

Check warning on line 23 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 23 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 23 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 23 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 23 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / cargo clippy 

unused variable: `arc`

Check warning on line 23 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`

Check warning on line 23 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`
BooleanOp::And(arc, arc1) => todo!(),

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc1`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc1`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc1`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc1`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / cargo clippy 

unused variable: `arc`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / cargo clippy 

unused variable: `arc1`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc1`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`

Check warning on line 24 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc1`
BooleanOp::Or(arc, arc1) => todo!(),

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc1`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc1`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc1`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc1`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / cargo clippy 

unused variable: `arc`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / cargo clippy 

unused variable: `arc1`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc1`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`

Check warning on line 25 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc1`
BooleanOp::Xor(arc, arc1) => todo!(),

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc1`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest 

unused variable: `arc1`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc1`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on macos-latest 

unused variable: `arc1`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / cargo clippy 

unused variable: `arc`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / cargo clippy 

unused variable: `arc1`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc1`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc`

Check warning on line 26 in crates/clarirs_core/src/algorithms/simplify.rs

View workflow job for this annotation

GitHub Actions / Test on windows-latest 

unused variable: `arc1`
BooleanOp::Eq(arc, arc1) => todo!(),
BooleanOp::Neq(arc, arc1) => todo!(),
BooleanOp::ULT(arc, arc1) => todo!(),
BooleanOp::ULE(arc, arc1) => todo!(),
BooleanOp::UGT(arc, arc1) => todo!(),
BooleanOp::UGE(arc, arc1) => todo!(),
BooleanOp::SLT(arc, arc1) => todo!(),
BooleanOp::SLE(arc, arc1) => todo!(),
BooleanOp::SGT(arc, arc1) => todo!(),
BooleanOp::SGE(arc, arc1) => todo!(),
BooleanOp::FpEq(arc, arc1) => todo!(),
BooleanOp::FpNeq(arc, arc1) => todo!(),
BooleanOp::FpLt(arc, arc1) => todo!(),
BooleanOp::FpLeq(arc, arc1) => todo!(),
BooleanOp::FpGt(arc, arc1) => todo!(),
BooleanOp::FpGeq(arc, arc1) => todo!(),
BooleanOp::FpIsNan(arc) => todo!(),
BooleanOp::FpIsInf(arc) => todo!(),
BooleanOp::StrContains(arc, arc1) => todo!(),
BooleanOp::StrPrefixOf(arc, arc1) => todo!(),
BooleanOp::StrSuffixOf(arc, arc1) => todo!(),
BooleanOp::StrIsDigit(arc) => todo!(),
BooleanOp::StrEq(arc, arc1) => todo!(),
BooleanOp::StrNeq(arc, arc1) => todo!(),
BooleanOp::If(arc, arc1, arc2) => todo!(),
BooleanOp::Annotated(arc, annotation) => todo!(),
}))
}
}
Expand All @@ -61,43 +59,41 @@ impl<'c> Simplify<'c> for BitVecAst<'c> {
Ok(self
.context()
.simplification_cache
.get_or_insert_with_bv(self.hash(), || {
match &self.op() {
BitVecOp::BVS(..) => self.clone(),
BitVecOp::BVV(..) => self.clone(),
BitVecOp::SI(..) => todo!(),
BitVecOp::Not(ast) => todo!(),
BitVecOp::And(arc, arc1) => todo!(),
BitVecOp::Or(arc, arc1) => todo!(),
BitVecOp::Xor(arc, arc1) => todo!(),
BitVecOp::Add(arc, arc1) => todo!(),
BitVecOp::Sub(arc, arc1) => todo!(),
BitVecOp::Mul(arc, arc1) => todo!(),
BitVecOp::UDiv(arc, arc1) => todo!(),
BitVecOp::SDiv(arc, arc1) => todo!(),
BitVecOp::URem(arc, arc1) => todo!(),
BitVecOp::SRem(arc, arc1) => todo!(),
BitVecOp::Pow(arc, arc1) => todo!(),
BitVecOp::LShL(arc, arc1) => todo!(),
BitVecOp::LShR(arc, arc1) => todo!(),
BitVecOp::AShL(arc, arc1) => todo!(),
BitVecOp::AShR(arc, arc1) => todo!(),
BitVecOp::RotateLeft(arc, arc1) => todo!(),
BitVecOp::RotateRight(arc, arc1) => todo!(),
BitVecOp::ZeroExt(arc, _) => todo!(),
BitVecOp::SignExt(arc, _) => todo!(),
BitVecOp::Extract(arc, _, _) => todo!(),
BitVecOp::Concat(arc, arc1) => todo!(),
BitVecOp::Reverse(arc) => todo!(),
BitVecOp::FpToIEEEBV(arc) => todo!(),
BitVecOp::FpToUBV(arc, _, fprm) => todo!(),
BitVecOp::FpToSBV(arc, _, fprm) => todo!(),
BitVecOp::StrLen(arc) => todo!(),
BitVecOp::StrIndexOf(arc, arc1, arc2) => todo!(),
BitVecOp::StrToBV(arc) => todo!(),
BitVecOp::If(arc, arc1, arc2) => todo!(),
BitVecOp::Annotated(arc, annotation) => todo!(),
}
.get_or_insert_with_bv(self.hash(), || match &self.op() {
BitVecOp::BVS(..) => self.clone(),
BitVecOp::BVV(..) => self.clone(),
BitVecOp::SI(..) => todo!(),
BitVecOp::Not(ast) => todo!(),
BitVecOp::And(arc, arc1) => todo!(),
BitVecOp::Or(arc, arc1) => todo!(),
BitVecOp::Xor(arc, arc1) => todo!(),
BitVecOp::Add(arc, arc1) => todo!(),
BitVecOp::Sub(arc, arc1) => todo!(),
BitVecOp::Mul(arc, arc1) => todo!(),
BitVecOp::UDiv(arc, arc1) => todo!(),
BitVecOp::SDiv(arc, arc1) => todo!(),
BitVecOp::URem(arc, arc1) => todo!(),
BitVecOp::SRem(arc, arc1) => todo!(),
BitVecOp::Pow(arc, arc1) => todo!(),
BitVecOp::LShL(arc, arc1) => todo!(),
BitVecOp::LShR(arc, arc1) => todo!(),
BitVecOp::AShL(arc, arc1) => todo!(),
BitVecOp::AShR(arc, arc1) => todo!(),
BitVecOp::RotateLeft(arc, arc1) => todo!(),
BitVecOp::RotateRight(arc, arc1) => todo!(),
BitVecOp::ZeroExt(arc, _) => todo!(),
BitVecOp::SignExt(arc, _) => todo!(),
BitVecOp::Extract(arc, _, _) => todo!(),
BitVecOp::Concat(arc, arc1) => todo!(),
BitVecOp::Reverse(arc) => todo!(),
BitVecOp::FpToIEEEBV(arc) => todo!(),
BitVecOp::FpToUBV(arc, _, fprm) => todo!(),
BitVecOp::FpToSBV(arc, _, fprm) => todo!(),
BitVecOp::StrLen(arc) => todo!(),
BitVecOp::StrIndexOf(arc, arc1, arc2) => todo!(),
BitVecOp::StrToBV(arc) => todo!(),
BitVecOp::If(arc, arc1, arc2) => todo!(),
BitVecOp::Annotated(arc, annotation) => todo!(),
}))
}
}
Expand All @@ -107,22 +103,20 @@ impl<'c> Simplify<'c> for FloatAst<'c> {
Ok(self
.context()
.simplification_cache
.get_or_insert_with_float(self.hash(), || {
match &self.op() {
FloatOp::FPS(_, fsort) => todo!(),
FloatOp::FPV(float) => todo!(),
FloatOp::FpNeg(arc, fprm) => todo!(),
FloatOp::FpAbs(arc, fprm) => todo!(),
FloatOp::FpAdd(arc, arc1, fprm) => todo!(),
FloatOp::FpSub(arc, arc1, fprm) => todo!(),
FloatOp::FpMul(arc, arc1, fprm) => todo!(),
FloatOp::FpDiv(arc, arc1, fprm) => todo!(),
FloatOp::FpSqrt(arc, fprm) => todo!(),
FloatOp::FpToFp(arc, fsort, fprm) => todo!(),
FloatOp::BvToFpUnsigned(arc, fsort, fprm) => todo!(),
FloatOp::If(arc, arc1, arc2) => todo!(),
FloatOp::Annotated(arc, annotation) => todo!(),
}
.get_or_insert_with_float(self.hash(), || match &self.op() {
FloatOp::FPS(_, fsort) => todo!(),
FloatOp::FPV(float) => todo!(),
FloatOp::FpNeg(arc, fprm) => todo!(),
FloatOp::FpAbs(arc, fprm) => todo!(),
FloatOp::FpAdd(arc, arc1, fprm) => todo!(),
FloatOp::FpSub(arc, arc1, fprm) => todo!(),
FloatOp::FpMul(arc, arc1, fprm) => todo!(),
FloatOp::FpDiv(arc, arc1, fprm) => todo!(),
FloatOp::FpSqrt(arc, fprm) => todo!(),
FloatOp::FpToFp(arc, fsort, fprm) => todo!(),
FloatOp::BvToFpUnsigned(arc, fsort, fprm) => todo!(),
FloatOp::If(arc, arc1, arc2) => todo!(),
FloatOp::Annotated(arc, annotation) => todo!(),
}))
}
}
Expand All @@ -132,17 +126,15 @@ impl<'c> Simplify<'c> for StringAst<'c> {
Ok(self
.context()
.simplification_cache
.get_or_insert_with_string(self.hash(), || {
match &self.op() {
StringOp::StringS(_, _) => todo!(),
StringOp::StringV(_) => todo!(),
StringOp::StrConcat(arc, arc1) => todo!(),
StringOp::StrSubstr(arc, arc1, arc2) => todo!(),
StringOp::StrReplace(arc, arc1, arc2) => todo!(),
StringOp::BVToStr(arc) => todo!(),
StringOp::If(arc, arc1, arc2) => todo!(),
StringOp::Annotated(arc, annotation) => todo!(),
}
.get_or_insert_with_string(self.hash(), || match &self.op() {
StringOp::StringS(_, _) => todo!(),
StringOp::StringV(_) => todo!(),
StringOp::StrConcat(arc, arc1) => todo!(),
StringOp::StrSubstr(arc, arc1, arc2) => todo!(),
StringOp::StrReplace(arc, arc1, arc2) => todo!(),
StringOp::BVToStr(arc) => todo!(),
StringOp::If(arc, arc1, arc2) => todo!(),
StringOp::Annotated(arc, annotation) => todo!(),
}))
}
}
Expand Down
9 changes: 4 additions & 5 deletions crates/clarirs_core/src/ast/mod.rs
View file
Original file line number Diff line number Diff line change
@@ -1,15 +1,14 @@
pub mod astcache;
pub mod annotation;
pub mod astcache;
pub mod bitvec;
pub mod bool;
pub mod factory;
mod factory_support;
pub mod float;
pub mod node;
pub mod op;
pub mod bool;
pub mod bitvec;
pub mod float;
pub mod string;

pub use annotation::Annotation;
pub use factory::AstFactory;
pub use node::{AstNode, AstRef};

10 changes: 7 additions & 3 deletions crates/clarirs_core/src/ast/node.rs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,9 @@
use std::{
collections::HashSet, fmt::Debug, hash::{Hash, Hasher}, sync::Arc, vec::IntoIter
collections::HashSet,
fmt::Debug,
hash::{Hash, Hasher},
sync::Arc,
vec::IntoIter,
};

use serde::Serialize;
Expand Down Expand Up @@ -107,7 +111,6 @@ impl<'c, O: Op<'c>> Op<'c> for AstNode<'c, O> {
}
}


pub type AstRef<'c, Op> = Arc<AstNode<'c, Op>>;

#[derive(Clone, Eq, PartialEq, Hash, Debug, Serialize)]
Expand Down Expand Up @@ -148,7 +151,8 @@ impl<'c> Op<'c> for VarAst<'c> {
VarAst::BitVec(ast) => ast.variables(),
VarAst::Float(ast) => ast.variables(),
VarAst::String(ast) => ast.variables(),
}.clone()
}
.clone()
}
}

Expand Down
3 changes: 1 addition & 2 deletions crates/clarirs_core/src/solver/concrete.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,7 @@ impl<'c> ConcreteSolver<'c> {
}
}

impl<'c> Solver<'c> for ConcreteSolver<'c>
{
impl<'c> Solver<'c> for ConcreteSolver<'c> {
type Model = ConcreteModel;

fn add(&mut self, _: &BoolAst<'c>) -> Result<(), ClarirsError> {
Expand Down

0 comments on commit 9cab6d8

Please sign in to comment.