Skip to content

Commit

Permalink
Non bool relations (#130)
Browse files Browse the repository at this point in the history
This adds a source-to-source translation that removes all
non-boolean-returning relations. It also changes the todo!s in the
checkers to panic!s and updates the checker code paths in command.rs.

---------

Signed-off-by: Alex Fischman <[email protected]>
Signed-off-by: James R. Wilcox <[email protected]>
Co-authored-by: James R. Wilcox <[email protected]>
  • Loading branch information
Alex-Fischman and wilcoxjay authored Jul 24, 2023
1 parent 3b59347 commit e79a92b
Show file tree
Hide file tree
Showing 8 changed files with 402 additions and 13 deletions.
4 changes: 2 additions & 2 deletions bounded/src/bdd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -294,12 +294,12 @@ fn check_internal<'a>(

for relation in &module.signature.relations {
if relation.sort != Sort::Bool {
todo!("non-bool relations")
panic!("non-bool relations in checker (use Module::convert_non_bool_relations)")
}
}

if !module.defs.is_empty() {
todo!("definitions are not supported yet");
panic!("definitions in checker (use Module::inline_defs)")
}

let d = extract(module).map_err(CheckerError::ExtractionError)?;
Expand Down
4 changes: 2 additions & 2 deletions bounded/src/sat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -168,12 +168,12 @@ pub fn check(

for relation in &module.signature.relations {
if relation.sort != Sort::Bool {
todo!("non-bool relations")
panic!("non-bool relations in checker (use Module::convert_non_bool_relations)")
}
}

if !module.defs.is_empty() {
todo!("definitions are not supported yet");
panic!("definitions in checker (use Module::inline_defs)")
}

let d = extract(module).map_err(CheckerError::ExtractionError)?;
Expand Down
4 changes: 2 additions & 2 deletions bounded/src/set.rs
Original file line number Diff line number Diff line change
Expand Up @@ -563,7 +563,7 @@ fn translate<'a>(
) -> Result<(BoundedProgram, Indices<'a>), TranslationError> {
for relation in &module.signature.relations {
if relation.sort != Sort::Bool {
todo!("non-bool relations")
panic!("non-bool relations in checker (use Module::convert_non_bool_relations)")
}
}

Expand All @@ -579,7 +579,7 @@ fn translate<'a>(
}

if !module.defs.is_empty() {
todo!("definitions are not supported yet");
panic!("definitions in checker (use Module::inline_defs)")
}

let d = extract(module).map_err(TranslationError::ExtractionError)?;
Expand Down
2 changes: 1 addition & 1 deletion bounded/src/smt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ pub fn check(
print_timing: bool,
) -> Result<CheckerAnswer, CheckerError> {
if !module.defs.is_empty() {
todo!("definitions are not supported yet");
panic!("definitions are not supported yet");
}

let d = extract(module).map_err(CheckerError::ExtractionError)?;
Expand Down
1 change: 1 addition & 0 deletions fly/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ pub mod defs;
pub mod ouritertools;
pub mod parser;
pub mod printer;
pub mod rets;
pub mod semantics;
pub mod sorts;
pub mod syntax;
Expand Down
Loading

0 comments on commit e79a92b

Please sign in to comment.