Allow creating constants in Dynamic.

z3/src/ast.rs

@@ -1673,6 +1673,29 @@ impl<'ctx> Dynamic<'ctx> {
             _ => None,
         }
     }
+<<<<<<< Updated upstream
+=======
+
+    pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S, sort: &Sort<'ctx>) -> Self {
+        assert_eq!(ctx, sort.ctx);
+
+        Self::new(ctx, unsafe {
+            Z3_mk_const(ctx.z3_ctx, name.into().as_z3_symbol(ctx), sort.z3_sort)
+        })
+    }
+
+    pub fn fresh_const(ctx: &'ctx Context, prefix: &str, sort: &Sort<'ctx>) -> Self {
+        assert_eq!(ctx, sort.ctx);
+
+        Self::new(ctx, unsafe {
+            let pp = CString::new(prefix).unwrap();
+            let p = pp.as_ptr();
+            Z3_mk_fresh_const(ctx.z3_ctx, p, sort.z3_sort)
+        })
+    }
+
+    // TODO as_set. SortKind::Set does not exist
+>>>>>>> Stashed changes
 }
 
 impl<'ctx> Datatype<'ctx> {