smt: add missing ureal to real conversion case

moves-rwth · Jan 8, 2024 · c19be1f · c19be1f
1 parent 024930f
commit c19be1f
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/src/smt/symbolic.rs b/src/smt/symbolic.rs
@@ -127,7 +127,7 @@ impl<'ctx> Symbolic<'ctx> {
             Symbolic::Int(v) => Dynamic::from(v),
             Symbolic::UInt(v) => Dynamic::from(v.as_int().clone()),
             Symbolic::Real(v) => Dynamic::from(v),
-            Symbolic::UReal(v) => Dynamic::from(v.as_real().clone()),
+            Symbolic::UReal(v) => Dynamic::from(v.into_real()),
             Symbolic::EUReal(v) => ctx.super_eureal().to_datatype(&v).as_dynamic(),
             Symbolic::List(v) => v.as_dynamic(),
             Symbolic::Uninterpreted(v) => v,

diff --git a/src/smt/translate_exprs.rs b/src/smt/translate_exprs.rs
@@ -339,6 +339,10 @@ impl<'smt, 'ctx> TranslateExprs<'smt, 'ctx> {
                         let operand = self.t_int(operand);
                         Real::from_int(&operand)
                     }
+                    TyKind::UReal => {
+                        let operand = self.t_ureal(operand);
+                        operand.into_real()
+                    }
                     _ => panic!("illegal cast to {:?} from {:?}", &expr.ty, &operand.ty),
                 }
             }

diff --git a/z3rro/src/ureal.rs b/z3rro/src/ureal.rs
@@ -37,6 +37,10 @@ impl<'ctx> UReal<'ctx> {
     pub fn as_real(&self) -> &Real<'ctx> {
         &self.0
     }
+
+    pub fn into_real(self) -> Real<'ctx> {
+        self.0
+    }
 }
 
 impl<'ctx> SmtAst<'ctx> for UReal<'ctx> {
-Original file line number
+Diff line change
@@ Expand Up / @@ -37,6 +37,10 @@ impl<'ctx> UReal<'ctx> { @@
         pub fn as_real(&self) -> &Real<'ctx> {
             &self.0
         }
+        pub fn into_real(self) -> Real<'ctx> {
+            self.0
+        }
     }
     impl<'ctx> SmtAst<'ctx> for UReal<'ctx> {
@@ Expand Down @@