Bound bool vars (#127)

All checkers can now translate boolean bound variables that aren't inside an App, which was previously an oversight. --------- Signed-off-by: Alex Fischman <[email protected]> Co-authored-by: Alex Fischman <[email protected]>
flyvy-verifier · Jul 21, 2023 · 21a5418 · 21a5418
1 parent fe60f99
commit 21a5418
Show file tree

Hide file tree

Showing 3 changed files with 21 additions and 5 deletions.
diff --git a/bounded/src/bdd.rs b/bounded/src/bdd.rs
@@ -454,6 +454,11 @@ fn term_to_bdd(
 
     let bdd: Bdd = match term {
         Term::Literal(value) => context.mk_bool(*value),
+        Term::Id(id) => match assignments.get(id) {
+            Some(0) => context.mk_bool(false),
+            Some(1) => context.mk_bool(true),
+            _ => return Err(CheckerError::CouldNotTranslateToBdd(term.clone())),
+        },
         Term::App(relation, primes, args) => context.get(
             relation,
             &args.iter().map(element).collect::<Result<Vec<_>, _>>()?,
@@ -508,8 +513,9 @@ fn term_to_bdd(
         }
         Term::UnaryOp(UOp::Prime | UOp::Always | UOp::Eventually, _)
         | Term::UnaryOp(UOp::Next | UOp::Previously, _)
-        | Term::BinOp(BinOp::Until | BinOp::Since, ..)
-        | Term::Id(_) => return Err(CheckerError::CouldNotTranslateToBdd(term.clone())),
+        | Term::BinOp(BinOp::Until | BinOp::Since, ..) => {
+            return Err(CheckerError::CouldNotTranslateToBdd(term.clone()))
+        }
     };
     Ok(bdd)
 }

diff --git a/bounded/src/sat.rs b/bounded/src/sat.rs
@@ -329,6 +329,11 @@ fn term_to_ast(
     let ast: Ast = match term {
         Term::Literal(true) => Ast::And(vec![]),
         Term::Literal(false) => Ast::Or(vec![]),
+        Term::Id(id) => match assignments.get(id) {
+            Some(0) => Ast::Or(vec![]),
+            Some(1) => Ast::And(vec![]),
+            _ => return Err(CheckerError::CouldNotTranslateToAst(term.clone())),
+        },
         Term::App(relation, primes, args) => Ast::Var(
             relation.to_string(),
             args.iter().map(element).collect::<Result<Vec<_>, _>>()?,
@@ -387,8 +392,9 @@ fn term_to_ast(
         }
         Term::UnaryOp(UOp::Prime | UOp::Always | UOp::Eventually, _)
         | Term::UnaryOp(UOp::Next | UOp::Previously, _)
-        | Term::BinOp(BinOp::Until | BinOp::Since, ..)
-        | Term::Id(_) => return Err(CheckerError::CouldNotTranslateToAst(term.clone())),
+        | Term::BinOp(BinOp::Until | BinOp::Since, ..) => {
+            return Err(CheckerError::CouldNotTranslateToAst(term.clone()))
+        }
     };
     Ok(ast)
 }

diff --git a/bounded/src/set.rs b/bounded/src/set.rs
@@ -1061,6 +1061,11 @@ fn term_to_ast(
     let ast: Ast = match term {
         Term::Literal(true) => Ast::And(btreeset![]),
         Term::Literal(false) => Ast::Or(btreeset![]),
+        Term::Id(id) => match assignments.get(id) {
+            Some(0) => Ast::Or(btreeset![]),
+            Some(1) => Ast::And(btreeset![]),
+            _ => return Err(TranslationError::CouldNotTranslateToAst(term.clone())),
+        },
         Term::App(name, 0, args) => {
             let args = args.iter().map(element).collect::<Result<Vec<_>, _>>()?;
             Ast::Includes(name.clone(), Elements::new(args))
@@ -1120,7 +1125,6 @@ fn term_to_ast(
         Term::UnaryOp(UOp::Prime | UOp::Always | UOp::Eventually, _)
         | Term::UnaryOp(UOp::Next | UOp::Previously, _)
         | Term::BinOp(BinOp::Until | BinOp::Since, ..)
-        | Term::Id(_)
         | Term::App(..) => return Err(TranslationError::CouldNotTranslateToAst(term.clone())),
     };
     Ok(ast)